OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspVerticalEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The radial derivative in a cusp is controlled by the actual hyperbolic Dirichlet energy of the pulled-back cubic section.

  1. lemma OAI.CubicFirstMoment.cubicThetaTangentEnergy_apply line 12
  2. def OAI.CubicFirstMoment.cubicThetaVerticalTangent line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaVerticalTangent_norm line 30
  4. def OAI.CubicFirstMoment.cubicThetaVerticalPoint line 37
  5. lemma OAI.CubicFirstMoment.cubicThetaCuspSection_deriv line 39
  6. theorem OAI.CubicFirstMoment.cubicThetaCuspSection_vertical_energy line 58