A fast occupation sequence and its adapted raw limit

The cutoffs are chosen strictly within the compact Cauchy radii. The raw real limsup preserves prefix measurability on every path.

References

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

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

There exists a fast positive occupation sequence.

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

The chosen fast sequence (junk 1/(k+1) for θ ∉ (1,2]).

Equations

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

theorem BGW.StableTrees.isSupAuxEpsSeq_supAuxEps {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : IsSupAuxEpsSeq θ (supAuxEps θ)

The selected sequence satisfies the fast Cauchy bounds.

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

The auxiliary limit M^*_t = limsup_k O_{ε_k}(t) along supAuxEps θ (raw, real-valued, adapted; the limsup keeps adaptedness by definition).

Equations

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

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

The raw auxiliary limit is jointly measurable for every index.

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

The raw auxiliary limit is strongly adapted for every index.