Discounted stopping-time and independent future-path reward factorisation
ProvedAvramDividend.Classical.indepStoppingWeight_futureReward_lintegral_factordiscounted-rewardindependencestopping-timestrong-markov
When a finite stopping clock is independent of a measurable future reward path, every measurable nonnegative discount depending on the stopping clock factors from the expected nonnegative future reward. This is the exact weighted-expectation bridge required after strong-Markov independence for first-upcrossing dividend valuation.
Preamble
import Mathlib.Probability.Independence.Integration open MeasureTheory ProbabilityTheory Set open scoped NNReal ENNReal
Formal statement
theorem AvramDividend.Classical.indepStoppingWeight_futureReward_lintegral_factor
{Ω β : Type*} [MeasurableSpace Ω] [MeasurableSpace β]
(P : Measure Ω)
(τ : Ω → ℝ≥0) (hτ : Measurable τ)
(Y : Ω → β) (hY : Measurable Y)
(hInd : IndepFun τ Y P)
(discount : ℝ≥0 → ℝ≥0∞) (hd : Measurable discount)
(reward : β → ℝ≥0∞) (hr : Measurable reward) :
(∫⁻ ω, discount (τ ω) * reward (Y ω) ∂P) =
(∫⁻ ω, discount (τ ω) ∂P) *
(∫⁻ ω, reward (Y ω) ∂P) := by
sorrySource
Mathlib.Probability.Independence.Integration via IndepFun.comp and lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun; intended consumer is barrier dividend strong-Markov split 79978d61.