The Fundamental Solution of Heat Equation

This file formalizes the properties of the heat kernel and its convolution solution following Rustom Choksi's Partial Differential Equations book (Chapter 7.2.2).

We establish:

1. Regularity properties (continuity and measurability).
2. $L^\infty$ bounds and decay estimates essential for dominated convergence.
3. Integrability of the kernel and its derivatives against a function $g$.
4. differentiation under the integral sign to prove the convolution solves the heat equation.

Reference

This formalization follows Chapter 7.2.2, "Partial Differential Equations, A First Course" by Professor Rustom Choksi.

1. Definitions and Derivative Shorthands

We define the convolution of the heat kernel with a function $g$ and introduce shorthand notation for the partial derivatives of the heat kernel.

noncomputable def Heat.heatConvolutionHK (α : ℝ) (g : ℝ → ℝ) (x t : ℝ) : ℝ

The convolution of the heat kernel with an initial data function g.

Equations

• Heat.heatConvolutionHK α g x t = ∫ (y : ℝ), Heat.heatKernel α (x - y) t * g y

noncomputable def Heat.HKt (α x t : ℝ) : ℝ

Partial derivative of the heat kernel with respect to time $t$.

Equations

• Heat.HKt α x t = deriv (fun (τ : ℝ) => Heat.heatKernel α x τ) t

noncomputable def Heat.HKx (α x t : ℝ) : ℝ

Partial derivative of the heat kernel with respect to space $x$.

Equations

• Heat.HKx α x t = deriv (fun (ξ : ℝ) => Heat.heatKernel α ξ t) x

noncomputable def Heat.HKxx (α x t : ℝ) : ℝ

Second partial derivative of the heat kernel with respect to space $x$.

Equations

• Heat.HKxx α x t = deriv (fun (x' : ℝ) => Heat.HKx α x' t) x

@[simp]

theorem Heat.sq_sub_comm (x y : ℝ) : (y - x) ^ 2 = (x - y) ^ 2

2. Explicit Derivative Formulas

We use the explicit calculations of the derivatives of the Heat Kernel from the previous chapter and make them consistent with the notation HKt, HKx, HKxx

theorem Heat.HKt_eq_derivative {α : ℝ} (hα : 0 < α) {t x : ℝ} (ht : 0 < t) : HKt α x t = -(1 / (2 * t)) * (1 / √(4 * Real.pi * α * t)) * Real.exp (-x ^ 2 / (4 * α * t)) + 1 / √(4 * Real.pi * α * t) * (1 / (4 * α) * (1 / t ^ 2) * x ^ 2) * Real.exp (-x ^ 2 / (4 * α * t))

theorem Heat.HKx_eq_derivative {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) : HKx α x t = 1 / √(4 * Real.pi * α * t) * (-(1 / (4 * α * t)) * (2 * x)) * Real.exp (-x ^ 2 / (4 * α * t))

theorem Heat.HKxx_eq_derivative {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) : HKxx α x t = 1 / √(4 * Real.pi * α * t) * (-(1 / (4 * α * t)) * 2 * Real.exp (-x ^ 2 / (4 * α * t)) + -(1 / (4 * α * t)) * (2 * x) * (-(1 / (4 * α * t)) * (2 * x)) * Real.exp (-x ^ 2 / (4 * α * t)))

3. Regularity: Continuity and Measurability

Here we establish that the heat kernel and its derivatives are continuous and strongly measurable functions. These properties are mainly used here as a prerequisite to showing that the solution formula indeed solves the heat equation, which requires us to differentiate under the integral.

theorem Heat.cont_HKt {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) : Continuous fun (y : ℝ) => HKt α (x - y) t

theorem Heat.meas_HKt {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => HKt α (x - y) t) MeasureTheory.volume

theorem Heat.cont_HKx {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) : Continuous fun (y : ℝ) => HKx α (x - y) t

theorem Heat.meas_HKx {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => HKx α (x - y) t) MeasureTheory.volume

theorem Heat.cont_HKxx {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) : Continuous fun (y : ℝ) => HKxx α (x - y) t

theorem Heat.meas_HKxx {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => HKxx α (x - y) t) MeasureTheory.volume

theorem Heat.cont_heatKernel {α x t : ℝ} : Continuous fun (y : ℝ) => heatKernel α (x - y) t

theorem Heat.meas_heatKernel {α x t : ℝ} : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => heatKernel α (x - y) t) MeasureTheory.volume

4. Pointwise Bounds and L-infinity Estimates

We define bounding constants K, Kx, Kxx and for the heat kernel's derivatives. This implies they belong to $L^\infty$.

noncomputable def Heat.Kx (α t : ℝ) : ℝ

Equations

• Heat.Kx α t = 1 / (2 * √Real.pi * α * t)

noncomputable def Heat.Kxx (α t : ℝ) : ℝ

Equations

• Heat.Kxx α t = (1 + 2 * Real.exp (-1)) / (2 * α * t * √(4 * Real.pi * α * t))

theorem Heat.heatKernel_bound_pointwise {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) (y : ℝ) : heatKernel α (x - y) t ≥ 0 ∧ heatKernel α (x - y) t ≤ 1 / √(4 * Real.pi * α * t)

theorem Heat.Linfty_heatKernel {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) : MeasureTheory.MemLp (fun (y : ℝ) => heatKernel α (x - y) t) ⊤ MeasureTheory.volume

theorem Heat.bound_x_exp_neg_x {x : ℝ} : x * Real.exp (-x) ≤ Real.exp (-1)

theorem Heat.sq_mul_exp_neg_mul_sq_le {b : ℝ} (hb : 0 < b) (x : ℝ) : x ^ 2 * Real.exp (-(b * x ^ 2)) ≤ Real.exp (-1) / b

theorem Heat.pointwise_bound_HKt {α x t : ℝ} (ht : 0 < t) (hα : 0 < α) : |HKt α x t| ≤ 3 / (2 * t) * c α t

theorem Heat.HKt_Linfinity_bound {α x t : ℝ} (ht : 0 < t) (hα : 0 < α) : MeasureTheory.MemLp (fun (y : ℝ) => HKt α (x - y) t) ⊤ MeasureTheory.volume

theorem Heat.pointwise_bound_HKx {α x t : ℝ} (ht : 0 < t) (hα : 0 < α) : |HKx α x t| ≤ Kx α t

theorem Heat.HKx_Linfinity_bound {α x t : ℝ} (ht : 0 < t) (hα : 0 < α) : MeasureTheory.MemLp (fun (y : ℝ) => HKx α (x - y) t) ⊤ MeasureTheory.volume

theorem Heat.HKxx_uniform_bound {α t : ℝ} (hα : 0 < α) (ht : 0 < t) (x : ℝ) : |HKxx α x t| ≤ Kxx α t

theorem Heat.pointwise_bound_HKxx {α x t : ℝ} (ht : 0 < t) (hα : 0 < α) : |HKxx α x t| ≤ Kxx α t

theorem Heat.HKxx_Linfinity_bound {α x t : ℝ} (ht : 0 < t) (hα : 0 < α) : MeasureTheory.MemLp (fun (y : ℝ) => HKxx α (x - y) t) ⊤ MeasureTheory.volume

theorem Heat.mono_Coeff {α t τ : ℝ} (ht : 0 < t) (hτ : 0 < τ) (hα : 0 < α) (hsize : τ ≤ t) : c α t ≤ c α τ

5. Integrability of the Kernels

We demonstrate that the heat kernel and its derivatives are integrable when multiplied by an integrable function $g$

theorem Heat.integrable_heatKernel {α t : ℝ} (hα : 0 < α) (ht : 0 < t) : MeasureTheory.Integrable (fun (x : ℝ) => heatKernel α x t) MeasureTheory.volume

theorem Heat.integrable_heatKernel_slice {α t : ℝ} (hα : 0 < α) (ht : 0 < t) (x : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => heatKernel α (x - y) t) MeasureTheory.volume

theorem Heat.integrable_heatKernel_mul_of_Linfty {B α : ℝ} (g : ℝ → ℝ) {x t : ℝ} (hα : 0 < α) (ht : 0 < t) (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hBound : ∀ (y : ℝ), |g y| ≤ B) : MeasureTheory.Integrable (fun (y : ℝ) => heatKernel α (x - y) t * |g y|) MeasureTheory.volume

theorem Heat.integrable_heatKernel_mul_of_L1 {α : ℝ} (g : ℝ → ℝ) {x t : ℝ} (hα : 0 < α) (ht : 0 < t) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : ℝ) => heatKernel α (x - y) t * g y) MeasureTheory.volume

theorem Heat.aestronglyMeasurable_heatKernel_mul {α x t : ℝ} (hα : 0 < α) (ht : 0 < t) (g : ℝ → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => heatKernel α (x - y) t * g y) MeasureTheory.volume

theorem Heat.eventually_aestronglyMeasurable_heatKernel_mul {α : ℝ} (g : ℝ → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) {x t : ℝ} (ht : 0 < t) : ∀ᶠ (τ : ℝ) in nhds t, MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => heatKernel α (x - y) τ * g y) MeasureTheory.volume

theorem Heat.aestronglyMeasurable_HKt_mul {α x t : ℝ} (g : ℝ → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hα : 0 < α) (ht : 0 < t) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => HKt α (x - y) t * g y) MeasureTheory.volume

theorem Heat.integ_HKt_mul_of_L1 {α : ℝ} (g : ℝ → ℝ) {x t : ℝ} (hα : 0 < α) (ht : 0 < t) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : ℝ) => HKt α (x - y) t * g y) MeasureTheory.volume

theorem Heat.aestronglyMeasurable_HKx_mul {α x t : ℝ} (g : ℝ → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hα : 0 < α) (ht : 0 < t) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => HKx α (x - y) t * g y) MeasureTheory.volume

theorem Heat.integ_HKx_mul_of_L1 {α : ℝ} (g : ℝ → ℝ) {x t : ℝ} (hα : 0 < α) (ht : 0 < t) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : ℝ) => HKx α (x - y) t * g y) MeasureTheory.volume

theorem Heat.aestronglyMeasurable_HKxx_mul {α x t : ℝ} (g : ℝ → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ht : 0 < t) (hα : 0 < α) : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ) => HKxx α (x - y) t * g y) MeasureTheory.volume

theorem Heat.integ_HKxx_mul_of_L1 {α : ℝ} (g : ℝ → ℝ) {x t : ℝ} (hα : 0 < α) (ht : 0 < t) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : ℝ) => HKxx α (x - y) t * g y) MeasureTheory.volume

6. Differentiation under the Integral Sign

We establish the validity of swapping the integral and derivative operators. This requires checking the Dominated Convergence Theorem conditions using the bounds established in Section 4.

theorem Heat.diff_HKt_mul {α x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) : ∀ᵐ (y : ℝ), ∀ τ ∈ Metric.ball t (t / 2), HasDerivAt (fun (τ' : ℝ) => heatKernel α (x - y) τ' * g y) (HKt α (x - y) τ * g y) τ

theorem Heat.diff_HKx_mul {α x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) : ∀ᵐ (y : ℝ), ∀ x' ∈ Metric.ball x 1, HasDerivAt (fun (x'' : ℝ) => heatKernel α (x'' - y) t * g y) (HKx α (x' - y) t * g y) x'

theorem Heat.diff_HKxx_mul {α x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) : ∀ᵐ (y : ℝ), ∀ x' ∈ Metric.ball x 1, HasDerivAt (fun (x'' : ℝ) => HKx α (x'' - y) t * g y) (HKxx α (x' - y) t * g y) x'

theorem Heat.swap_t_heatKernel {α x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : HasDerivAt (fun (τ : ℝ) => ∫ (y : ℝ), heatKernel α (x - y) τ * g y) (∫ (y : ℝ), HKt α (x - y) t * g y) t

Swap the time derivative $\partial_t$ with the integral $\int$.

theorem Heat.swap_x_heatKernel {α x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : HasDerivAt (fun (x' : ℝ) => ∫ (y : ℝ), heatKernel α (x' - y) t * g y) (∫ (y : ℝ), HKx α (x - y) t * g y) x

Swap the spatial derivative $\partial_x$ with the integral $\int$.

theorem Heat.swap_xx_heatKernel {α x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : HasDerivAt (fun (x' : ℝ) => ∫ (y : ℝ), HKx α (x' - y) t * g y) (∫ (y : ℝ), HKxx α (x - y) t * g y) x

Swap the second spatial derivative $\partial_{xx}$ with the integral $\int$.

7. Main Result: The Heat Equation

Finally, we combine the pointwise heat equation property of the kernel with the differentiation-under-integral results to show that the convolution $u(x,t) = (K * g)(x)$ solves the heat equation $u_t = \alpha u_{xx}$.

theorem Heat.heat_from_convolution_heatKernel {t α : ℝ} (g : ℝ → ℝ) (hα : 0 < α) (ht : 0 < t) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (x : ℝ) : deriv (fun (τ : ℝ) => heatConvolutionHK α g x τ) t = α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => heatConvolutionHK α g x'' t) x') x