OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeMassOperator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The same cubed-prime correspondence on the actual automorphic mass space. It agrees with the energy operator and is self-adjoint there.

  1. def OAI.CubicFirstMoment.cubicThetaFiniteMassClosure line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaFiniteMassClosure_val line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaFiniteMassClosure_dense line 20
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRawMass line 30
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRawMass_bound line 34
  6. def OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeMass line 43
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeMass_finite line 48
  8. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeMass_energy line 57
  9. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeMass_bound line 70
  10. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeMass_symmetric line 80