OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeL2.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual L2 representatives of sections on the finite prime cover. The Atkin action preserves square integrability and the exact L2 norm.

  1. abbrev OAI.CubicFirstMoment.CubicThetaPrimeL2 line 13
  2. def OAI.CubicFirstMoment.cubicThetaPrimeSectionRepresentative line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionRepresentative_measurable line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionRepresentative_norm line 24
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinSection_memLp line 31
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionL2_norm_sq line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinSection_L2_norm line 54
  8. def OAI.CubicFirstMoment.cubicThetaPrimeFiniteSections line 64
  9. def OAI.CubicFirstMoment.cubicThetaPrimeFiniteValue line 75
  10. def OAI.CubicFirstMoment.cubicThetaPrimeFiniteAtkin line 81
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeFiniteAtkin_norm line 87