Universal height sequence: definitions and deterministic properties

The sequence interface records rational-age and almost-everywhere-age convergence under all laws. The totalized limsup is measurable, nonnegative, and depends literally on the prefix.

def BGW.StableTrees.IsUniversalHeightSeq (θ : ℝ) (ε : ℕ → ℝ) : Prop

ε is positive, strictly decreasing to 0, and along it the approximations converge almost surely at every rational time: to H02's height under the stable law, and to some limit under N on {q < ζ} and under the unit law at ages q < 1; the same holds at Lebesgue-almost every age (needed by H04's locality at the random ages q - g).

Equations

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

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

The chosen universal sequence (junk 1/(k+1) only if none exists).

Equations

• BGW.StableTrees.heightEps θ = if h : ∃ (ε : ℕ → ℝ), BGW.StableTrees.IsUniversalHeightSeq θ ε then Classical.choose h else fun (k : ℕ) => 1 / (↑k + 1)

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

The height read along the universal sequence (a real limsup; junk where it diverges).

Equations

• BGW.StableTrees.heightUniv θ f t = Filter.limsup (fun (k : ℕ) => BGW.StableTrees.heightApprox (BGW.StableTrees.heightEps θ k) f t) Filter.atTop

theorem BGW.StableTrees.heightEps_pos (θ : ℝ) (k : ℕ) : 0 < heightEps θ k

Every chosen cutoff is positive, including the fallback sequence.

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

Joint measurability of the universal height.

theorem BGW.StableTrees.heightUniv_zero (θ : ℝ) (f : Skorokhod.DLoc) : heightUniv θ f 0 = 0

heightUniv θ f 0 = 0 for every path.

theorem BGW.StableTrees.heightUniv_nonneg (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : 0 ≤ heightUniv θ f t

heightUniv is nonnegative for every path.

theorem BGW.StableTrees.heightApprox_eq_of_restrict_eq (ε : ℝ) (T : NNReal) (f g : Skorokhod.DLoc) (hfg : Skorokhod.DLoc.restrict T f = Skorokhod.DLoc.restrict T g) (t : NNReal) (ht : t ≤ T) : heightApprox ε f t = heightApprox ε g t

Agreement of compact prefixes implies agreement of every contained approximation.

theorem BGW.StableTrees.heightUniv_eq_of_restrict_eq (θ : ℝ) (T : NNReal) (f g : Skorokhod.DLoc) (hfg : Skorokhod.DLoc.restrict T f = Skorokhod.DLoc.restrict T g) (t : NNReal) (ht : t ≤ T) : heightUniv θ f t = heightUniv θ g t

Literal prefix locality: heightUniv θ f t reads f only on [0,t].