OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstStoppedTailEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The height-tail estimate depends only on the actual coefficient energies and uniform inner bound. This form permits independent norm twists before restoring the smooth total-product envelope.

  1. theorem OAI.CubicFirstMoment.scaleFirst_energy_cutoff_tail line 15
  2. theorem OAI.CubicFirstMoment.scaleFirst_energy_twisted_cutoff_tail line 71