Stopping progressive martingales with almost surely right continuous paths #
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.martingale_stoppedProcess_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)
{τ : Skorokhod.DLoc → WithTop NNReal}
(hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ)
:
Continuous-time stopping for a progressive martingale with right continuous paths on a single event of full probability. The stopping time itself may be unbounded.