OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticGradientMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual gradient energy of the arithmetic remainder is integrable in every cusp, with the same convergent vertical power as its mass.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticCoordinateEnergy line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoordinateEnergy_apply line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoordinateEnergy_density_bound line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoordinateEnergy_density_continuousOn line 59
  5. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCoordinateEnergy_integrable line 74