The Laplacian as the heat generator in the supremum norm

A bounded uniformly continuous C² function with bounded first and second derivatives and uniformly continuous Laplacian belongs to the domain of the heat generator on bounded uniformly continuous functions. The generator sends it to its Laplacian, with Mathlib's sign convention ∂ₜu = Δu.

heatSemigroupBUC_sub_eq_integral is Duhamel's identity in the Banach space of bounded uniformly continuous functions. Strong continuity applied to the Laplacian gives convergence of the time difference quotients in supremum norm. No compact support is required, and this file does not characterize the full generator domain.

References

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

theorem TauCeti.heatSemigroupBUC_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] {f g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)} {M₁ M₂ : ℝ} (hf : ContDiff ℝ 2 ⇑↑f) (h₁ : ∀ (y : E), ‖fderiv ℝ (⇑↑f) y‖ ≤ M₁) (h₂ : ∀ (y : E), ‖fderiv ℝ (fderiv ℝ ⇑↑f) y‖ ≤ M₂) (hg : Laplacian.laplacian ⇑↑f = ⇑↑g) {t : ℝ} (ht : 0 < t) : (heatSemigroupBUC.realOperator t) f - f = ∫ (s : ℝ) in Set.Ioc 0 t, (heatSemigroupBUC.realOperator s) g

Duhamel's identity in supremum norm. For bounded uniformly continuous C² data f with bounded first and second derivatives and bounded uniformly continuous Laplacian g, e^{tΔ} f - f = ∫₀ᵗ e^{sΔ} g ds as a Banach-valued integral.

theorem TauCeti.tendsto_heatSemigroupBUC_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] {f g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)} {M₁ M₂ : ℝ} (hf : ContDiff ℝ 2 ⇑↑f) (h₁ : ∀ (y : E), ‖fderiv ℝ (⇑↑f) y‖ ≤ M₁) (h₂ : ∀ (y : E), ‖fderiv ℝ (fderiv ℝ ⇑↑f) y‖ ≤ M₂) (hg : Laplacian.laplacian ⇑↑f = ⇑↑g) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((heatSemigroupBUC.realOperator t) f - f)) (nhdsWithin 0 (Set.Ioi 0)) (nhds g)

The time difference quotients of the heat orbit converge to the Laplacian in supremum norm for bounded C² data with bounded first and second derivatives and uniformly continuous Laplacian.

theorem TauCeti.mem_domain_heatSemigroupBUC {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)} {M₁ M₂ : ℝ} (hf : ContDiff ℝ 2 ⇑↑f) (h₁ : ∀ (y : E), ‖fderiv ℝ (⇑↑f) y‖ ≤ M₁) (h₂ : ∀ (y : E), ‖fderiv ℝ (fderiv ℝ ⇑↑f) y‖ ≤ M₂) (hg : Laplacian.laplacian ⇑↑f = ⇑↑g) : f ∈ heatSemigroupBUC.domain

Bounded uniformly continuous C² data with bounded first and second derivatives and bounded uniformly continuous Laplacian lie in the domain of the heat generator.

theorem TauCeti.generator_heatSemigroupBUC {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)} {M₁ M₂ : ℝ} (hf : ContDiff ℝ 2 ⇑↑f) (h₁ : ∀ (y : E), ‖fderiv ℝ (⇑↑f) y‖ ≤ M₁) (h₂ : ∀ (y : E), ‖fderiv ℝ (fderiv ℝ ⇑↑f) y‖ ≤ M₂) (hg : Laplacian.laplacian ⇑↑f = ⇑↑g) : ↑heatSemigroupBUC.generator ⟨f, ⋯⟩ = g

The heat generator is the Laplacian on bounded uniformly continuous C² functions with bounded first and second derivatives and bounded uniformly continuous Laplacian.