The Heat Kernel and the 1D Heat Equation

Main Definitions

• heatKernel α x t: The fundamental solution to the 1D heat equation with diffusivity α
• heatK α: Helper constant 4πα appearing in the normalization
• a α t: Helper function 1/(4αt) appearing in the exponential
• c α t: Normalization constant 1/√(4παt)

Main Results

• heatKernel_pos: The heat kernel is strictly positive for all x when α > 0 and t > 0
• integral_heatKernel_one_gaussian: The heat kernel integrates to one (normalization property)
• heatKernel_solves_heat_eq: The heat kernel satisfies the heat equation ∂u/∂t = α ∂²u/∂x²

Reference

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

Core Definitions

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

The one-dimensional heat kernel (fundamental solution) with diffusivity α.

For α > 0 and t > 0, this function gives the temperature distribution at time t resulting from a unit point source at x = 0 at time t = 0.

Equations

• Heat.heatKernel α x t = 1 / √(4 * Real.pi * α * t) * Real.exp (-x ^ 2 / (4 * α * t))

noncomputable def Heat.heatK (α : ℝ) : ℝ

Helper constant k = 4πα used in the normalization factor.

Equations

• Heat.heatK α = 4 * Real.pi * α

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

The coefficient a(α,t) = 1/(4αt) appearing in the exponential term.

Equations

• Heat.a α t = 1 / (4 * α * t)

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

The normalization constant c(α,t) = 1/√(4παt).

Equations

• Heat.c α t = 1 / √(Heat.heatK α * t)

Basic Properties and Positivity

theorem Heat.heatK_pos {α : ℝ} (hα : α > 0) : heatK α > 0

theorem Heat.a_pos {α t : ℝ} (hα : α > 0) (ht : t > 0) : a α t > 0

theorem Heat.c_pos {α t : ℝ} (hα : α > 0) (ht : t > 0) : c α t > 0

theorem Heat.heatKernel_pos (α t : ℝ) {x : ℝ} (hα : 0 < α) (ht : 0 < t) : 0 < heatKernel α x t

Property 1: The heat kernel is strictly positive for all x when α > 0 and t > 0.

Normalization Property

theorem Heat.integral_heatKernel_one_gaussian (α t : ℝ) (hα : 0 < α) (ht : 0 < t) : ∫ (x : ℝ), heatKernel α x t = 1

Property 2: The heat kernel integrates to one over all of ℝ.

This shows that the heat kernel is properly normalized and can be interpreted as a probability density function (specifically, a Gaussian distribution).

Derivative Lemmas

We establish the derivatives of the heat kernel with respect to both space and time variables. These are needed to verify that the heat kernel satisfies the heat equation.

Helper Lemmas for Derivatives

theorem Heat.deriv_sqrt_inv {x : ℝ} (hx : x > 0) : HasDerivAt (fun (τ : ℝ) => 1 / √τ) (-(1 / (2 * x)) * (1 / √x)) x

Derivative of 1/√x at a positive point.

theorem Heat.deriv_exp_heatKernel {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) : HasDerivAt (fun (x' : ℝ) => Real.exp (-x' ^ 2 / (4 * α * t))) (-(1 / (4 * α * t)) * (2 * x) * Real.exp (-x ^ 2 / (4 * α * t))) x

Derivative of the exponential term exp(-(x²)/(4αt)) with respect to x.

Time Derivative

theorem Heat.hasDerivAt_heatKernel_t (α : ℝ) (hα : 0 < α) {t x : ℝ} (ht : 0 < t) : HasDerivAt (fun (τ : ℝ) => heatKernel α x τ) (-(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))) t

The time derivative of the heat kernel ∂/∂t heatKernel(α, x, t).

First Spatial Derivative

theorem Heat.hasDerivAt_heatKernel_x {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) : HasDerivAt (fun (x' : ℝ) => heatKernel α x' t) (1 / √(4 * Real.pi * α * t) * (-(1 / (4 * α * t)) * (2 * x)) * Real.exp (-x ^ 2 / (4 * α * t))) x

The first spatial derivative of the heat kernel ∂/∂x heatKernel(α, x, t).

Second Spatial Derivative

theorem Heat.hasDerivAt_heatKernel_x_x {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) : HasDerivAt (fun (x' : ℝ) => 1 / √(4 * Real.pi * α * t) * (-(1 / (4 * α * t)) * (2 * x')) * Real.exp (-x' ^ 2 / (4 * α * 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)))) x

Auxiliary lemma: derivative of the first spatial derivative's formula.

theorem Heat.hasDerivAt_heatKernel_xx {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) : HasDerivAt (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => heatKernel α x'' t) x') (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)))) x

The second spatial derivative of the heat kernel ∂²/∂x² heatKernel(α, x, t).

Main Theorem: The Heat Equation

The heat kernel satisfies the one-dimensional heat equation ∂u/∂t = α ∂²u/∂x². This is the fundamental property that makes it the fundamental solution to the heat equation.

theorem Heat.heatKernel_solves_heat_eq (α : ℝ) (hα : 0 < α) {t x : ℝ} (ht : 0 < t) : deriv (fun (τ : ℝ) => heatKernel α x τ) t = α * deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => heatKernel α x'' t) x') x

Main Theorem: The heat kernel satisfies the heat equation.

For any `α > 0`, `t > 0`, and `x ∈ ℝ`, we have:

    ∂/∂t heatKernel(α, x, t) = α * ∂²/∂x² heatKernel(α, x, t)

This establishes that the heat kernel is indeed the fundamental solution
to the one-dimensional heat equation. 

Property 4: Convergence to Dirac Delta

As t → 0⁺, the heat kernel heatKernel(α, x, t) concentrates at the origin and converges to the Dirac delta distribution δ₀ in the sense of distributions.

More precisely, for any test funciton φ(x)

lim_{t → 0⁺} ∫ heatKernel(α, x, t) · φ(x) dx = φ(0)

This property explains why the heat kernel serves as the fundamental solution: it represents the evolution of an initial point source of heat at x = 0.

Formal proof: See Section [7.2.3] for the complete formalization of this convergence result.