The heat kernel is an approximate identity

For a bounded measurable function g on a finite-dimensional real inner product space E, the function u(t, x) = (K_t ⋆ g)(x), where K_t is the heat kernel, is the candidate solution of the Cauchy problem ∂ₜu = Δu, u(0, ·) = g. This file proves that u attains its initial datum:

• the convolution is bounded by the same constant as g (K_t ⋆ · is an L^∞ contraction);
• if g is continuous at x₀, then u(t, x) → g(x₀) as (t, x) → (0⁺, x₀);
• if g is bounded and uniformly continuous, then K_t ⋆ g → g uniformly as t → 0⁺.

The heat kernel is the dilation K_t(x) = c ^ n K_1(c • x) with c = 1 / √t (TauCeti.heatKernel_eq_mul_heatKernel_one_smul), so as t → 0⁺ its mass concentrates at the origin (TauCeti.tendsto_setIntegral_compl_ball_heatKernel). This follows from Mathlib's peak-function theorem MeasureTheory.tendsto_integral_comp_smul_smul_of_integrable. The three statements above then come from a single estimate, TauCeti.norm_heatKernel_convolution_sub_le, which splits the convolution integral into the parts near and far from the origin.

Mathlib's Real.tendsto_integral_gaussian_smul' is the pointwise limit at a fixed point for an integrable datum, which it needs for Fourier inversion. The Cauchy problem instead takes bounded data, which need not be integrable, and needs the joint limit in (t, x).

Main declarations

• TauCeti.tendsto_setIntegral_compl_ball_heatKernel: the mass of K_t outside any ball about the origin tends to zero as t → 0⁺.
• TauCeti.norm_heatKernel_convolution_le: ‖(K_t ⋆ g)(x)‖ ≤ M when ‖g‖ ≤ M a.e.
• TauCeti.norm_heatKernel_convolution_sub_le: the approximate-identity estimate.
• TauCeti.tendsto_heatKernel_convolution: (K_t ⋆ g)(x) → g(x₀) as (t, x) → (0⁺, x₀) at a point of continuity of g.
• TauCeti.tendstoUniformly_heatKernel_convolution: K_t ⋆ g → g uniformly for bounded uniformly continuous g.

References

• L. C. Evans, Partial Differential Equations, Section 2.3.1, Theorem 1.
• E. M. Stein, G. Weiss, Introduction to Fourier Analysis on Euclidean Spaces, Chapter I, Section 1 (approximate identities).

theorem TauCeti.tendsto_norm_pow_mul_heatKernel_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (k : ℕ) : Filter.Tendsto (fun (x : E) => ‖x‖ ^ k * heatKernel 1 x) (Bornology.cobounded E) (nhds 0)

At unit time the heat kernel decays faster than any power: ‖x‖ ^ k K_1(x) → 0 as ‖x‖ → ∞ for every k. For k = dim E this is the decay hypothesis of Mathlib's peak-function theorem.

theorem TauCeti.tendsto_setIntegral_compl_ball_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {r : ℝ} (hr : 0 < r) : Filter.Tendsto (fun (t : ℝ) => ∫ (z : E) in (Metric.ball 0 r)ᶜ, heatKernel t z) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Concentration of the heat kernel. As t → 0⁺, the mass of K_t outside any ball about the origin tends to zero.

theorem TauCeti.norm_heatKernel_convolution_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) {g : E → F} {M : ℝ} (hM : ∀ᵐ (y : E), ‖g y‖ ≤ M) (x : E) : ‖MeasureTheory.convolution (heatKernel t) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x‖ ≤ M

The heat semigroup is an L^∞ contraction. If ‖g‖ ≤ M almost everywhere, then ‖(K_t ⋆ g)(x)‖ ≤ M for every t > 0 and every x.

theorem TauCeti.norm_heatKernel_convolution_sub_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] {t : ℝ} (ht : 0 < t) {g : E → F} (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) {M : ℝ} (hM : ∀ᵐ (y : E), ‖g y‖ ≤ M) (x : E) (a : F) {r ε : ℝ} (hε₀ : 0 ≤ ε) (hε : ∀ z ∈ Metric.ball 0 r, ‖g (x - z) - a‖ ≤ ε) : ‖MeasureTheory.convolution (heatKernel t) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x - a‖ ≤ ε + (M + ‖a‖) * ∫ (z : E) in (Metric.ball 0 r)ᶜ, heatKernel t z

The approximate-identity estimate for the heat kernel. Let ‖g‖ ≤ M almost everywhere, and suppose ‖g(x - z) - a‖ ≤ ε for all z in the ball of radius r about the origin. Then ‖(K_t ⋆ g)(x) - a‖ ≤ ε + (M + ‖a‖) ∫_{‖z‖ ≥ r} K_t(z) dz.

theorem TauCeti.tendsto_heatKernel_convolution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] {g : E → F} (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) {M : ℝ} (hM : ∀ᵐ (y : E), ‖g y‖ ≤ M) {x₀ : E} (hx₀ : ContinuousAt g x₀) : Filter.Tendsto (fun (p : ℝ × E) => MeasureTheory.convolution (heatKernel p.1) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume p.2) (nhdsWithin 0 (Set.Ioi 0) ×ˢ nhds x₀) (nhds (g x₀))

The initial condition of the heat equation. Let g be measurable and essentially bounded, and continuous at x₀. Then (K_t ⋆ g)(x) → g(x₀) as (t, x) → (0⁺, x₀): the function u(t, x) = (K_t ⋆ g)(x) attains the initial datum g at x₀.

theorem TauCeti.tendstoUniformly_heatKernel_convolution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] (g : BoundedContinuousFunction E F) (hg : UniformContinuous ⇑g) : TendstoUniformly (fun (t : ℝ) => MeasureTheory.convolution (heatKernel t) (⇑g) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) (⇑g) (nhdsWithin 0 (Set.Ioi 0))

Uniform convergence to the initial datum. For a bounded uniformly continuous g, K_t ⋆ g → g uniformly on E as t → 0⁺.