OAI/NumberTheory/CubicMoment/Estimates/FarIntegratedBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual far-cell height integral gains (J/T)^2. Its only analytic coefficient bound is a uniform mean for the original finite polynomial.

  1. theorem OAI.CubicFirstMoment.far_integrated_norm_bound line 14