OAI/NumberTheory/CubicMoment/Theta/CubicThetaSectionCutoffEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local cutoff estimate in intrinsic quotient variables. This is the pointwise bridge from the actual local graph to the global energy.

  1. lemma OAI.CubicFirstMoment.cubicThetaSectionFunction_energy_density line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaSectionCutoffEnergy_bound line 24