OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspCutoffEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

With any prescribed loss above the sharp coefficient one, cutting off a cusp costs only mass in its fixed compact transition annulus.

  1. lemma OAI.CubicFirstMoment.cubicThetaCuspRaw_differentiableAt line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaCuspCutoff_energy line 26