Finite stopped-history sigma-algebra independent of entire future Lévy increment path

Proved

AvramDividend.Classical.levy_finiteStopping_stoppedSigma_indep_shiftedPath

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

future-path-independencelevy-processstopped-sigma-algebrastrong-markov

The sigma-algebra of events observable by a finite stopping time is independent of the sigma-algebra generated by the entire Lévy path of increments after the stopping time. Given an arbitrary stopped-history measurable event A and a measurable future-path event, use the proved restricted full-path Markov law to derive the measure-intersection factorisation and then Mathlib's independence criterion.

Preamble

import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Process.Stopping
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Theorems.Thm_AvramDividend_Classical_isStoppingTime_withTop_of_le_events
import Theorems.Thm_AvramDividend_Classical_levy_finiteStopping_stoppedFuturePath_measurable
import Theorems.Thm_AvramDividend_Classical_levy_finiteStopping_restrictedFuturePath_mapLaw
import Theorems.Thm_AvramDividend_Classical_restrictedMapLaw_event_marginal_factor
import Theorems.Thm_AvramDividend_Classical_stoppedHistory_event_measurable

open MeasureTheory ProbabilityTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.levy_finiteStopping_stoppedSigma_indep_shiftedPath
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (τ : Ω → ℝ≥0)
    (hτ : ∀ s : ℝ≥0, MeasurableSet[𝓕 s] {ω : Ω | τ ω ≤ s}) :
    Indep
      (isStoppingTime_withTop_of_le_events τ hτ).measurableSpace
      (MeasurableSpace.comap
        (fun ω : Ω => fun t : ℝ≥0 =>
          X.X (τ ω + t) ω - X.X (τ ω) ω)
        inferInstance) P := by
  sorry

Source

Canonical stronger sigma-algebra form of proved 61930a38-11f1-449e-bbb6-67d59c6d5ca8, via full-path restricted map law e2543758-86c1-4254-a0b4-433781e31752. With measurable stopping clock this proves IndepFun of clock and future path, critical for 79978d61-9d1f-4b20-b8a5-114797a8e380.

View graph