Measurability of the whole shifted Lévy future path at bounded stopping times

Proved

AvramDividend.Classical.levy_boundedStopping_stoppedFuturePath_measurable

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

avram-classicalfuture-pathmeasurabilitystopping-timestrong-markov

For any bounded stopping time of an adapted right-continuous Lévy process, the random entire future increment path is a measurable map into the real-valued product path space. Derives coordinate measurability from bounded continuous nonnegative reward measurability via positive and negative parts.

Preamble

import Mathlib.Probability.Process.Stopping
import Mathlib.Topology.Constructions
import Mathlib.Topology.Instances.ENNReal.Lemmas
import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
import Mathlib.Algebra.Order.Group.MinMax
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Theorems.Thm_AvramDividend_Classical_levy_boundedStopping_stoppedFutureReward_measurable

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

Formal statement

theorem AvramDividend.Classical.levy_boundedStopping_stoppedFuturePath_measurable
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (τ : Ω → ℝ≥0)
    (hstop : IsStoppingTime 𝓕 (fun ω => (τ ω : WithTop ℝ≥0)))
    (T : ℝ≥0) (hbound : ∀ ω, τ ω ≤ T) :
    Measurable (fun ω : Ω => fun t : ℝ≥0 =>
      X.X (τ ω + t) ω - X.X (τ ω) ω) := by
  sorry

Source

Eliminates the stopped-path pushforward measurability blocker for full strong-Markov independence 61930a38-11f1-449e-bbb6-67d59c6d5ca8 and barrier-value splitting 79978d61-9d1f-4b20-b8a5-114797a8e380. No scale function hypotheses.

View graph