OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Norm transfer through the entire product Mellin line. The central polynomial bound, derived Gauss complement and elementary model tail are kept separate in this finite integral inequality.

  1. lemma OAI.CubicFirstMoment.centered_mellin_integral_bound line 13