Properties of the Heat Fundamental Solution, Solution to the Initial Value Problem

This file establishes key qualitative properties of the solution formula to the heat equation, involving the convolution of the heat kernel and the initial condition g

Main Results

• heat_maximum_principle: The maximum principle - solutions are bounded by the supremum of the initial data
• heatKernel_IVP_limit_textbook: Continuity property - the solution converges to the initial data as t → 0⁺

Key Lemmas

• heatKernel_mass_one_x_sub_y_even: The solution formula integrates to 1 (translation invariance)
• heatTail_changeOfVariables: Change of variables formula for analyzing kernel tails
• gaussian_tail_bound_by_weighted: Analytical bound on Gaussian tail integrals

Reference

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

Symmetry and Mass Properties

theorem Heat.heatKernel_even {α t : ℝ} (z : ℝ) : heatKernel α (-z) t = heatKernel α z t

The heat kernel is an even function in its spatial argument.

theorem Heat.heatKernel_mass_one_x_sub_y_even {α t : ℝ} (x : ℝ) (hα : 0 < α) (ht : 0 < t) : ∫ (y : ℝ), heatKernel α (x - y) t = 1

Translation Invariance: The heat kernel integrates to 1 regardless of translation. -

The Maximum Principle

noncomputable def Heat.Lmul : ℝ →L[ℝ] ℝ →L[ℝ] ℝ

The Maximum Principle for the Heat Equation

If the initial data g satisfies |g(y)| ≤ B for all y, then the solution at any later time and position also satisfies |u(x,t)| ≤ B.

This fundamental property expresses the fact that the heat equation is a diffusion process that redistributes heat but does not create new temperature extrema. The maximum and minimum temperatures can only decrease over time. -

Equations

• Heat.Lmul = ContinuousLinearMap.mul ℝ ℝ

theorem Heat.heat_maximum_principle {g : ℝ → ℝ} (x : ℝ) {α t B : ℝ} (hα : 0 < α) (ht : 0 < t) (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hBound : ∀ (y : ℝ), |g y| ≤ B) : |heatConvolutionHK α g x t| ≤ B

Gaussian Tail Analysis

This section contains technical lemmas for analyzing the decay of Gaussian tail integrals, which are needed to prove that the solution converges to the initial data as t → 0⁺.

theorem Heat.heatTail_changeOfVariables {α x δ t : ℝ} (hα : 0 < α) (ht : 0 < t) : ∫ (y : ℝ), {y : ℝ | δ ≤ |y - x|}.indicator (fun (y : ℝ) => heatKernel α (x - y) t) y = 1 / √Real.pi * ∫ (z : ℝ), {z : ℝ | δ / √(4 * α * t) ≤ |z|}.indicator (fun (z : ℝ) => Real.exp (-z ^ 2)) z

Change of variables formula for heat kernel tail integrals.

Transforms the integral ∫_{|y-x| ≥ δ} Φ(x-y,t) dy into a standard Gaussian tail integral via the substitution z = (x-y)/√(4αt).

def Heat.IsBoundedAbs (g : ℝ → ℝ) : Prop

Equations

• Heat.IsBoundedAbs g = ∃ (B : ℝ), ∀ (y : ℝ), |g y| ≤ B

theorem Heat.int_z_sq_exp_z_sq : MeasureTheory.Integrable (fun (z : ℝ) => |z| ^ 2 * Real.exp (-z ^ 2)) MeasureTheory.volume

Integrability of z² exp(-z²). Used in Gaussian tail bounds.

theorem Heat.far_measurable (δ x : ℝ) : MeasurableSet {y : ℝ | δ ≤ |y - x|}

The "far" region {y : |y - x| ≥ δ} is measurable.

theorem Heat.integral_split_near_far {α x t : ℝ} (g : ℝ → ℝ) (far : Set ℝ) (hα : 0 < α) (ht : 0 < t) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (h_meas_far : MeasurableSet far) : ∫ (y : ℝ), heatKernel α (x - y) t * (g y - g x) = (∫ (y : ℝ) in farᶜ, heatKernel α (x - y) t * (g y - g x)) + ∫ (y : ℝ) in far, heatKernel α (x - y) t * (g y - g x)

Helper lemma for splitting integrals into near and far regions.

theorem Heat.integral_indicator_tail_even {f : ℝ → ℝ} {R : ℝ} (hR : 0 < R) (heven : ∀ (x : ℝ), f (-x) = f x) (hint : MeasureTheory.IntegrableOn f (Set.Ici R) MeasureTheory.volume) : ∫ (z : ℝ), {z : ℝ | R ≤ |z|}.indicator f z = 2 * ∫ (z : ℝ) in Set.Ici R, f z

For even functions, the two-sided tail integral equals twice the one-sided integral.

theorem Heat.integral_mul_exp_neg_sq_Ici_zero : ∫ (z : ℝ) in Set.Ici 0, z * Real.exp (-z ^ 2) = 1 / 2

Evaluation of ∫₀^∞ z exp(-z²) dz = 1/2.

theorem Heat.gaussian_tail_bound_by_weighted {R : ℝ} (hR : 0 < R) : ∫ (z : ℝ) in Set.Ici R, Real.exp (-z ^ 2) ≤ 1 / R * ∫ (z : ℝ) in Set.Ici 0, z * Real.exp (-z ^ 2)

Key Gaussian tail bound:

This is the analytical estimate that allows us to bound Gaussian tail integrals and prove convergence as t → 0.

Convergence to Initial Data

This section proves that the solution u(x,t) → g(x) as t → 0⁺, establishing that the convolution formula satisfies the initial condition.

theorem Heat.heatKernel_IVP_limit_textbook {α : ℝ} (g : ℝ → ℝ) (x : ℝ) (hα : 0 < α) (g_bounded : IsBoundedAbs g) (g_cont : Continuous g) (g_int : MeasureTheory.Integrable g MeasureTheory.volume) : Filter.Tendsto (fun (t : ℝ) => heatConvolutionHK α g x t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g x))

Main Theorem: The solution converges to the initial data as t → 0⁺

Given bounded, continuous, integrable initial data g, the solution u(x,t) = ∫ Φ(x-y,t) g(y) dy converges to g(x) as t → 0⁺.

Proof Strategy

The proof follows the textbook approach:

1. Rewrite using mass-one property: |u(x,t) - g(x)| = |∫ Φ(x-y,t)[g(y) - g(x)] dy|

2. Split into near and far regions: Choose δ > 0 from continuity of g at x.

   • Near: |y-x| < δ where |g(y) - g(x)| < ε/2
   • Far: |y-x| ≥ δ where we use boundedness

3. Estimate near integral: ∫{near} Φ |g(y) - g(x)| dy ≤ (ε/2) ∫{near} Φ dy ≤ ε/2

4. Estimate far integral using Gaussian tail bounds: ∫{far} Φ |g(y) - g(x)| dy ≤ 2B ∫{far} Φ dy ≤ C√t

5. Choose t small enough: For t < δ₀, have C√t < ε/2, giving total < ε.