Stopped occupation estimates for the public supremum local time

The almost sure identifications of the public clock and its ladder times with their auxiliary counterparts transfer the stopped second moments and full-filter convergence.

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

theorem BGW.StableTrees.supOccupation_stopped_L2_bound {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supOccupation ε f (supLadderTime θ z f) ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), supOccupation ε f (supLadderTime θ z f) ^ 2 ∂↑(stableLocalLaw θ) ≤ C

Stopped second-moment bound: for each level z there is C bounding, uniformly in ε ∈ (0, 1], the second moment of the approximation stopped at the ladder time A_z; the squared approximation is integrable.

theorem BGW.StableTrees.supOccupation_stopped_L2_tendsto {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : (∀ (ε : ℝ), 0 < ε → ε ≤ 1 → MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => (supOccupation ε f (supLadderTime θ z f) - ↑z) ^ 2) ↑(stableLocalLaw θ)) ∧ Filter.Tendsto (fun (ε : ℝ) => ∫ (f : Skorokhod.DLoc), (supOccupation ε f (supLadderTime θ z f) - ↑z) ^ 2 ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Stopped L² convergence: E[(supOccupation ε f (A_z) - z)²] → 0 as ε ↓ 0, consistent with M(A_z) = z. The auxiliary clock is constructed from compact-time estimates before the public choice of supEps; this public stopped theorem follows by the identification of the public local time and the stopped energy estimate.

theorem BGW.StableTrees.supOccupation_stopped_uniform_tendstoInMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) (δ : ℝ) (hδ : 0 < δ) : Filter.Tendsto (fun (ε : ℝ) => ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | δ ≤ ⨆ (t : ↑(Set.Iic (supLadderTime θ z f))), |supOccupation ε f ↑t - supLocalTime θ f ↑t|}) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Stopped Cauchy bound: the approximations stopped at A_z converge to M(A_z) = z uniformly over the stopped time interval, in probability, as ε ↓ 0 along the full filter.