The Feynman–Kac formula

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

Glossary: https://glossary.constraintsurfacedynamics.com/feynman-kac/ Plain-language, CSD-role and formal statements of the Feynman-Kac formula, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

For a Brownian motion B with almost surely continuous paths, a bounded continuous potential V and a bounded f ∈ L²(ℝᵈ),

(e^{−t(H₀ + V)} f)(x) = E[ f (x + B_t) · exp (−∫₀ᵗ V (x + B_s) ds) ] for a.e. x,

where e^{−t(H₀+V)} is the perturbed heat semigroup of HeatSemigroup.lean (the Dyson series around P_t with interaction −V; no generator is written). The Euclidean path integral is a Wiener integral, as Kac stated it in 1949.

The proof joins the two limits of the same time-sliced expression:

• the operator side converges by the Trotter product formula (tendsto_trotter_perturbedHeat), once exp (−h M_V) = M_{e^{−hV}} (★ exp_smul_neg_potential, the exponential of a multiplication operator is multiplication by the exponential);

• the Wiener side is the time-sliced functional of TimeSlicedWiener.lean, whose Riemann sums along the continuous path converge (tendsto_riemannSum) and are dominated;

• the two limits agree because their integrals over every finite-measure set agree (ae_eq_of_forall_setIntegral_eq_of_sigmaFinite).

• expPot hV h — the L^∞ class of e^{−hV}; ★ exp_smul_neg_potential;

• tendsto_riemannSum — Riemann sums of a continuous function on [0, t];

• ★★ feynmanKac — the Feynman–Kac formula.

Honest scope

⚠️ Conditional on a Brownian motion. hB : IsBrownianVec B P (a Brownian motion in ℝᵈ with almost surely continuous paths, Probability/BrownianVec.lean) is a hypothesis; the Mathlib pin does not yet construct one. Bounded continuous V, bounded measurable f ∈ L². The extension to f ∈ L² alone is FeynmanKacL2.lean.

References: M. Kac, On distributions of certain Wiener functionals, Trans. AMS 65, 1 (1949); B. Simon, Functional Integration and Quantum Physics, Thm 6.2; Probability/TimeSlicedWiener.lean (FC-3); Analysis/Semigroup/HeatSemigroup.lean (FC-2); Analysis/Semigroup/BoundedPerturbation.lean (FC-1); specs/feynman-continuum-scoping.md (FC-4); specs/BACKLOG.md #36(c).

The exponential of a multiplication operator

theorem FeynmanKac.coeFn_sum_range {α : Type u_2} {F : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : ENNReal} (u : ℕ → ↥(MeasureTheory.Lp F p μ)) (N : ℕ) : ↑↑(∑ n ∈ Finset.range N, u n) =ᵐ[μ] fun (x : α) => ∑ n ∈ Finset.range N, ↑↑(u n) x

The coercion of a finite sum of Lp elements is the sum of the coercions, almost everywhere.

theorem FeynmanKac.measurable_expFun {ι : Type u_1} {V : EuclideanSpace ℝ ι → ℝ} (hVm : Measurable V) (h : ℝ) : Measurable fun (x : EuclideanSpace ℝ ι) => Complex.exp (-(↑h * ↑(V x)))

theorem FeynmanKac.norm_expFun_le {ι : Type u_1} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) (h : ℝ) (x : EuclideanSpace ℝ ι) : ‖Complex.exp (-(↑h * ↑(V x)))‖ ≤ Real.exp (|h| * CV)

theorem FeynmanKac.memLp_expFun {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} (hVm : Measurable V) {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) (h : ℝ) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => Complex.exp (-(↑h * ↑(V x)))) ⊤ MeasureTheory.volume

noncomputable def FeynmanKac.expPot {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} (hVm : Measurable V) {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) (h : ℝ) : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)

The L^∞ class of e^{−h V}.

Equations

• FeynmanKac.expPot hVm hCV h = MeasureTheory.MemLp.toLp (fun (x : EuclideanSpace ℝ ι) => Complex.exp (-(↑h * ↑(V x)))) ⋯

theorem FeynmanKac.coeFn_expPot {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} (hVm : Measurable V) {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) (h : ℝ) : ↑↑(expPot hVm hCV h) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => Complex.exp (-(↑h * ↑(V x)))

theorem FeynmanKac.neg_potential_pow_apply_ae_eq {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} {VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => ↑(V x)) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (n : ℕ) : ↑↑(((-HeatSemigroup.potential VL) ^ n) f) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => (-↑(V x)) ^ n * ↑↑f x

The powers of the multiplication operator by −V, pointwise.

theorem FeynmanKac.norm_sum_pow_div_factorial_le (c : ℂ) (N : ℕ) : ‖∑ n ∈ Finset.range N, c ^ n / ↑n.factorial‖ ≤ Real.exp ‖c‖

The partial sums of the exponential series are bounded by e^{|c|}.

theorem FeynmanKac.exp_smul_neg_potential {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} (hVm : Measurable V) {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) {VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => ↑(V x)) (h : ℝ) : NormedSpace.exp (h • -HeatSemigroup.potential VL) = HeatSemigroup.potential (expPot hVm hCV h)

★ The exponential of a multiplication operator is multiplication by the exponential: exp (h • (−M_V)) = M_{e^{−hV}} on L².

Riemann sums along a continuous path

theorem FeynmanKac.tendsto_riemannSum (g : ℝ → ℝ) (hg : Continuous g) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => t / ↑n * ∑ k ∈ Finset.range n, g ((↑k + 1) * t / ↑n)) Filter.atTop (nhds (∫ (s : ℝ) in 0..t, g s))

Riemann sums of a continuous function on [0, t] converge to its integral.

The Wiener side

theorem FeynmanKac.prod_exp_eq {ι : Type u_1} {V : EuclideanSpace ℝ ι → ℝ} {Ω : Type u_2} (B : NNReal → Ω → EuclideanSpace ℝ ι) (h : NNReal) (f : EuclideanSpace ℝ ι → ℂ) (n : ℕ) (x : EuclideanSpace ℝ ι) (ω : Ω) : (∏ k ∈ Finset.range n, Complex.exp (-(↑↑h * ↑(V (x + B (↑(k + 1) * h) ω))))) * f (x + B (↑n * h) ω) = Complex.exp (-↑(↑h * ∑ k ∈ Finset.range n, V (x + B (↑(k + 1) * h) ω))) * f (x + B (↑n * h) ω)

The sliced weight is the exponential of a Riemann sum.

theorem FeynmanKac.abs_riemann_le {ι : Type u_1} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) {Ω : Type u_2} (B : NNReal → Ω → EuclideanSpace ℝ ι) {t : NNReal} {n : ℕ} (hn : 0 < n) (x : EuclideanSpace ℝ ι) (ω : Ω) : |↑t / ↑n * ∑ k ∈ Finset.range n, V (x + B (↑(k + 1) * (t / ↑n)) ω)| ≤ ↑t * CV

The Riemann sums of the potential along the path are bounded by t · CV.

theorem FeynmanKac.norm_slicedWiener_le {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (B : NNReal → Ω → EuclideanSpace ℝ ι) (h : NNReal) {g f : EuclideanSpace ℝ ι → ℂ} {Cg Cf : ℝ} (hCg : ∀ (x : EuclideanSpace ℝ ι), ‖g x‖ ≤ Cg) (hCf : ∀ (x : EuclideanSpace ℝ ι), ‖f x‖ ≤ Cf) (n : ℕ) (x : EuclideanSpace ℝ ι) : ‖TimeSlicedWiener.slicedWiener P B h g f n x‖ ≤ Cg ^ n * Cf

The time-sliced functional is bounded by Cg ^ n · Cf.

theorem FeynmanKac.toNNReal_slice (t : NNReal) {n : ℕ} (hn : 0 < n) (k : ℕ) : ((↑k + 1) * ↑t / ↑n).toNNReal = ↑(k + 1) * (t / ↑n)

The index of the k-th slice end, as a nonnegative real.

theorem FeynmanKac.tendsto_riemann_path {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} {Ω : Type u_2} (hVc : Continuous V) {B : NNReal → Ω → EuclideanSpace ℝ ι} {t : NNReal} (ht : 0 < t) (x : EuclideanSpace ℝ ι) {ω : Ω} (hω : Continuous fun (s : NNReal) => B s ω) : Filter.Tendsto (fun (n : ℕ) => ↑t / ↑n * ∑ k ∈ Finset.range n, V (x + B (↑(k + 1) * (t / ↑n)) ω)) Filter.atTop (nhds (∫ (s : ℝ) in 0..↑t, V (x + B s.toNNReal ω)))

Along a continuous path, the Riemann sums of the potential converge to its time integral.

theorem FeynmanKac.tendsto_slicedWiener {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) (hVc : Continuous V) {f : EuclideanSpace ℝ ι → ℂ} (hf : Measurable f) {t : NNReal} (ht : 0 < t) (x : EuclideanSpace ℝ ι) (hfi : MeasureTheory.Integrable (fun (ω : Ω) => f (x + B t ω)) P) : Filter.Tendsto (fun (n : ℕ) => TimeSlicedWiener.slicedWiener P B (t / ↑n) (fun (z : EuclideanSpace ℝ ι) => Complex.exp (-(↑(↑t / ↑n) * ↑(V z)))) f n x) Filter.atTop (nhds (∫ (ω : Ω), Complex.exp (-↑(∫ (s : ℝ) in 0..↑t, V (x + B s.toNNReal ω))) * f (x + B t ω) ∂P))

The Wiener-side limit: along a Brownian motion with continuous paths, the time-sliced functional with weight e^{−(t/n) V} converges to the Feynman–Kac functional, for any measurable f integrable along the endpoint x + B_t (bounded f in particular).

Feynman–Kac

theorem FeynmanKac.feynmanKac {ι : Type u_1} [Fintype ι] {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) (hVc : Continuous V) {VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => ↑(V x)) {f : EuclideanSpace ℝ ι → ℂ} (hf : Measurable f) {Cf : ℝ} (hCf : ∀ (x : EuclideanSpace ℝ ι), ‖f x‖ ≤ Cf) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {t : NNReal} (ht : 0 < t) : ↑↑((HeatSemigroup.perturbedHeat VL ↑t) (MeasureTheory.MemLp.toLp f hf2)) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => ∫ (ω : Ω), Complex.exp (-↑(∫ (s : ℝ) in 0..↑t, V (x + B s.toNNReal ω))) * f (x + B t ω) ∂P

★★ The Feynman–Kac formula. For a Brownian motion B with almost surely continuous paths, a bounded continuous potential V (with VL its L^∞ class) and a bounded measurable f ∈ L²,

(e^{−t(H₀+V)} f)(x) = E[ exp (−∫₀ᵗ V (x + B_s) ds) · f (x + B_t) ] for a.e. x,

where e^{−t(H₀+V)} is the perturbed heat semigroup (the Dyson series around P_t). The Euclidean path integral is a Wiener integral: the operator side is the Trotter limit of the time-sliced products, the Wiener side the limit of the time-sliced functionals, and the two agree on every finite-measure set.