Discounted reward and Brownian integrand for a bounded diffusion

import Definitions.Def_FeynmanKac_BoundedDiffusionModel
import Definitions.Def_FeynmanKac_DiscountedReward
import Mathlib.Analysis.Calculus.Deriv.Basic

open MeasureTheory

namespace FeynmanKac.BoundedDiffusionModel

/-- The discounted classical-solution value together with accumulated
discounted running payments, instantiated on the actual diffusion path. -/
noncomputable def discountedReward {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P]
    (m : BoundedDiffusionModel P)
    (u : ℝ → ℝ → ℝ) (s : ℝ) (ω : Ω) : ℝ :=
  FeynmanKac.discountedReward
    m.path m.potential u m.runningSource m.initialTime s ω

/-- The predictable-integrand candidate for the space component of Itô's
formula. Its actual measurability and stochastic-integral admissibility
remain separate proof obligations. -/
noncomputable def discountedSpaceGradient
    {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P]
    (m : BoundedDiffusionModel P)
    (u : ℝ → ℝ → ℝ) (s : ℝ) (ω : Ω) : ℝ :=
  m.pathDiscount s ω *
    m.volatility (m.path s ω) s *
    deriv (fun x => u x s) (m.path s ω)

end FeynmanKac.BoundedDiffusionModel