OAI/NumberTheory/CubicMoment/Estimates/SmallBPoissonEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An absolute Poisson envelope and its actual infinite tail for arbitrary coefficients, in terms of their exact quadratic energy.

  1. theorem OAI.CubicFirstMoment.arbitrary_poisson_dyad_energy line 14
  2. theorem OAI.CubicFirstMoment.arbitrary_poisson_energy_tail line 42