OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeC1Energy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

C1 sections and their continuous intrinsic energy on the prime cover. Both the value and energy transform under the same Atkin map.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeC1Sections line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimeC1Atkin line 22
  3. def OAI.CubicFirstMoment.cubicThetaPrimeQuotientEnergy line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeQuotientEnergy_apply line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeQuotientEnergy_nonneg line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeQuotientEnergy_continuous line 48
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeC1Atkin_energy line 53
  8. theorem OAI.CubicFirstMoment.cubicThetaPrimeC1Atkin_energy_integral line 60