Public clock path properties and normalization

Identification transfers the auxiliary clock's continuity, recurrence and Stieltjes support. The full positive-cutoff normalization follows from convergence in mean.

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

theorem BGW.StableTrees.supOccupation_tendstoInMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : MeasureTheory.TendstoInMeasure (↑(stableLocalLaw θ)) (fun (ε : ℝ) (f : Skorokhod.DLoc) => supOccupation ε f t) (nhdsWithin 0 (Set.Ioi 0)) fun (f : Skorokhod.DLoc) => supLocalTime θ f t

Full-filter convergence in probability to the public clock.

theorem BGW.StableTrees.ae_supLocalTime_spec {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supLocalTime θ f 0 = 0 ∧ Monotone (supLocalTime θ f) ∧ Continuous (supLocalTime θ f) ∧ Filter.Tendsto (supLocalTime θ f) Filter.atTop Filter.atTop

The public local time starts at zero, is monotone and continuous, and tends to infinity.

theorem BGW.StableTrees.ae_supLocalTime_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), 0 < t → 0 < supLocalTime θ f t

Immediate positivity of the public local time.

noncomputable def BGW.StableTrees.supLocalTimeStieltjes (θ : ℝ) (f : Skorokhod.DLoc) : StieltjesFunction ℝ

The Stieltjes function s ↦ M_{s⁺} on ℝ; junk zero where M is not monotone and continuous (a null set).

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.supLocalTimeStieltjes_eq_aux {θ : ℝ} {f : Skorokhod.DLoc} (he : ∀ (t : NNReal), supLocalTime θ f t = supAuxLocalTime θ f t) : supLocalTimeStieltjes θ f = supAuxStieltjes θ f

On the identification event, the public and auxiliary Stieltjes functions agree.

theorem BGW.StableTrees.ae_supLocalTimeStieltjes_support {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (supLocalTimeStieltjes θ f).measure {s : ℝ | 0 ≤ s ∧ supRunning f s.toNNReal ≠ ↑f s.toNNReal} = 0

The public Stieltjes measure is supported on the supremum contact set.

theorem BGW.StableTrees.ae_supLocalTime_const_of_lt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s t : NNReal), s < t → (∀ u ∈ Set.Icc s t, ↑f u < supRunning f u ∧ Function.leftLim (↑f) u < supRunning f u) → supLocalTime θ f t = supLocalTime θ f s

The public clock is constant on intervals away from contact, including left limits.