Zero potential produces unit exponential discount
ProvedFeynmanKac.discount_zero_potentialdiscountfeynman-kacheat-equationzero-potential
For identically zero discounting or killing potential, the exponent of the discount factor is the integral of zero on any pair of endpoints. That integral vanishes, so the exponential discount equals one. The expanded formula has no dependency on separately published definition modules, permitting this independent mathematical leaf to compile.
Preamble
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic import Mathlib.Analysis.SpecialFunctions.ExpDeriv
Formal statement
theorem FeynmanKac.discount_zero_potential (t s : ℝ) :
Real.exp (-(∫ r in t..s, (0 : ℝ))) = 1 := by sorrySource
Wikipedia Feynman–Kac formula https://en.wikipedia.org/wiki/Feynman%E2%80%93Kac_formula