Bounded optional sampling with almost surely right continuous paths #
Dyadic upper approximations preserve stopping times. Their stopped values are uniformly integrable conditional expectations of a single terminal value. This permits passing to a pathwise right continuous limit without completing the filtration or changing the process.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.stoppedValue_ae_eq_condExp_of_ae_rightContinuous
{P : MeasureTheory.Measure Skorokhod.DLoc}
[MeasureTheory.IsProbabilityMeasure P]
{M : NNReal → Skorokhod.DLoc → ℝ}
(hM : MeasureTheory.Martingale M Skorokhod.DLoc.filtration P)
(hprog : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration M)
(hright : ∀ᵐ (f : Skorokhod.DLoc) ∂P, ∀ (r : NNReal), ContinuousWithinAt (fun (s : NNReal) => M s f) (Set.Ici r) r)
{T : NNReal}
{τ : Skorokhod.DLoc → WithTop NNReal}
(hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ)
(hτ_le : ∀ (f : Skorokhod.DLoc), τ f ≤ ↑T)
:
MeasureTheory.stoppedValue M τ =ᵐ[P] P[M T | hτ.measurableSpace]
Bounded optional sampling for a progressive martingale whose paths are almost surely right continuous; the raw representative need not be right continuous on exceptional paths.