OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteEnergySum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite sum estimate for the literal squared differential norm.

  1. lemma OAI.CubicFirstMoment.cubicThetaTangentEnergy_sum_le line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaFunctionEnergy_sum_le line 30
  3. lemma OAI.CubicFirstMoment.cubicThetaFunctionEnergy_one_sub line 44