OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeEnergyInvariant.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The first-derivative energy of a C1 section descends to the actual prime quotient. Its invariance is obtained by differentiating automorphy.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionFunction_automorphy line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimeSectionDifferential line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionDifferential_automorphy line 25
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeSectionEnergy_invariant line 52
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionEnergy_continuous line 70