The Feynman–Kac formula on all of L²

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

Probability/FeynmanKac.lean proves Kac's formula for bounded measurable f ∈ L². This module removes the boundedness (BACKLOG #42, FC-4′): for every g ∈ L²(ℝᵈ),

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

(★★ feynmanKac_Lp), the right side being the Feynman–Kac functional fkFunctional, which is well defined for a.e. x because ω ↦ g (x + B_t ω) is P-integrable for a.e. x (ae_integrable_shift: the joint integrability of (x, y) ↦ g (x + y) on finite-measure sets against the Gaussian, from HeatSemigroup.lean, sliced by Fubini and pushed through the law of B_t).

Design

Both sides are continuous in g and agree on the simple functions, which are dense in L² (Lp.simpleFunc.denseRange); the identification is made on every finite-measure set A:

• the operator side is bounded, ‖∫_A e^{−t(H₀+V)} h‖ ≤ ‖1_A‖ ‖e^{−t(H₀+V)}‖ ‖h‖;
• ★ the Wiener side is bounded by the heat semigroup of |h|: ‖∫_A fk h‖ ≤ e^{t‖V‖} ∫_A E‖h (x + B_t)‖ dx, and x ↦ E‖h (x + B_t)‖ is P_t |h| almost everywhere (absConv_ae_eq, through the pointwise formula of HeatSemigroup.lean and the law of B_t), so the integral is at most ‖1_A‖ ‖h‖ by Cauchy–Schwarz and contraction (setIntegral_absConv_le, norm_setIntegral_fkFunctional_le);
• so ‖∫_A (e^{−t(H₀+V)} g − fk g)‖ ≤ K_A ‖g − s‖ for every simple s, hence = 0.

The measurability of fkFunctional g comes for free from FeynmanKac.tendsto_slicedWiener, generalised there to any f integrable along the endpoint: fk g is an a.e. pointwise limit of the measurable sliced functionals.

• fkFunctional V P B t f x — the functional; fkFunctional_congr_ae — it depends only on the a.e.-class of f (the endpoint has a Gaussian law);
• aestronglyMeasurable_weight — the path integral of the potential is a.e.-measurable in ω (a limit of Riemann sums along the a.s. continuous paths), integrable_weight_mul;
• ★ absConv_ae_eq — E‖g (x + B_t)‖ = (P_t |g|)(x) for a.e. x;
• ★★ feynmanKac_Lp — Feynman–Kac for every g ∈ L².

Honest scope

⚠️ Conditional on a Brownian motion in ℝᵈ (hB : IsBrownianVec B P), bounded continuous V, t > 0; as in FeynmanKac.lean.

References: M. Kac, Trans. AMS 65, 1 (1949); B. Simon, Functional Integration and Quantum Physics, Thm 6.2; Probability/FeynmanKac.lean (FC-4); specs/feynman-continuum-scoping.md §4; specs/BACKLOG.md #42; specs/future-work.md FP-1.

The functional

noncomputable def FeynmanKac.weight {ι : Type u_1} {Ω : Type u_2} (V : EuclideanSpace ℝ ι → ℝ) (B : NNReal → Ω → EuclideanSpace ℝ ι) (t : NNReal) (x : EuclideanSpace ℝ ι) (ω : Ω) : ℂ

The Feynman–Kac weight exp (−∫₀ᵗ V (x + B_s) ds).

Equations

• FeynmanKac.weight V B t x ω = Complex.exp (-↑(∫ (s : ℝ) in 0..↑t, V (x + B s.toNNReal ω)))

noncomputable def FeynmanKac.fkFunctional {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (V : EuclideanSpace ℝ ι → ℝ) (P : MeasureTheory.Measure Ω) (B : NNReal → Ω → EuclideanSpace ℝ ι) (t : NNReal) (f : EuclideanSpace ℝ ι → ℂ) (x : EuclideanSpace ℝ ι) : ℂ

The Feynman–Kac functional E[exp (−∫₀ᵗ V (x + B_s) ds) · f (x + B_t)].

Equations

• FeynmanKac.fkFunctional V P B t f x = ∫ (ω : Ω), FeynmanKac.weight V B t x ω * f (x + B t ω) ∂P

theorem FeynmanKac.norm_weight_le {ι : Type u_1} {Ω : Type u_2} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) (B : NNReal → Ω → EuclideanSpace ℝ ι) (t : NNReal) (x : EuclideanSpace ℝ ι) (ω : Ω) : ‖weight V B t x ω‖ ≤ Real.exp (↑t * CV)

theorem FeynmanKac.aestronglyMeasurable_pathIntegral {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} (hVc : Continuous V) {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (x : EuclideanSpace ℝ ι) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (s : ℝ) in 0..↑t, V (x + B s.toNNReal ω)) P

The path integral of the potential is a.e.-strongly measurable in ω: a limit of Riemann sums along the almost surely continuous paths.

theorem FeynmanKac.aestronglyMeasurable_weight {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} (hVc : Continuous V) {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (x : EuclideanSpace ℝ ι) : MeasureTheory.AEStronglyMeasurable (weight V B t x) P

theorem FeynmanKac.integrable_weight_mul {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) (hVc : Continuous V) {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) {f : EuclideanSpace ℝ ι → ℂ} {x : EuclideanSpace ℝ ι} (hfi : MeasureTheory.Integrable (fun (ω : Ω) => f (x + B t ω)) P) : MeasureTheory.Integrable (fun (ω : Ω) => weight V B t x ω * f (x + B t ω)) P

theorem FeynmanKac.fkFunctional_congr_ae {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) {f₁ f₂ : EuclideanSpace ℝ ι → ℂ} (h : f₁ =ᵐ[MeasureTheory.volume] f₂) (x : EuclideanSpace ℝ ι) : fkFunctional V P B t f₁ x = fkFunctional V P B t f₂ x

The functional depends only on the a.e.-class of f: for t > 0 the endpoint x + B_t has a Gaussian law.

Integrability along the endpoint, and the averaged modulus

theorem FeynmanKac.ae_integrable_shift {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) (t : NNReal) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∀ᵐ (x : EuclideanSpace ℝ ι), MeasureTheory.Integrable (fun (ω : Ω) => ↑↑g (x + B t ω)) P

For g ∈ L², ω ↦ g (x + B_t ω) is integrable for almost every x.

noncomputable def FeynmanKac.absL {ι : Type u_1} [Fintype ι] (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

|g| as an element of L².

Equations

• FeynmanKac.absL g = MeasureTheory.MemLp.toLp (fun (x : EuclideanSpace ℝ ι) => ↑‖↑↑g x‖) ⋯

theorem FeynmanKac.coeFn_absL {ι : Type u_1} [Fintype ι] (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑(absL g) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => ↑‖↑↑g x‖

theorem FeynmanKac.norm_absL {ι : Type u_1} [Fintype ι] (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖absL g‖ = ‖g‖

theorem FeynmanKac.heatConv_congr_ae {ι : Type u_1} [Fintype ι] {t : ℝ} (ht : 0 < t) {f₁ f₂ : EuclideanSpace ℝ ι → ℂ} (h : f₁ =ᵐ[MeasureTheory.volume] f₂) (x : EuclideanSpace ℝ ι) : HeatSemigroup.heatConv t f₁ x = HeatSemigroup.heatConv t f₂ x

The heat convolution depends only on the a.e.-class of the function (t > 0).

theorem FeynmanKac.absConv_ae_eq {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (fun (x : EuclideanSpace ℝ ι) => ↑(∫ (ω : Ω), ‖↑↑g (x + B t ω)‖ ∂P)) =ᵐ[MeasureTheory.volume] ↑↑((HeatSemigroup.heatSemigroup ↑t) (absL g))

★ The averaged modulus is the heat semigroup of |g|: E‖g (x + B_t)‖ = (P_t |g|)(x) for almost every x.

theorem FeynmanKac.integrableOn_absConv {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {A : Set (EuclideanSpace ℝ ι)} (hμA : MeasureTheory.volume A < ⊤) : MeasureTheory.IntegrableOn (fun (x : EuclideanSpace ℝ ι) => ∫ (ω : Ω), ‖↑↑g (x + B t ω)‖ ∂P) A MeasureTheory.volume

theorem FeynmanKac.setIntegral_absConv_le {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {A : Set (EuclideanSpace ℝ ι)} (hA : MeasurableSet A) (hμA : MeasureTheory.volume A < ⊤) : ∫ (x : EuclideanSpace ℝ ι) in A, ∫ (ω : Ω), ‖↑↑g (x + B t ω)‖ ∂P ≤ ‖MeasureTheory.indicatorConstLp 2 hA ⋯ 1‖ * ‖g‖

★ ∫_A E‖g (x + B_t)‖ dx ≤ ‖1_A‖ ‖g‖: Cauchy–Schwarz against the indicator and the contraction property of the heat semigroup.

Bounds and measurability of the functional

theorem FeynmanKac.norm_fkFunctional_le {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) (t : NNReal) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∀ᵐ (x : EuclideanSpace ℝ ι), ‖fkFunctional V P B t (↑↑g) x‖ ≤ Real.exp (↑t * CV) * ∫ (ω : Ω), ‖↑↑g (x + B t ω)‖ ∂P

theorem FeynmanKac.norm_setIntegral_fkFunctional_le {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {A : Set (EuclideanSpace ℝ ι)} (hA : MeasurableSet A) (hμA : MeasureTheory.volume A < ⊤) : ‖∫ (x : EuclideanSpace ℝ ι) in A, fkFunctional V P B t (↑↑g) x‖ ≤ Real.exp (↑t * CV) * (‖MeasureTheory.indicatorConstLp 2 hA ⋯ 1‖ * ‖g‖)

★ The Wiener side is bounded on finite-measure sets: ‖∫_A fk g‖ ≤ e^{t‖V‖} ‖1_A‖ ‖g‖.

theorem FeynmanKac.aestronglyMeasurable_fkFunctional {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) [MeasureTheory.IsProbabilityMeasure P] (hVc : Continuous V) {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.AEStronglyMeasurable (fkFunctional V P B t ↑↑g) MeasureTheory.volume

The functional is a.e.-strongly measurable: an a.e. pointwise limit of the sliced functionals.

theorem FeynmanKac.integrableOn_fkFunctional {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) [MeasureTheory.IsProbabilityMeasure P] (hVc : Continuous V) {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : ProbabilityTheory.IsBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) {t : NNReal} (ht : 0 < t) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {A : Set (EuclideanSpace ℝ ι)} (hμA : MeasureTheory.volume A < ⊤) : MeasureTheory.IntegrableOn (fkFunctional V P B t ↑↑g) A MeasureTheory.volume

Feynman–Kac on L²

theorem FeynmanKac.feynmanKac_simpleFunc {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) [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)) {t : NNReal} (ht : 0 < t) (s : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 MeasureTheory.volume)) : ↑↑((HeatSemigroup.perturbedHeat VL ↑t) ↑s) =ᵐ[MeasureTheory.volume] fkFunctional V P B t ↑↑↑s

Feynman–Kac for a simple function, from FeynmanKac.feynmanKac.

theorem FeynmanKac.feynmanKac_Lp {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {V : EuclideanSpace ℝ ι → ℝ} {CV : ℝ} (hCV : ∀ (x : EuclideanSpace ℝ ι), |V x| ≤ CV) [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)) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) {t : NNReal} (ht : 0 < t) : ↑↑((HeatSemigroup.perturbedHeat VL ↑t) g) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ ι) => ∫ (ω : Ω), Complex.exp (-↑(∫ (s : ℝ) in 0..↑t, V (x + B s.toNNReal ω))) * ↑↑g (x + B t ω) ∂P

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

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

Both sides are continuous in g on every finite-measure set and agree on the dense set of simple functions (FeynmanKac.feynmanKac).