The heat semigroup on L²(ℝᵈ) as Gaussian convolution

Category: 1-Mathlib (CSD-free; staged for upstream).

The heat semigroup P_t f = γ_t * f, γ_t the centred Gaussian of variance t, on L²(ℝ, ℂ), built as the Bochner integral of translates: P_t f = ∫ τ_y f dγ_t(y) in L², where τ_y f = f (· + y) is the translation isometry. Every property then comes from the isometry and the probability measure, with no kernel estimate: ‖P_t‖ ≤ 1, P_s P_t = P_{s+t} (Gaussian convolution of measures), strong continuity (the translates move continuously in L², and γ_t concentrates at 0), and P_0 = 1. It is a strongly continuous contraction semigroup in the sense of BoundedPerturbation.lean, so the Dyson series, the Duhamel equation and the Trotter product formula of that module apply to P_t perturbed by a bounded potential.

The Wiener side: the pointwise formula (P_t f)(x) = ∫ f (x + y) dγ_t(y) a.e., and for a pre-Brownian motion B this is E[f (x + B_t)]. No generator is written: −½Δ never appears.

• gaussian t — the Gaussian of variance t (the Dirac mass at 0 for t ≤ 0); gaussian_conv_gaussian — γ_s ∗ γ_t = γ_{s+t};
• translate y : L² →L[ℂ] L² — the translation isometry, continuous_translate_apply, translate_translate;
• heatSemigroup t : L² →L[ℂ] L² — ∫ τ_y f dγ_t(y); norm_heatSemigroup_le, heatSemigroup_of_nonpos, ★ heatSemigroup_add (the semigroup law), ★ continuous_heatSemigroup_apply (strong continuity);
• ★★ isContractionSemigroup_heatSemigroup — the heat semigroup is an IsContractionSemigroup;
• ★ heatSemigroup_apply_ae_eq — the pointwise formula P_t f =ᵐ x ↦ ∫ f (x + y) dγ_t(y), by pairing with indicators of finite-measure sets and Fubini;
• ★ heatConv_eq_integral_brownian — ∫ f (x + y) dγ_t(y) = E[f (x + B_t)] for a pre-Brownian motion;
• potential V — multiplication by a bounded potential V ∈ L^∞ (Mathlib's Hölder pairing); perturbedHeat V t — e^{−t(H₀+V)} as the Dyson series around P_t with interaction −V, a semigroup (perturbedHeat_add) satisfying the Duhamel equation (★ perturbedHeat_eq);
• ★★ tendsto_trotter_perturbedHeat — the Trotter product formula (P_{t/n} · exp (−(t/n) V))ⁿ f → e^{−t(H₀+V)} f: the time-sliced Euclidean path integral in operator form. Feynman–Kac (FC-4) identifies the left side with the Wiener functional.

The wider picture. The same operator e^{−t(H₀+V)} is reached from the Dyson series (perturbation theory), from the Duhamel equation (the evolution equation), and from the Trotter limit (time slicing); with FC-3/FC-4 it is also the Wiener functional (the path integral). One object, four formulations of the same quantum dynamics, each a theorem at the pin.

Honest scope

⚠️ L²(ℝᵈ), ℝᵈ = EuclideanSpace ℝ ι. The Gaussian is the product Gaussian gaussianVec of Probability/BrownianVec.lean (its convolution and scaling laws are read off characteristic functions, Measure.ext_of_charFun), and the Brownian motion is IsPreBrownianVec, d jointly independent real ones (BACKLOG #41, 2026-09-20; one dimension before). Pointwise statements are almost-everywhere statements about L² classes.

References: M. Kac, Trans. AMS 65, 1 (1949); B. Simon, Functional Integration and Quantum Physics, Ch. 1; Analysis/Semigroup/BoundedPerturbation.lean (FC-1); specs/feynman-continuum-scoping.md (FC-2); specs/BACKLOG.md #36(c).

Multiplication operators on L²(E)

noncomputable def HeatSemigroup.potential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Multiplication by a bounded potential V ∈ L^∞ as an operator on L²(E), Mathlib's Hölder pairing L^∞ × L² → L².

Equations

• HeatSemigroup.potential V = (ContinuousLinearMap.holderL MeasureTheory.volume ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ)) V

theorem HeatSemigroup.coeFn_potential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((potential V) f) =ᵐ[MeasureTheory.volume] fun (x : E) => ↑↑V x * ↑↑f x

theorem HeatSemigroup.norm_potential_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) : ‖potential V‖ ≤ ‖V‖

instance HeatSemigroup.instNontrivialL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : Nontrivial ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

L²(E) is nontrivial: the indicator of the unit ball.

The Gaussians

noncomputable def HeatSemigroup.gaussian {ι : Type u_1} [Fintype ι] (t : ℝ) : MeasureTheory.Measure (EuclideanSpace ℝ ι)

The centred Gaussian of variance t in every coordinate; the Dirac mass at 0 for t ≤ 0.

Equations

• HeatSemigroup.gaussian t = ProbabilityTheory.gaussianVec ι t.toNNReal

instance HeatSemigroup.instIsProbabilityMeasureEuclideanSpaceRealGaussian {ι : Type u_1} [Fintype ι] (t : ℝ) : MeasureTheory.IsProbabilityMeasure (gaussian t)

theorem HeatSemigroup.charFun_gaussian {ι : Type u_1} [Fintype ι] (t : ℝ) (ξ : EuclideanSpace ℝ ι) : MeasureTheory.charFun (gaussian t) ξ = Complex.exp (-↑↑t.toNNReal * ↑‖ξ‖ ^ 2 / 2)

theorem HeatSemigroup.gaussian_of_nonpos {ι : Type u_1} [Fintype ι] {t : ℝ} (ht : t ≤ 0) : gaussian t = MeasureTheory.Measure.dirac 0

theorem HeatSemigroup.gaussian_conv_gaussian {ι : Type u_1} [Fintype ι] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : (gaussian s).conv (gaussian t) = gaussian (s + t)

The Gaussians convolve: γ_s ∗ γ_t = γ_{s+t} (characteristic functions).

theorem HeatSemigroup.gaussian_eq_map {ι : Type u_1} [Fintype ι] {t : ℝ} (ht : 0 ≤ t) : gaussian t = MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ ι) => √t • x) (gaussian 1)

The Gaussian of variance t ≥ 0 is the standard Gaussian scaled by √t.

theorem HeatSemigroup.gaussian_absolutelyContinuous {ι : Type u_1} [Fintype ι] {t : ℝ} (ht : 0 < t) : (gaussian t).AbsolutelyContinuous MeasureTheory.volume

The Gaussian of positive variance is absolutely continuous with respect to Lebesgue measure.

Translation on L²

noncomputable def HeatSemigroup.translate {ι : Type u_1} [Fintype ι] (y : EuclideanSpace ℝ ι) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Translation f ↦ f (· + y) as a continuous linear isometry of L²(ℝᵈ).

Equations

• HeatSemigroup.translate y = (MeasureTheory.Lp.compMeasurePreservingₗᵢ ℂ (fun (x : EuclideanSpace ℝ ι) => x + y) ⋯).toContinuousLinearMap

theorem HeatSemigroup.translate_apply {ι : Type u_1} [Fintype ι] (y : EuclideanSpace ℝ ι) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (translate y) f = (MeasureTheory.Lp.compMeasurePreserving (fun (x : EuclideanSpace ℝ ι) => x + y) ⋯) f

theorem HeatSemigroup.coeFn_translate {ι : Type u_1} [Fintype ι] (y : EuclideanSpace ℝ ι) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((translate y) f) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => ↑↑f (x + y)

theorem HeatSemigroup.norm_translate_apply {ι : Type u_1} [Fintype ι] (y : EuclideanSpace ℝ ι) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(translate y) f‖ = ‖f‖

theorem HeatSemigroup.translate_zero {ι : Type u_1} [Fintype ι] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (translate 0) f = f

theorem HeatSemigroup.continuous_translate_apply {ι : Type u_1} [Fintype ι] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Continuous fun (y : EuclideanSpace ℝ ι) => (translate y) f

The translates of an L² function move continuously.

theorem HeatSemigroup.translate_translate {ι : Type u_1} [Fintype ι] (y z : EuclideanSpace ℝ ι) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (translate y) ((translate z) f) = (translate (z + y)) f

Translations compose: τ_y (τ_z f) = τ_{z+y} f.

The heat semigroup

noncomputable def HeatSemigroup.heatIntegral {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The heat operator as the L²-valued Bochner integral of the translates.

Equations

• HeatSemigroup.heatIntegral t f = ∫ (y : EuclideanSpace ℝ ι), (HeatSemigroup.translate y) f ∂HeatSemigroup.gaussian t

theorem HeatSemigroup.integrable_translate {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.Integrable (fun (y : EuclideanSpace ℝ ι) => (translate y) f) (gaussian t)

theorem HeatSemigroup.norm_heatIntegral_le {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖heatIntegral t f‖ ≤ ‖f‖

theorem HeatSemigroup.heatIntegral_add {ι : Type u_1} [Fintype ι] (t : ℝ) (f g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : heatIntegral t (f + g) = heatIntegral t f + heatIntegral t g

theorem HeatSemigroup.heatIntegral_smul {ι : Type u_1} [Fintype ι] (t : ℝ) (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : heatIntegral t (c • f) = c • heatIntegral t f

noncomputable def HeatSemigroup.heatSemigroup {ι : Type u_1} [Fintype ι] (t : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The heat semigroup P_t f = ∫ τ_y f dγ_t(y) as a continuous linear map on L²(ℝᵈ).

Equations

• HeatSemigroup.heatSemigroup t = { toFun := HeatSemigroup.heatIntegral t, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem HeatSemigroup.heatSemigroup_apply {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (heatSemigroup t) f = ∫ (y : EuclideanSpace ℝ ι), (translate y) f ∂gaussian t

theorem HeatSemigroup.norm_heatSemigroup_le {ι : Type u_1} [Fintype ι] (t : ℝ) : ‖heatSemigroup t‖ ≤ 1

theorem HeatSemigroup.norm_heatSemigroup_apply_le {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(heatSemigroup t) f‖ ≤ ‖f‖

theorem HeatSemigroup.heatSemigroup_of_nonpos {ι : Type u_1} [Fintype ι] {t : ℝ} (ht : t ≤ 0) : heatSemigroup t = 1

theorem HeatSemigroup.heatSemigroup_max {ι : Type u_1} [Fintype ι] (t : ℝ) : heatSemigroup t = heatSemigroup (max t 0)

theorem HeatSemigroup.heatSemigroup_add {ι : Type u_1} [Fintype ι] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : heatSemigroup (s + t) = heatSemigroup s * heatSemigroup t

★ The semigroup law: P_{s+t} = P_s P_t for s, t ≥ 0, by Gaussian convolution.

Strong continuity

theorem HeatSemigroup.heatSemigroup_apply_sub_eq {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (heatSemigroup t) f - f = ∫ (y : EuclideanSpace ℝ ι), (translate y) f - f ∂gaussian t

theorem HeatSemigroup.norm_heatSemigroup_apply_sub_le {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(heatSemigroup t) f - f‖ ≤ ∫ (y : EuclideanSpace ℝ ι), ‖(translate y) f - f‖ ∂gaussian t

theorem HeatSemigroup.tendsto_integral_norm_translate_sub {ι : Type u_1} [Fintype ι] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Filter.Tendsto (fun (t : ℝ) => ∫ (y : EuclideanSpace ℝ ι), ‖(translate y) f - f‖ ∂gaussian t) (nhdsWithin 0 (Set.Ici 0)) (nhds 0)

The Gaussians concentrate at 0: ∫ ‖τ_y f − f‖ dγ_t(y) → 0 as t → 0⁺.

theorem HeatSemigroup.norm_heatSemigroup_apply_sub_apply_le {ι : Type u_1} [Fintype ι] {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(heatSemigroup a) f - (heatSemigroup b) f‖ ≤ ‖(heatSemigroup (b - a)) f - f‖

For 0 ≤ a ≤ b, ‖P_a f − P_b f‖ ≤ ‖P_{b−a} f − f‖.

theorem HeatSemigroup.continuous_heatSemigroup_apply {ι : Type u_1} [Fintype ι] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Continuous fun (t : ℝ) => (heatSemigroup t) f

★ Strong continuity: t ↦ P_t f is continuous for every f ∈ L².

theorem HeatSemigroup.isContractionSemigroup_heatSemigroup {ι : Type u_1} [Fintype ι] : IsContractionSemigroup heatSemigroup

★★ The heat semigroup is a strongly continuous contraction semigroup in the sense of BoundedPerturbation.lean: the Dyson series, the Duhamel equation and the Trotter product formula apply to it perturbed by any bounded operator.

The pointwise formula

noncomputable def HeatSemigroup.heatConv {ι : Type u_1} [Fintype ι] (t : ℝ) (f : EuclideanSpace ℝ ι → ℂ) (x : EuclideanSpace ℝ ι) : ℂ

The Wiener functional x ↦ ∫ f (x + y) dγ_t(y).

Equations

• HeatSemigroup.heatConv t f x = ∫ (y : EuclideanSpace ℝ ι), f (x + y) ∂HeatSemigroup.gaussian t

theorem HeatSemigroup.aestronglyMeasurable_shift {ι : Type u_1} [Fintype ι] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (t : ℝ) : MeasureTheory.AEStronglyMeasurable (fun (p : EuclideanSpace ℝ ι × EuclideanSpace ℝ ι) => ↑↑f (p.1 + p.2)) (MeasureTheory.volume.prod (gaussian t))

theorem HeatSemigroup.integrable_shift_prod {ι : Type u_1} [Fintype ι] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (t : ℝ) {s : Set (EuclideanSpace ℝ ι)} (hμs : MeasureTheory.volume s < ⊤) : MeasureTheory.Integrable (fun (p : EuclideanSpace ℝ ι × EuclideanSpace ℝ ι) => ↑↑f (p.1 + p.2)) ((MeasureTheory.volume.restrict s).prod (gaussian t))

theorem HeatSemigroup.integrableOn_heatConv {ι : Type u_1} [Fintype ι] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (t : ℝ) {s : Set (EuclideanSpace ℝ ι)} (hμs : MeasureTheory.volume s < ⊤) : MeasureTheory.IntegrableOn (heatConv t ↑↑f) s MeasureTheory.volume

theorem HeatSemigroup.heatSemigroup_apply_ae_eq {ι : Type u_1} [Fintype ι] (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((heatSemigroup t) f) =ᵐ[MeasureTheory.volume] heatConv t ↑↑f

★ The pointwise formula: P_t f =ᵐ x ↦ ∫ f (x + y) dγ_t(y). The L²-valued Bochner integral of the translates and the Wiener functional agree almost everywhere, by pairing with the indicators of finite-measure sets and Fubini.

The Wiener side

theorem HeatSemigroup.heatConv_eq_integral_brownian {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsPreBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : ℝ} (ht : 0 < t) {f : EuclideanSpace ℝ ι → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (x : EuclideanSpace ℝ ι) : heatConv t f x = ∫ (ω : Ω), f (x + B t.toNNReal ω) ∂P

★ For a pre-Brownian motion B in ℝᵈ and t > 0, the Wiener functional is the expectation ∫ f (x + y) dγ_t(y) = E[f (x + B_t)].

Bounded potentials and the perturbed heat semigroup

noncomputable def HeatSemigroup.perturbedHeat {ι : Type u_1} [Fintype ι] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (t : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The perturbed heat semigroup e^{−t(H₀ + V)} for a bounded potential V: the Dyson series of BoundedPerturbation.lean around P_t with interaction −V. No generator is written.

Equations

• HeatSemigroup.perturbedHeat V t = ⋯.perturbed (-HeatSemigroup.potential V) t

theorem HeatSemigroup.perturbedHeat_apply {ι : Type u_1} [Fintype ι] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (perturbedHeat V t) f = ContractionSemigroup.dysonSum heatSemigroup (-potential V) t f

theorem HeatSemigroup.perturbedHeat_add {ι : Type u_1} [Fintype ι] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : perturbedHeat V (t + s) = perturbedHeat V t * perturbedHeat V s

The perturbed heat semigroup is a semigroup.

theorem HeatSemigroup.perturbedHeat_eq {ι : Type u_1} [Fintype ι] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) {t : ℝ} (ht : 0 ≤ t) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (perturbedHeat V t) f = (heatSemigroup t) f - ∫ (s : ℝ) in 0..t, (heatSemigroup (t - s)) ((potential V) ((perturbedHeat V s) f))

★ The Duhamel equation of the perturbed heat semigroup: e^{−t(H₀+V)} f = P_t f − ∫₀ᵗ P_{t−s} (V · e^{−s(H₀+V)} f) ds.

theorem HeatSemigroup.tendsto_trotter_perturbedHeat {ι : Type u_1} [Fintype ι] (V : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) {t : ℝ} (ht : 0 ≤ t) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Filter.Tendsto (fun (n : ℕ) => (ContractionSemigroup.trotterStep heatSemigroup (-potential V) (t / ↑n) ^ n) f) Filter.atTop (nhds ((perturbedHeat V t) f))

★★ The Trotter product formula for the heat semigroup with a bounded potential: (P_{t/n} · exp (−(t/n) V))ⁿ f → e^{−t(H₀+V)} f. This is the time-sliced Euclidean path integral in operator form; Feynman–Kac (FC-4) identifies the left side with a Wiener functional.