OAI/NumberTheory/CubicMoment/Estimates/OuterPrimalScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recover the three primal powers from the exact summed Poisson bound. The epsilon loss does not multiply the separate unit zero-frequency term.

  1. lemma OAI.CubicFirstMoment.outer_poisson_power_common line 10
  2. def OAI.CubicFirstMoment.outerPowerConstant line 26
  3. lemma OAI.CubicFirstMoment.outerPowerConstant_pos line 31
  4. lemma OAI.CubicFirstMoment.outer_primal_scale_bound line 39