OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarCuspEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scaled cusp cutoffs have uniformly bounded hyperbolic gradient. The bound uses the unique high primitive row and exact Mobius transport.

  1. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_upper line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_local_zero line 25
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_energy_invariant line 40
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspCutoff_scaled_energy line 58
  5. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_energy_bound line 69