OAI/NumberTheory/CubicMoment/Estimates/LowEnergyTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Ordinary-height tails from logarithmic-width localization. The bounded second coefficient and both energies are preserved under every norm twist; full-line Mellin restoration retains the actual product envelope.

  1. theorem OAI.CubicFirstMoment.low_energy_cutoff_tail line 16
  2. theorem OAI.CubicFirstMoment.low_energy_envelope_cutoff_tail line 72