OAI/NumberTheory/CubicMoment/Estimates/ExceptionalBenchmark.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalize the exceptional moments by the actual local dispersion benchmark B²(PQ²)^(1/3), retaining a positive power saving.

  1. lemma OAI.CubicFirstMoment.exceptional_conductor_lower line 10
  2. lemma OAI.CubicFirstMoment.conductor_rpow_identity line 17
  3. theorem OAI.CubicFirstMoment.exceptional_moment_benchmark line 25