CubicBesselPowerDecay.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit arbitrary power majorants for the cubic theta kernel.

lemma OAI.CubicFirstMoment.pow_mul_exp_neg_le_factorial line 10
lemma OAI.CubicFirstMoment.exp_neg_div_le_power line 19
lemma OAI.CubicFirstMoment.cubicBesselHeat_power_bound line 28
theorem OAI.CubicFirstMoment.cubicBesselKernel_power_bound line 47
Source documentation
The power is arbitrary; the coefficient is the exact Gamma integral of its positive majorant. This is used for summing the actual theta series.
```
theorem cubicBesselKernel_power_bound (k : ℕ) (hk : 1 ≤ k) {x : ℝ} (hx : 0 < x) :
    cubicBesselKernel x ≤ ((k.factorial:ℝ)*Real.Gamma ((k:ℝ)-1/3))*
      x^(1/6-(k:ℝ)) := by
…
```
Mentions: OAI.CubicFirstMoment.cubicBesselKernel