Public occupation sequence and totalized supremum clock

The auxiliary fast sequence supplies existence. The extended limsup retains pathwise monotonicity even on exceptional paths where the real limsup has its default value.

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

theorem BGW.StableTrees.exists_isSupOccupationSeq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (ε : ℕ → ℝ), IsSupOccupationSeq θ ε

A positive strictly decreasing sequence with simultaneous finite occupation limits exists.

noncomputable def BGW.StableTrees.supEps (θ : ℝ) : ℕ → ℝ

The chosen sequence ε_k ↓ 0.

Equations

• BGW.StableTrees.supEps θ = if h : 1 < θ ∧ θ ≤ 2 then Classical.choose ⋯ else fun (k : ℕ) => 1 / (↑k + 1)

theorem BGW.StableTrees.isSupOccupationSeq_supEps {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : IsSupOccupationSeq θ (supEps θ)

The public choice is an admissible simultaneous occupation sequence.

theorem BGW.StableTrees.supEps_pos (θ : ℝ) (k : ℕ) : 0 < supEps θ k

Every public cutoff is positive, also outside the stable index range.

noncomputable def BGW.StableTrees.supLocalTime (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : ℝ

The supremum local time L^S = M, the limsup of the occupation approximations along supEps θ (real-valued, junk 0 where the occupations are unbounded).

Equations

• BGW.StableTrees.supLocalTime θ f t = Filter.limsup (fun (k : ℕ) => BGW.StableTrees.supOccupation (BGW.StableTrees.supEps θ k) f t) Filter.atTop

noncomputable def BGW.StableTrees.supLocalTimeENN (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : ENNReal

The ENNReal limsup p(t) of the nonnegative occupations along supEps θ: the totalized local time, everywhere nondecreasing in t.

Equations

• BGW.StableTrees.supLocalTimeENN θ f t = Filter.limsup (fun (k : ℕ) => ENNReal.ofReal (BGW.StableTrees.supOccupation (BGW.StableTrees.supEps θ k) f t)) Filter.atTop

theorem BGW.StableTrees.limsup_eq_toReal_of_nonneg {u : ℕ → ℝ} (hu : ∀ (k : ℕ), 0 ≤ u k) : Filter.limsup u Filter.atTop = (Filter.limsup (fun (k : ℕ) => ENNReal.ofReal (u k)) Filter.atTop).toReal

Nonnegative real sequences have compatible real and extended limsups, including unbounded sequences, for which both real readings are zero.

theorem BGW.StableTrees.supLocalTime_eq_toReal (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : supLocalTime θ f t = (supLocalTimeENN θ f t).toReal

The real clock is the finite reading of the extended clock on every path.

theorem BGW.StableTrees.monotone_supLocalTimeENN (θ : ℝ) (f : Skorokhod.DLoc) : Monotone (supLocalTimeENN θ f)

The extended clock is nondecreasing in time on every path.

theorem BGW.StableTrees.measurable_supLocalTimeENN_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => supLocalTimeENN θ p.2 p.1

The extended clock is jointly measurable in time and path.

theorem BGW.StableTrees.measurable_supLocalTimeENN_filtration (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supLocalTimeENN θ f t

Prefix measurability of the extended clock in the right-continuous filtration.

theorem BGW.StableTrees.measurable_supLocalTime_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => supLocalTime θ p.2 p.1

Joint measurability of the real public clock.

theorem BGW.StableTrees.stronglyAdapted_supLocalTime (θ : ℝ) : MeasureTheory.StronglyAdapted Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => supLocalTime θ f t

The real public clock is strongly adapted.

theorem BGW.StableTrees.measurable_supLocalTime (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supLocalTime θ f t

Fixed-time measurability of the real public clock.

theorem BGW.StableTrees.ae_tendsto_supOccupation {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), Filter.Tendsto (fun (k : ℕ) => supOccupation (supEps θ k) f t) Filter.atTop (nhds (supLocalTime θ f t))

The selected occupations converge simultaneously to their public real limsup.