OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootL2.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

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

  1. abbrev OAI.CubicFirstMoment.CubicThetaPrimeRootL2 line 13
  2. def OAI.CubicFirstMoment.cubicThetaPrimeRootSectionRepresentative line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionRepresentative_measurable line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionRepresentative_norm line 24
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylSection_memLp line 31
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionL2_norm_sq line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylSection_L2_norm line 54
  8. def OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteSections line 64
  9. def OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteValue line 75
  10. def OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteWeyl line 81
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteWeyl_norm line 87