OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspScalarIntegrals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar transport from the quotient to each arithmetic cusp cell. These formulas separate mass and derivative energy, so the sharp Hardy coefficient is preserved when the cusp estimates are summed.

  1. def OAI.CubicFirstMoment.cubicThetaCuspPullback line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspPullback_apply line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaCuspPullback_integrable line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspPullback_integral line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaMass_integrable line 48
  6. lemma OAI.CubicFirstMoment.cubicThetaGradientEnergy_integrable line 53
  7. lemma OAI.CubicFirstMoment.cubicThetaCuspPullback_mass line 58
  8. lemma OAI.CubicFirstMoment.cubicThetaCuspPullback_energy line 67