OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspHardy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact radial energy identity and Hardy bound, with the hyperbolic spectral threshold equal to one.

  1. lemma OAI.CubicFirstMoment.norm_square_integrable line 14
  2. lemma OAI.CubicFirstMoment.cross_compact line 20
  3. lemma OAI.CubicFirstMoment.cross_integrable line 28
  4. lemma OAI.CubicFirstMoment.cubicTheta_log_cross_integral line 33
  5. theorem OAI.CubicFirstMoment.cubicTheta_log_energy_identity line 42
  6. theorem OAI.CubicFirstMoment.cubicTheta_radial_energy_identity line 56
  7. theorem OAI.CubicFirstMoment.cubicTheta_radial_hardy line 64