OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootAverageBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Contraction of the actual root average in the quotient square norm. The bound follows from finite Cauchy--Schwarz and the proved measure transport.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootAverage_value line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootAverage_norm_sq line 24
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootResidueOperator_integrable line 52
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootAverage_mass_le line 64