Modified Bessel Function K₁

This file defines the modified Bessel function K₁(z) via its integral representation and establishes key properties needed for the free covariance in AQFT.

Main definitions

• besselK1 - The modified Bessel function K₁(z) = ∫₀^∞ exp(-z cosh(t)) cosh(t) dt
• besselK1_properTime - Alternative proper-time representation: K₁(z) = (z/2) ∫₀^∞ t^{-2} exp(-t - z²/(4t)) dt

Main results

• besselK1_pos - K₁(z) > 0 for z > 0
• besselK1_asymptotic - Asymptotic bound K₁(z) ≤ √(π/(2z)) · exp(-z) · 2 for z ≥ 1
• besselK1_eq_properTime - Equivalence of cosh and proper-time representations
• schwingerIntegral_eq_besselK1 - Identity connecting Schwinger integral to K₁

Notes

The cosh integral representation is particularly useful because:

1. It's manifestly real and positive for positive arguments
2. The integrand decays exponentially in t for any z > 0
3. It directly shows the analytic structure in z

For the massive scalar field in 4D Euclidean space, the exact formula is: C(x,y) = (m / (4π² |x-y|)) · K₁(m |x-y|)

noncomputable def besselK1 (z : ℝ) : ℝ

The modified Bessel function K₁(z) via cosh integral representation. K₁(z) = ∫₀^∞ exp(-z cosh(t)) cosh(t) dt This is well-defined and positive for z > 0.

Equations

• besselK1 z = ∫ (t : ℝ) in Set.Ici 0, Real.exp (-z * Real.cosh t) * Real.cosh t

theorem besselK1_pos (z : ℝ) (hz : 0 < z) : 0 < besselK1 z

K₁(z) is positive for z > 0.

theorem besselK1_continuousOn : ContinuousOn besselK1 (Set.Ioi 0)

K₁ is continuous on (0, ∞). This follows from dominated convergence since the integrand z ↦ exp(-z cosh(t)) cosh(t) is continuous in z and dominated by exp(-ε cosh(t)) cosh(t) for z ≥ ε, which is integrable.

The formal proof uses MeasureTheory.continuousOn_of_dominated_of_compact: for z in compact K ⊆ (0, ∞), bound by exp(-min(K) * cosh(t)) * cosh(t).

theorem besselK1_asymptotic (z : ℝ) (hz : 1 ≤ z) : besselK1 z ≤ (Real.sinh 1 + 2) * Real.exp (-z)

K₁ has exponential decay: K₁(z) ≤ (sinh(1) + 2) · exp(-z) for z ≥ 1. This bound is sufficient for proving integrability of the free covariance kernel. The proof uses the same technique as besselK1_mul_self_le but for z ≥ 1.

theorem besselK1_mul_self_le (z : ℝ) (hz : 0 < z) (hz_le : z ≤ 1) : z * besselK1 z ≤ Real.cosh 1 + 2

For z ∈ (0, 1], we have z · K₁(z) ≤ cosh(1) + 2. This follows from splitting the integral at t = 1:

• On [0,1]: z · ∫₀¹ exp(-z cosh t) cosh t dt ≤ z · cosh(1) ≤ cosh(1)
• On [1,∞): z · ∫₁^∞ exp(-z cosh t) cosh t dt ≤ 2 (via exponential bound)

theorem besselK1_near_origin_bound (z : ℝ) (hz : 0 < z) (hz_small : z ≤ 1) : besselK1 z ≤ (Real.cosh 1 + 2) / z

Near-origin bound for K₁: K₁(z) ≤ (cosh(1) + 2)/z for z ∈ (0, 1]. This follows from z · K₁(z) ≤ cosh(1) + 2 (proved in besselK1_mul_self_le).

theorem radial_besselK1_integrable (m : ℝ) (hm : 0 < m) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ 2 * besselK1 (m * r)) (Set.Ioi 0) MeasureTheory.volume

The radial integrand r² K₁(mr) is integrable on (0, ∞) for m > 0.

Mathematical justification:

• Near 0: K₁(mr) 1/(mr), so r² K₁(mr) r/m, which is integrable near 0
• At ∞: K₁(mr) ~ e^{-mr}/√(mr), so r² K₁(mr) decays exponentially

This is a key ingredient for showing the free covariance kernel is L¹ in 4D.

theorem bessel_symmetry_integral (z : ℝ) (hz : 0 < z) : ∫ (u : ℝ), Real.exp (-u) * Real.exp (-z * Real.cosh u) = 2 * besselK1 z

Symmetry lemma: the full-line integral of exp(-u) * exp(-z cosh u) equals twice the half-line cosh integral, which is 2 * K₁(z).

∫_{-∞}^∞ exp(-u) * exp(-z cosh u) du = 2 ∫_0^∞ cosh(u) * exp(-z cosh u) du

This follows from splitting at 0 and using cosh(-u) = cosh(u).

theorem schwingerIntegral_eq_besselK1 (m r : ℝ) (hm : 0 < m) (hr : 0 < r) : ∫ (t : ℝ) in Set.Ioi 0, 1 / t ^ 2 * Real.exp (-m ^ 2 * t - r ^ 2 / (4 * t)) = 4 * m / r * besselK1 (m * r)

Key identity connecting the Schwinger proper-time integral to K₁: ∫₀^∞ t^{-2} exp(-m²t - r²/(4t)) dt = (4m/r) · K₁(mr)

This is proven directly via the substitution t = (r/(2m)) exp(u), which transforms the integral to the cosh representation of K₁.