Heat equation as a Brownian expectation
ProvedFeynmanKac.heat_terminal_representationdiffusionfeynman-kacpde
For a genuine one-dimensional Brownian diffusion in the published model, suppose its drift vanishes everywhere, volatility equals one everywhere, potential is zero and the running source is zero. If u is a bounded classical solution of the resulting backward heat equation with the prescribed terminal payoff and its discounted Brownian-gradient term satisfies the model's finite-energy condition, then its initial value equals the expected terminal payoff under the diffusion's probability law. This is a specialisation of the intended full Feynman–Kac representation, not a stochastic identity inserted into the model.
Preamble
import Definitions.Def_FeynmanKac_ClassicalSolutionConditions import Definitions.Def_FeynmanKac_BoundedDiffusionModel import Definitions.Def_FeynmanKac_PathDiscount import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Formal statement
theorem FeynmanKac.heat_terminal_representation
{Ω : Type*} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure P]
(m : FeynmanKac.BoundedDiffusionModel P)
(u : ℝ → ℝ → ℝ) (hu : m.IsClassicalPDESolution u)
(hμ : ∀ x s, m.drift x s = 0)
(hσ : ∀ x s, m.volatility x s = 1)
(hV : ∀ x s, m.potential x s = 0)
(hf : ∀ x s, m.runningSource x s = 0)
(hgrad : m.SquareIntegrableDiscountedGradient u) :
u m.initialState m.initialTime =
∫ ω, m.terminalPayoff (m.path m.terminalTime ω) ∂P := by sorrySource
Wikipedia Feynman–Kac formula https://en.wikipedia.org/wiki/Feynman%E2%80%93Kac_formula; James Nolen, Stanford notes Section 4.1 https://math.stanford.edu/~ryzhik/STANFORD/STANF227-10/notes227-09.pdf
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.