OAI/NumberTheory/CubicMoment/Estimates/MellinMassIntegration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble a local Mellin estimate and the two signed tails as a bound for the full integral.

  1. lemma OAI.CubicFirstMoment.integral_height_split line 11
  2. theorem OAI.CubicFirstMoment.integral_local_and_signed_tail line 31