OAI/NumberTheory/CubicMoment/Theta/CubicThetaLogMeasure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The radial L2 mass and energy after logarithmic height conjugation. The measure factors are exactly those of hyperbolic three-space.

  1. lemma OAI.CubicFirstMoment.cubicThetaLogLift_mass_integrand line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaLogLift_mass line 17
  3. theorem OAI.CubicFirstMoment.cubicThetaLogLift_mass_integrable_iff line 25
  4. theorem OAI.CubicFirstMoment.cubicThetaLogLift_energy line 33