Dense good times for the unit excursion law

Fixed jumps of a probability law on càdlàg paths form a countable set. Removing them yields a countable set meeting every open subinterval of (0,1).

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

noncomputable def BGW.StableTrees.unitPrefix (θ : ℝ) (a : NNReal) : MeasureTheory.Measure (Skorokhod.D ↑a ℝ)

The law of the unit-excursion prefix.

Equations

• BGW.StableTrees.unitPrefix θ a = MeasureTheory.Measure.map (BGW.StableTrees.excursionRestrict a) ↑(BGW.StableTrees.unitExcursionLaw θ)

def BGW.StableTrees.NoFixedJumpUnit (θ : ℝ) (t : NNReal) : Prop

Absence of a fixed jump under the unit law.

Equations

• BGW.StableTrees.NoFixedJumpUnit θ t = ∀ᵐ (e : BGW.StableTrees.Excursion) ∂↑(BGW.StableTrees.unitExcursionLaw θ), Function.leftLim (↑e.path) t = ↑e.path t

theorem BGW.StableTrees.exists_goodTimes_unit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (G : Set NNReal), G.Countable ∧ G ⊆ Set.Ioo 0 1 ∧ (∀ (x y : NNReal), x < y → y ≤ 1 → ∃ t ∈ G, x < t ∧ t < y) ∧ ∀ t ∈ G, NoFixedJumpUnit θ t

Countably many dense good times.