The heat semigroup on Lᵖ

On a finite-dimensional real inner product space E of dimension n, convolution with the heat kernel K_t(x) = (4πt)^(-n/2) exp(-‖x‖² / (4t)) defines, for 1 ≤ p < ∞, the heat semigroup e^{tΔ} on Lᵖ(E; F) with values in a real Banach space F:

e^{tΔ} f = K_t ⋆ f = ∫ y, K_t(y) • f(· - y) dy for t > 0, and e^{0Δ} f = f.

This file proves that it is a strongly continuous contraction semigroup:

• each e^{tΔ} is a contraction of Lᵖ, by Young's inequality, because K_t ≥ 0 has mass one;
• e^{(s+t)Δ} = e^{sΔ} e^{tΔ}, from the Chapman–Kolmogorov identity K_s ⋆ K_t = K_{s+t} and associativity of convolution on Lᵖ;
• e^{tΔ} f → f in Lᵖ as t → 0⁺: the heat kernel is an approximate identity, applied to the continuous bounded Lᵖ-valued orbit y ↦ f(· + y) of translations.

For t > 0 the class e^{tΔ} f is represented almost everywhere by the classical convolution K_t ⋆ f; for essentially bounded f, TauCeti.hasDerivAt_heatKernel_convolution shows that this convolution is smooth and solves the heat equation pointwise. The generator of the semigroup, the Laplacian on Lᵖ with its natural domain, is not identified in this file.

The restriction p < ∞ is essential: on L^∞ the operators are still contractions, but the semigroup is not strongly continuous at 0.

Main declarations

• TauCeti.tendsto_convolutionLp_heatKernel: K_t ⋆ f → f in Lᵖ as t → 0⁺.
• TauCeti.heatSemigroup: the heat semigroup on Lᵖ, as a ContractionSemigroup.
• TauCeti.heatSemigroup_apply, TauCeti.heatSemigroup_apply_apply: for t ≠ 0, the operator at time t is convolution with K_t.
• TauCeti.heatSemigroup_zero: the operator at time 0 is the identity.
• TauCeti.heatSemigroup_ae_eq_convolution: for t ≠ 0, e^{tΔ} f is represented almost everywhere by the classical convolution K_t ⋆ f.

References

• L. C. Evans, Partial Differential Equations, Section 2.3.1.
• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Chapter II, 2.12 (the diffusion semigroup).

theorem TauCeti.tendsto_convolutionLp_heatKernel {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (hp : p ≠ ⊤) (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)) : Filter.Tendsto (fun (t : ℝ) => (convolutionLp hp (heatKernel t) MeasureTheory.volume) f) (nhdsWithin 0 (Set.Ioi 0)) (nhds f)

The heat kernel is an approximate identity on Lᵖ. For 1 ≤ p < ∞ and f ∈ Lᵖ, K_t ⋆ f → f in Lᵖ as t → 0⁺.

noncomputable def TauCeti.heatSemigroup {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (hp : p ≠ ⊤) : Semigroups.ContractionSemigroup ↥(MeasureTheory.Lp F p MeasureTheory.volume)

The heat semigroup e^{tΔ} on Lᵖ(E; F) for 1 ≤ p < ∞: the identity at time 0, and convolution with the heat kernel K_t at time t > 0 (TauCeti.heatSemigroup_apply). It is a strongly continuous contraction semigroup.

@[simp]

theorem TauCeti.heatSemigroup_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (hp : p ≠ ⊤) : (heatSemigroup hp) 0 = ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p MeasureTheory.volume)

At time 0 the heat semigroup is the identity.

theorem TauCeti.heatSemigroup_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (hp : p ≠ ⊤) {t : NNReal} (ht : t ≠ 0) : (heatSemigroup hp) t = convolutionLp hp (heatKernel ↑t) MeasureTheory.volume

At a positive time t the heat semigroup is convolution with the heat kernel K_t.

theorem TauCeti.heatSemigroup_apply_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (hp : p ≠ ⊤) {t : NNReal} (ht : t ≠ 0) (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)) : ((heatSemigroup hp) t) f = ∫ (y : E), heatKernel (↑t) y • (MeasureTheory.volume.translateLp p (-y)) f

At a positive time t the heat semigroup sends f to the Lᵖ-valued integral ∫ y, K_t(y) • f(· - y) dy.

theorem TauCeti.heatSemigroup_ae_eq_convolution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (hp : p ≠ ⊤) {t : NNReal} (ht : t ≠ 0) {f : E → F} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ↑↑(((heatSemigroup hp) t) (MeasureTheory.MemLp.toLp f hf)) =ᵐ[MeasureTheory.volume] MeasureTheory.convolution (heatKernel ↑t) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

At a positive time t, the heat semigroup applied to the class of f ∈ Lᵖ is represented almost everywhere by the classical heat convolution (K_t ⋆ f)(x) = ∫ y, K_t(y) • f(x - y) dy.

theorem TauCeti.heatSemigroup_ae_eq_convolution_coeFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (hp : p ≠ ⊤) {t : NNReal} (ht : t ≠ 0) (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)) : ↑↑(((heatSemigroup hp) t) f) =ᵐ[MeasureTheory.volume] MeasureTheory.convolution (heatKernel ↑t) (↑↑f) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

At a positive time t, the heat semigroup applied to f : Lp is represented almost everywhere by convolution of the heat kernel with the chosen representative of f.