The three-dimensional heat kernel

This file fixes the Gaussian normalization used by the parabolic estimates. The spatial variable is the repository's Fin 3 → ℝ type, and the spatial quadratic form is written as a finite sum so that it is independent of the ambient sup norm on the function space.

Definitions and elementary identities

noncomputable def CKN.Foundation.Heat.heatKernel (x : Parabolic.Vec3) (t : ℝ) : ℝ

Three-dimensional Gaussian heat kernel, extended by zero to nonpositive time.

Equations

• CKN.Foundation.Heat.heatKernel x t = if 0 < t then (4 * Real.pi * t) ^ (-3 / 2) * Real.exp ((-∑ i : Fin 3, x i ^ 2) / (4 * t)) else 0

noncomputable def CKN.Foundation.Heat.heatKernelPlus (p : Parabolic.ParabolicPoint) : ℝ

Causal heat kernel on parabolic points.

Equations

• CKN.Foundation.Heat.heatKernelPlus p = if 0 < p.2 then CKN.Foundation.Heat.heatKernel p.1 p.2 else 0

noncomputable def CKN.Foundation.Heat.rhoTwo (x : Parabolic.Vec3) (t : ℝ) : ℝ

Sum of spatial Euclidean length and the square root of time used in kernel estimates.

Equations

• CKN.Foundation.Heat.rhoTwo x t = CKN.Foundation.Parabolic.vec3EuclideanNorm x + √t

theorem CKN.Foundation.Heat.vec3EuclideanNorm_sq (x : Parabolic.Vec3) : Parabolic.vec3EuclideanNorm x ^ 2 = ∑ i : Fin 3, x i ^ 2

theorem CKN.Foundation.Heat.heatKernel_eq_zero_of_nonpos {x : Parabolic.Vec3} {t : ℝ} (ht : t ≤ 0) : heatKernel x t = 0

theorem CKN.Foundation.Heat.heatKernel_eq_formula {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : heatKernel x t = (4 * Real.pi * t) ^ (-3 / 2) * Real.exp (-Parabolic.vec3EuclideanNorm x ^ 2 / (4 * t))

theorem CKN.Foundation.Heat.heatKernel_eq_formula_sum {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : heatKernel x t = (4 * Real.pi * t) ^ (-3 / 2) * Real.exp ((-∑ i : Fin 3, x i ^ 2) / (4 * t))

theorem CKN.Foundation.Heat.heatKernel_nonneg (x : Parabolic.Vec3) (t : ℝ) : 0 ≤ heatKernel x t

theorem CKN.Foundation.Heat.heatKernel_pos {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : 0 < heatKernel x t

theorem CKN.Foundation.Heat.heatKernelPlus_eq_heatKernel (p : Parabolic.ParabolicPoint) : heatKernelPlus p = heatKernel p.1 p.2

theorem CKN.Foundation.Heat.heatKernelPlus_eq_zero_of_nonpos {x : Parabolic.Vec3} {t : ℝ} (ht : t ≤ 0) : heatKernelPlus (x, t) = 0

theorem CKN.Foundation.Heat.heatKernel_integrable {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (x : Parabolic.Vec3) => heatKernel x t) MeasureTheory.volume

theorem CKN.Foundation.Heat.gaussian_integral (t : ℝ) (ht : 0 < t) : ∫ (x : Parabolic.Vec3), Real.exp ((-∑ i : Fin 3, x i ^ 2) / (4 * t)) = √(4 * Real.pi * t) ^ 3

theorem CKN.Foundation.Heat.heatKernel_integral (t : ℝ) (ht : 0 < t) : ∫ (x : Parabolic.Vec3), heatKernel x t = 1

theorem CKN.Foundation.Heat.heatKernelPlus_nonneg (p : Parabolic.ParabolicPoint) : 0 ≤ heatKernelPlus p