The time-sliced Wiener functional is the iterated heat–potential product

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

Feynman's finite-slice formula in the Euclidean continuum. For a pre-Brownian motion B, a slice length h > 0, a bounded weight g (think g = e^{−h V}) and a bounded f ∈ L², the time-sliced Wiener functional

W_n(x) = E[ g (x + B_h) · g (x + B_{2h}) ⋯ g (x + B_{nh}) · f (x + B_{nh}) ]

equals, almost everywhere in x, the n-fold operator product ((P_h ∘ M_g)ⁿ f)(x), P_h the heat semigroup and M_g multiplication by g. The sum over paths of the finite-dimensional Matrix.pow_succ_apply_eq_sum_pathWeight becomes an integral over the n intermediate positions of the Brownian path, the one-step amplitude the Gaussian kernel times the weight.

• slicedWiener B P h g f n x — the functional; slicedWiener_zero (W₀ = f);
• integral_prod_of_indepFun — the freezing lemma: for independent X, Y and bounded measurable Ψ, E[Ψ (X, Y)] = E_ω[ E_ω'[Ψ (X ω, Y ω')] ];
• ★ slicedWiener_succ — the Markov step: W_{n+1}^B(x) = ∫ g (x + y) · W_n^{B'}(x + y) dγ_h(y) with B' the process shifted by h (IsPreBrownianReal.shift, indepFun_shift);
• ★★ pow_stepOp_apply_ae_eq_slicedWiener — the time-sliced formula: (P_h ∘ M_g)ⁿ f =ᵐ W_n, by induction on n through the Markov step and the pointwise formula of the heat semigroup.

Honest scope

⚠️ Bounded data. g and f are bounded strongly measurable (and f ∈ L²), so every expectation is of a bounded random variable; the extension to f ∈ L² alone is by continuity in Feynman–Kac (FC-4). On ℝᵈ, for a pre-Brownian motion in ℝᵈ (IsPreBrownianVec, Probability/BrownianVec.lean; one dimension before BACKLOG #41).

References: M. Kac, Trans. AMS 65, 1 (1949); B. Simon, Functional Integration and Quantum Physics, §1; Analysis/Semigroup/HeatSemigroup.lean (FC-2); LinearAlgebra/Matrix/PathSum.lean (the finite-dimensional sum over paths); specs/feynman-continuum-scoping.md (FC-3); specs/BACKLOG.md #36(c).

The freezing lemma

theorem TimeSlicedWiener.integral_prod_of_indepFun {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {𝒳 : Type u_3} {𝒴 : Type u_4} [MeasurableSpace 𝒳] [MeasurableSpace 𝒴] {X : Ω → 𝒳} {Y : Ω → 𝒴} (hXY : ProbabilityTheory.IndepFun X Y P) (hX : AEMeasurable X P) (hY : AEMeasurable Y P) {Ψ : 𝒳 × 𝒴 → ℂ} (hΨ : Measurable Ψ) {C : ℝ} (hC : ∀ (p : 𝒳 × 𝒴), ‖Ψ p‖ ≤ C) : ∫ (ω : Ω), Ψ (X ω, Y ω) ∂P = ∫ (ω : Ω), ∫ (ω' : Ω), Ψ (X ω, Y ω') ∂P ∂P

Freezing an independent variable: for independent X : Ω → 𝒳 and Y : Ω → 𝒴 and a bounded measurable Ψ, E[Ψ (X, Y)] = E_ω[E_ω'[Ψ (X ω, Y ω')]].

The time-sliced Wiener functional

noncomputable def TimeSlicedWiener.slicedWiener {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (B : NNReal → Ω → EuclideanSpace ℝ ι) (h : NNReal) (g f : EuclideanSpace ℝ ι → ℂ) (n : ℕ) (x : EuclideanSpace ℝ ι) : ℂ

The time-sliced Wiener functional: n slices of length h, the weight g sampled at the slice ends and f at the final time.

Equations

• TimeSlicedWiener.slicedWiener P B h g f n x = ∫ (ω : Ω), (∏ k ∈ Finset.range n, g (x + B (↑(k + 1) * h) ω)) * f (x + B (↑n * h) ω) ∂P

theorem TimeSlicedWiener.slicedWiener_zero {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsPreBrownianVec B P) (h : NNReal) (g f : EuclideanSpace ℝ ι → ℂ) (x : EuclideanSpace ℝ ι) : slicedWiener P B h g f 0 x = f x

theorem TimeSlicedWiener.measurable_pathFunctional {ι : Type u_1} [Fintype ι] {g f : EuclideanSpace ℝ ι → ℂ} (hg : Measurable g) (hf : Measurable f) (h : NNReal) (n : ℕ) : Measurable fun (p : EuclideanSpace ℝ ι × (NNReal → EuclideanSpace ℝ ι)) => (∏ k ∈ Finset.range n, g (p.1 + p.2 (↑(k + 1) * h))) * f (p.1 + p.2 (↑n * h))

The path functional of n slices, as a measurable function of the starting point and the path.

theorem TimeSlicedWiener.norm_pathFunctional_le {ι : Type u_1} {g f : EuclideanSpace ℝ ι → ℂ} {Cg Cf : ℝ} (hCg : ∀ (x : EuclideanSpace ℝ ι), ‖g x‖ ≤ Cg) (hCf : ∀ (x : EuclideanSpace ℝ ι), ‖f x‖ ≤ Cf) (h : NNReal) (n : ℕ) (p : EuclideanSpace ℝ ι × (NNReal → EuclideanSpace ℝ ι)) : ‖(∏ k ∈ Finset.range n, g (p.1 + p.2 (↑(k + 1) * h))) * f (p.1 + p.2 (↑n * h))‖ ≤ Cg ^ n * Cf

theorem TimeSlicedWiener.measurable_slicedWiener {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ∀ (t : NNReal), Measurable (B t)) (h : NNReal) {g f : EuclideanSpace ℝ ι → ℂ} (hg : Measurable g) (hf : Measurable f) (n : ℕ) : Measurable (slicedWiener P B h g f n)

x ↦ W_n(x) is measurable.

theorem TimeSlicedWiener.slicedWiener_succ {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsPreBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) (h : NNReal) {g f : EuclideanSpace ℝ ι → ℂ} (hg : Measurable g) (hf : Measurable f) {Cg Cf : ℝ} (hCg : ∀ (x : EuclideanSpace ℝ ι), ‖g x‖ ≤ Cg) (hCf : ∀ (x : EuclideanSpace ℝ ι), ‖f x‖ ≤ Cf) (n : ℕ) (x : EuclideanSpace ℝ ι) : slicedWiener P B h g f (n + 1) x = ∫ (y : EuclideanSpace ℝ ι), g (x + y) * slicedWiener P (fun (t : NNReal) (ω : Ω) => B (h + t) ω - B h ω) h g f n (x + y) ∂HeatSemigroup.gaussian ↑h

★ The Markov step. With B' the process shifted by h, W_{n+1}^B(x) = ∫ g (x + y) · W_n^{B'}(x + y) dγ_h(y).

The operator side

noncomputable def TimeSlicedWiener.stepOp {ι : Type u_1} [Fintype ι] (h : NNReal) (gL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The one-step operator P_h ∘ M_g: multiply by the weight, then diffuse for time h.

Equations

• TimeSlicedWiener.stepOp h gL = HeatSemigroup.heatSemigroup ↑h * HeatSemigroup.potential gL

theorem TimeSlicedWiener.stepOp_apply {ι : Type u_1} [Fintype ι] (h : NNReal) (gL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (v : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (stepOp h gL) v = (HeatSemigroup.heatSemigroup ↑h) ((HeatSemigroup.potential gL) v)

theorem TimeSlicedWiener.ae_gaussian_of_ae {ι : Type u_1} [Fintype ι] {h : NNReal} (hh : 0 < h) {u v : EuclideanSpace ℝ ι → ℂ} (huv : u =ᵐ[MeasureTheory.volume] v) (x : EuclideanSpace ℝ ι) : (fun (y : EuclideanSpace ℝ ι) => u (x + y)) =ᵐ[HeatSemigroup.gaussian ↑h] fun (y : EuclideanSpace ℝ ι) => v (x + y)

An almost-everywhere identity on ℝᵈ holds γ_h-almost everywhere along every translate.

theorem TimeSlicedWiener.pow_stepOp_apply_ae_eq_slicedWiener {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {h : NNReal} (hh : 0 < h) {g f : EuclideanSpace ℝ ι → ℂ} (hg : Measurable g) (hf : Measurable f) {Cg Cf : ℝ} (hCg : ∀ (x : EuclideanSpace ℝ ι), ‖g x‖ ≤ Cg) (hCf : ∀ (x : EuclideanSpace ℝ ι), ‖f x‖ ≤ Cf) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {gL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} (hgL : ↑↑gL =ᵐ[MeasureTheory.volume] g) (n : ℕ) (B : NNReal → Ω → EuclideanSpace ℝ ι) : ProbabilityTheory.IsPreBrownianVec B P → (∀ (t : NNReal), Measurable (B t)) → ↑↑((stepOp h gL ^ n) (MeasureTheory.MemLp.toLp f hf2)) =ᵐ[MeasureTheory.volume] slicedWiener P B h g f n

★★ The time-sliced formula. For every pre-Brownian motion B, slice length h > 0, bounded measurable weight g (with gL its L^∞ class) and bounded measurable f ∈ L²,

((P_h ∘ M_g)ⁿ f)(x) = E[ g (x + B_h) ⋯ g (x + B_{nh}) · f (x + B_{nh}) ] for a.e. x.

Feynman's sum over paths with n slices, in the Euclidean continuum: the operator product on the left, the integral over Brownian paths on the right.