OAI/NumberTheory/CubicMoment/Theta/CubicThetaGlobalL2.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual automorphic sections as global L2 vectors. A Borel section chooses representatives, while the norm is the continuous intrinsic norm on the quotient, so compact smooth sections are square integrable.

  1. abbrev OAI.CubicFirstMoment.CubicThetaGlobalL2 line 14
  2. def OAI.CubicFirstMoment.cubicThetaSectionRepresentative line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaSectionRepresentative_measurable line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaSectionRepresentative_norm line 23
  5. lemma OAI.CubicFirstMoment.cubicThetaSectionRepresentative_memLp line 29
  6. def OAI.CubicFirstMoment.cubicThetaGlobalMass line 36
  7. def OAI.CubicFirstMoment.cubicThetaAutomorphicL2 line 58
  8. instance OAI.CubicFirstMoment.cubicThetaAutomorphicL2_complete line 61