Unconditional full-path Markov–Tonelli formula for countably killed q-scale payoff

Proved

AvramDividend.Classical.chat04_countable_killed_scale_markov_tonelli

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

countable-gridkilled-semigroupmarkovq-scaletwo-sided-exit

For any deterministic Lévy splitting time s, any F_s-measurable initial reserve H, any countable future monitoring schedule τ through horizon T, and any measurable scale candidate W, the discounted terminal payoff killed by every monitored future reserve factorises into an integral over the distribution of H and an independent integral over the full future Lévy path. This is the explicit state-dependent killed semigroup kernel identity needed to build the q-scale renewal/harmonicity proof a885f0b3 and then strict two-sided exit identity 3e1ce2c8.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Map
import Mathlib.MeasureTheory.Measure.Prod
import Mathlib.Probability.Independence.Process.Basic
import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
import Mathlib.Topology.Instances.ENNReal.Lemmas
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Theorems.Thm_AvramDividend_Classical_chat04_unconditional_history_future_path_markov_tonelli
import Theorems.Thm_AvramDividend_Classical_chat04_countable_shifted_future_reserve_survival_measurable

open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
attribute [local instance] Classical.propDecidable
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.chat04_countable_killed_scale_markov_tonelli
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (s : ℝ≥0) (H : Ω → ℝ) (hH : Measurable[𝓕 s] H)
    (τ : ℕ → ℝ≥0) (T t : ℝ≥0)
    (q : ℝ) (W : ℝ → ℝ) (hW : Measurable W) :
    (∫⁻ ω,
        if ∀ j : ℕ, τ j ≤ T →
          0 ≤ H ω + (X.X (s + τ j) ω - X.X s ω)
        then ENNReal.ofReal
          (Real.exp (-(q * (t : ℝ))) *
            W (H ω + (X.X (s + t) ω - X.X s ω)))
        else (0 : ℝ≥0∞) ∂P) =
    ∫⁻ h, ∫⁻ y,
      (if ∀ j : ℕ, τ j ≤ T → 0 ≤ h + y (τ j)
        then ENNReal.ofReal
          (Real.exp (-(q * (t : ℝ))) * W (h + y t))
        else (0 : ℝ≥0∞))
      ∂(Measure.map (fun ω => (fun u : ℝ≥0 => X.X u ω)) P)
      ∂(Measure.map H P) := by sorry

Source

Proved unconditional whole-future-path Markov–Tonelli chat04_unconditional_history_future_path_markov_tonelli; Proved jointly measurable countably killed scale payoff chat04_countable_shifted_killed_scale_payoff_measurable; pinned Mathlib Bochner-Lebesgue product measure integration.

View graph