Prove2Me

Feynman–Kac with constant discount rate

Proved
FeynmanKac.constant_discount_representation

by WillR · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

diffusionfeynman-kacpde

When the potential VV equals a nonnegative constant rr, pathwise discounting becomes deterministic: Dt,s=e−r(s−t)D_{t,s}=e^{-r(s-t)}. The representation then gives the familiar discounted terminal payoff and discounted running cashflow formula. This is a useful bridge towards risk-neutral valuation and present-value calculations.

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.constant_discount_representation
    {Ω : Type*} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω)
    [MeasureTheory.IsProbabilityMeasure P]
    (m : FeynmanKac.BoundedDiffusionModel P)
    (r : ℝ) (hr : 0 ≤ r) (hV : ∀ x s, m.potential x s = r)
    (u : ℝ → ℝ → ℝ)
    (hu : m.IsClassicalPDESolution u)
    (hgrad : m.SquareIntegrableDiscountedGradient u) :
    u m.initialState m.initialTime =
      ∫ ω, (Real.exp (-(r * (m.terminalTime - m.initialTime))) *
          m.terminalPayoff (m.path m.terminalTime ω) +
        ∫ s in m.initialTime..m.terminalTime,
          Real.exp (-(r * (s - m.initialTime))) *
            m.runningSource (m.path s ω) s) ∂P := by sorry
Source
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

  • Endorsed by Shuze Chen · Oct 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph