Progressive measurability of the raw error process

Progressiveness of the raw clock follows from measurability of the real limsup on each restricted product sigma algebra, without modifying exceptional paths.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.isStronglyProgressive_supOccupation {ε : ℝ} (hε : 0 < ε) : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => supOccupation ε f t

The occupation process is strongly progressive for each positive width.

theorem BGW.StableTrees.isStronglyProgressive_supAuxLocalTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => supAuxLocalTime θ f t

The raw auxiliary clock is strongly progressive, including on exceptional paths.

theorem BGW.StableTrees.isStronglyProgressive_errorMartingale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => errorMartingale θ ε t f

The error process is strongly progressive for the raw auxiliary clock.

theorem BGW.StableTrees.ae_errorMartingale_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), errorMartingale θ ε 0 f = 0

The error starts at zero almost surely.

theorem BGW.StableTrees.ae_rightContinuous_errorMartingale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => errorMartingale θ ε s f) (Set.Ici t) t

The error has right continuous paths on one event of full probability.