OAI/NumberTheory/CubicMoment/Estimates/PrimeConductorScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conductor powers measured at the full convolution length transfer to each rough coordinate, with one additional logarithmic power.

  1. lemma OAI.CubicFirstMoment.rough_coordinate_conductor_scale line 12