Time integrals for derivatives of the four-dimensional Green kernel

The zeroth-order Green bound in GreenBounds.lean uses

∫₀∞ t⁻² exp (-a / t) dt = a⁻¹.

Differentiating the Gaussian once and twice introduces the two adjacent integrals proved here. Keeping these scalar identities separate avoids repeating the inversion substitution in the derivative estimates for blueprint node I-green.

def Anderson4D.euclideanDistSq (x : R4) : ℝ

Squared Euclidean length on the lifted space ℝ⁴. It is kept separate from the ambient Pi norm because the paper's heat kernel uses the Euclidean quadratic form while R4 deliberately carries mathlib's Pi norm.

Equations

• Anderson4D.euclideanDistSq x = ∑ i : Fin Anderson4D.dim, x i ^ 2

noncomputable def Anderson4D.euclideanHeatKernel4 (t : ℝ) (x : R4) : ℝ

The non-periodized four-dimensional Gaussian heat kernel.

Equations

• Anderson4D.euclideanHeatKernel4 t x = (4 * Real.pi * t) ^ (-2) * Real.exp (-Anderson4D.euclideanDistSq x / (4 * t))

noncomputable def Anderson4D.laplaceFundamental4 (x : R4) : ℝ

The principal singularity in paper (4.1): (4π²|x|²)⁻¹.

Equations

• Anderson4D.laplaceFundamental4 x = (4 * Real.pi ^ 2 * Anderson4D.euclideanDistSq x)⁻¹

theorem Anderson4D.euclideanDistSq_nonneg (x : R4) : 0 ≤ euclideanDistSq x

The Euclidean squared length is nonnegative.

theorem Anderson4D.euclideanHeatKernel4_eq_timeMajorant {t : ℝ} (ht : 0 < t) (x : R4) : euclideanHeatKernel4 t x = (16 * Real.pi ^ 2)⁻¹ * ((t ^ 2)⁻¹ * Real.exp (-(euclideanDistSq x / 4 / t)))

Algebraic normal form of the Euclidean heat kernel used by all three time-integral calculations.

theorem Anderson4D.integrableOn_euclideanHeatKernel4 {x : R4} (hx : euclideanDistSq x ≠ 0) : MeasureTheory.IntegrableOn (fun (t : ℝ) => euclideanHeatKernel4 t x) (Set.Ioi 0) MeasureTheory.volume

The Euclidean heat kernel is genuinely integrable in time away from the spatial origin.

theorem Anderson4D.integral_euclideanHeatKernel4 {x : R4} (hx : euclideanDistSq x ≠ 0) : ∫ (t : ℝ) in Set.Ioi 0, euclideanHeatKernel4 t x = laplaceFundamental4 x

The exact Bessel-time representation of the four-dimensional principal singularity. This fixes the coefficient 1/(4π²) appearing in the improved part of (4.1).

theorem Anderson4D.integral_inv_cube_exp {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ) in Set.Ioi 0, (t ^ 3)⁻¹ * Real.exp (-(a / t)) = a⁻¹ ^ 2

The first-derivative time integral: ∫₀∞ t⁻³ exp (-a/t) dt = a⁻².

theorem Anderson4D.integral_inv_fourth_exp {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ) in Set.Ioi 0, (t ^ 4)⁻¹ * Real.exp (-(a / t)) = 2 * a⁻¹ ^ 3

The second-derivative time integral: ∫₀∞ t⁻⁴ exp (-a/t) dt = 2a⁻³.

theorem Anderson4D.integrableOn_inv_cube_exp {a : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (t ^ 3)⁻¹ * Real.exp (-(a / t))) (Set.Ioi 0) MeasureTheory.volume

Absolute integrability of the first-derivative time majorant. This is the hypothesis needed to exchange a first spatial derivative with the Bessel-potential time integral.

theorem Anderson4D.integrableOn_inv_fourth_exp {a : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (t ^ 4)⁻¹ * Real.exp (-(a / t))) (Set.Ioi 0) MeasureTheory.volume

Absolute integrability of the second-derivative time majorant.