The generator of the heat semigroup is the Laplacian

Let E be a finite-dimensional real inner product space, F a real Banach space and 1 ≤ p < ∞. The heat semigroup e^{tΔ} on Lᵖ(E; F) (TauCeti.heatSemigroup) is convolution with the heat kernel K_t. This file shows that on functions φ of class C² with compact support its generator is the Laplacian:

(e^{tΔ} φ - φ) / t → Δ φ in Lᵖ as t → 0⁺,

so φ lies in the domain of the generator A and A φ = Δ φ. Here Δ is Mathlib's Laplacian, the sum of the pure second derivatives, so that e^{tΔ} solves ∂ₜu = Δu.

The proof is Duhamel's formula (K_t ⋆ φ)(x) - φ(x) = ∫₀ᵗ (K_s ⋆ Δ φ)(x) ds at every point x (TauCeti.heatKernel_convolution_sub_eq_integral). Integrating over sets of finite measure and exchanging the two integrals lifts this to the identity e^{tΔ} φ - φ = ∫₀ᵗ e^{sΔ} (Δ φ) ds of Lᵖ-valued integrals. The average of the orbit of Δ φ over (0, t] tends to Δ φ by strong continuity (TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_average_orbit_zero).

This identifies the generator only on C² functions with compact support; its full domain is not determined here. For scalar-valued functions and 1 < p < ∞ that domain is the Sobolev space W^{2,p}, by the Calderón–Zygmund estimates, while for p = 1 and dim E ≥ 2 it is strictly larger than W^{2,1}.

Main declarations

• TauCeti.heatSemigroup_sub_eq_integral: the identity e^{tΔ} φ - φ = ∫₀ᵗ e^{sΔ} (Δ φ) ds in Lᵖ, lifting Duhamel's formula TauCeti.heatKernel_convolution_sub_eq_integral, e^{tΔ} φ - φ = ∫₀ᵗ e^{sΔ} (Δ φ) ds.
• TauCeti.tendsto_heatSemigroup_sub: (e^{tΔ} φ - φ) / t → Δ φ in Lᵖ.
• TauCeti.mem_domain_heatSemigroup and TauCeti.generator_heatSemigroup: φ lies in the domain of the generator, which sends it to Δ φ.

References

• L. C. Evans, Partial Differential Equations, Section 2.3.1 (the fundamental solution of the heat equation) and Section 7.4 (semigroup theory).

theorem TauCeti.heatSemigroup_sub_eq_integral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {p : ENNReal} [Fact (1 ≤ p)] {φ : E → F} (hp : p ≠ ⊤) (hφ : ContDiff ℝ 2 φ) (hc : HasCompactSupport φ) {f g : ↥(MeasureTheory.Lp F p MeasureTheory.volume)} (hf : ↑↑f =ᵐ[MeasureTheory.volume] φ) (hg : ↑↑g =ᵐ[MeasureTheory.volume] Laplacian.laplacian φ) {t : ℝ} (ht : 0 < t) : ((heatSemigroup hp).realOperator t) f - f = ∫ (s : ℝ) in Set.Ioc 0 t, ((heatSemigroup hp).realOperator s) g

Duhamel's formula for the heat semigroup. Let φ be of class C² with compact support, and let f, g ∈ Lᵖ be the classes of φ and Δ φ. Then for t > 0, e^{tΔ} f - f = ∫₀ᵗ e^{sΔ} g ds as Lᵖ-valued integrals.

theorem TauCeti.tendsto_heatSemigroup_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {p : ENNReal} [Fact (1 ≤ p)] {φ : E → F} (hp : p ≠ ⊤) (hφ : ContDiff ℝ 2 φ) (hc : HasCompactSupport φ) {f g : ↥(MeasureTheory.Lp F p MeasureTheory.volume)} (hf : ↑↑f =ᵐ[MeasureTheory.volume] φ) (hg : ↑↑g =ᵐ[MeasureTheory.volume] Laplacian.laplacian φ) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • (((heatSemigroup hp).realOperator t) f - f)) (nhdsWithin 0 (Set.Ioi 0)) (nhds g)

The heat semigroup differentiates C² data into its Laplacian. Let φ be of class C² with compact support, and let f, g ∈ Lᵖ be the classes of φ and Δ φ. Then (e^{tΔ} f - f) / t → g in Lᵖ as t → 0⁺.

theorem TauCeti.mem_domain_heatSemigroup {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {p : ENNReal} [Fact (1 ≤ p)] {φ : E → F} (hp : p ≠ ⊤) (hφ : ContDiff ℝ 2 φ) (hc : HasCompactSupport φ) {f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)} (hf : ↑↑f =ᵐ[MeasureTheory.volume] φ) : f ∈ (heatSemigroup hp).domain

C² functions with compact support lie in the domain of the heat generator.

theorem TauCeti.generator_heatSemigroup {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {p : ENNReal} [Fact (1 ≤ p)] {φ : E → F} (hp : p ≠ ⊤) (hφ : ContDiff ℝ 2 φ) (hc : HasCompactSupport φ) {f g : ↥(MeasureTheory.Lp F p MeasureTheory.volume)} (hf : ↑↑f =ᵐ[MeasureTheory.volume] φ) (hg : ↑↑g =ᵐ[MeasureTheory.volume] Laplacian.laplacian φ) : ↑(heatSemigroup hp).generator ⟨f, ⋯⟩ = g

The generator of the heat semigroup is the Laplacian on C² functions with compact support: if f, g ∈ Lᵖ are the classes of φ and Δ φ, then the generator sends f to g.