CubicBesselIntegral.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The fixed order-one-third Bessel kernel in the cubic theta expansion. The Schläfli heat integral is used as the definition; its Mellin mass is proved by absolute Fubini and the two ordinary Gamma integrals. Normalization: NIST DLMF 10.32.10, specialized to nu=1/3 and positive argument; the cubic theta expansion is DR v3 section 5.1, Eq.(5.6).

def OAI.CubicFirstMoment.cubicBesselHeat line 16
Source documentation
The positive heat integrand for 2*K_(1/3)(2*sqrt x).
```
def cubicBesselHeat (x t : ℝ) : ℝ :=
…
```
def OAI.CubicFirstMoment.cubicBesselKernel line 20
Source documentation
Fixed Bessel order required by the cubic metaplectic Fourier series.
```
def cubicBesselKernel (x : ℝ) : ℝ :=
…
```
lemma OAI.CubicFirstMoment.cubicBesselHeat_nonneg line 23
lemma OAI.CubicFirstMoment.integrable_inverse_laplace_rpow line 28
lemma OAI.CubicFirstMoment.cubicBesselHeat_integrable line 36
lemma OAI.CubicFirstMoment.cubicBesselKernel_nonneg line 53
lemma OAI.CubicFirstMoment.cubicBesselHeat_inner_integral line 60
lemma OAI.CubicFirstMoment.cubicBesselHeat_mellin_integrable line 84
theorem OAI.CubicFirstMoment.cubicBesselKernel_real_mellin line 118
Source documentation
The Mellin mass needed to normalize the order-one-third theta kernel.
```
theorem cubicBesselKernel_real_mellin {σ : ℝ} (hσ : 1/6 < σ) :
    (∫ x in Ioi (0:ℝ), x^(σ-1)*cubicBesselKernel x) =
      Real.Gamma (σ+1/6)*Real.Gamma (σ-1/6) := by
…
```
Mentions: OAI.CubicFirstMoment.cubicBesselKernel