OAI/NumberTheory/CubicMoment/Estimates/CubicBesselBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit exponential decay of the fixed cubic Bessel kernel, obtained from its defining positive heat integral.

  1. lemma OAI.CubicFirstMoment.cubicBessel_exponent_bound line 11
  2. lemma OAI.CubicFirstMoment.cubicBesselHeat_exp_bound line 23
  3. lemma OAI.CubicFirstMoment.cubicBesselKernel_exp_bound line 34
  4. lemma OAI.CubicFirstMoment.cubicBessel_exp_prefactor line 51
  5. theorem OAI.CubicFirstMoment.cubicBesselKernel_exponential_decay line 65

    Source documentation

    A single exponential majorant for all positive arguments at least one.

    theorem cubicBesselKernel_exponential_decay {x : ℝ} (hx : 1 ≤ x) :
    cubicBesselKernel x ≤ (Real.Gamma (1/3)*2^(1/3:ℝ))*Real.exp (-Real.sqrt x) := by
…

    Mentions: OAI.CubicFirstMoment.cubicBesselKernel