Identification of the joint height limit

The exact finite-path occupation map converges by continuous mapping, and its distance from the discrete occupation vector is bounded by the final cell length. A joint vector error is covered by finitely many coordinate errors, and upper limits preserve the finite-sum bound. Choose positive bands tending to zero outside the exceptional countable set. The discrete two-limit estimate and the sealed continuum approximation identify both sides of the fixed-band joint convergence.

theorem BGW.StableTrees.DiscreteHeightApprox.measure_prod_pi_error_le {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace S] (P : MeasureTheory.Measure Ω) {r : ℕ} (X : Ω → S) (F G : Ω → Fin r → ℝ) {δ : ℝ} (hδ : 0 < δ) : P {ω : Ω | δ ≤ dist (X ω, F ω) (X ω, G ω)} ≤ ∑ i : Fin r, P {ω : Ω | δ / 2 < |F ω i - G ω i|}

A finite-vector joint error is bounded by a sum of coordinate error probabilities.

theorem BGW.StableTrees.DiscreteHeightApprox.limsup_finset_sum_le {α : Type u_1} {ι : Type u_2} (l : Filter α) (s : Finset ι) (f : ι → α → ENNReal) : Filter.limsup (fun (n : α) => ∑ i ∈ s, f i n) l ≤ ∑ i ∈ s, Filter.limsup (f i) l

Upper limits of finite sums of extended nonnegative reals are subadditive.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_limsup_prod_pi_error {α : Type u_1} {S : Type u_2} [PseudoMetricSpace S] {l : Filter α} {Ω : ℕ → Type u_3} [(n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) {r : ℕ} (X : (n : ℕ) → Ω n → S) (F : α → (n : ℕ) → Ω n → Fin r → ℝ) (G : (n : ℕ) → Ω n → Fin r → ℝ) (hc : ∀ (i : Fin r), ∀ δ > 0, Filter.Tendsto (fun (u : α) => Filter.limsup (fun (n : ℕ) => ↑(P n) {ω : Ω n | δ < |F u n ω i - G n ω i|}) Filter.atTop) l (nhds 0)) {δ : ℝ} (hδ : 0 < δ) : Filter.Tendsto (fun (u : α) => Filter.limsup (fun (n : ℕ) => ↑(P n) {ω : Ω n | δ ≤ dist (X n ω, F u n ω) (X n ω, G n ω)}) Filter.atTop) l (nhds 0)

Coordinate two-limit bounds give the joint finite-vector two-limit bound.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_limsup_measureReal_of_measure {α : Type u_1} {l : Filter α} {Ω : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (E : α → (n : ℕ) → Set (Ω n)) (h : Filter.Tendsto (fun (u : α) => Filter.limsup (fun (n : ℕ) => ↑(P n) (E u n)) Filter.atTop) l (nhds 0)) : Filter.Tendsto (fun (u : α) => Filter.limsup (fun (n : ℕ) => (↑(P n)).real (E u n)) Filter.atTop) l (nhds 0)

Convergence of upper-limit probabilities implies convergence of their real versions.

theorem BGW.StableTrees.DiscreteHeightApprox.dist_discreteJoint_finiteOccupationJoint_le (B : ℕ → ℝ) {n : ℕ} (hn : 0 < n) (hB : 0 < B n) (T : NNReal) {r : ℕ} (t : Fin r → NNReal) (ht : ∀ (i : Fin r), t i ≤ T) (ω : ℕ → ℕ) {ε : ℝ} (hε : 0 < ε) : dist (discreteJoint B n T ε t ω) (finiteOccupationJoint T ε t (DiscreteForest.forestWalkPath B n T ω)) ≤ 1 / (↑n * ε)

The entire joint occupation vector has the same deterministic mesh-error bound.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_joint_occupation {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) {r : ℕ} (t : Fin r → NNReal) (ht : ∀ (i : Fin r), t i ≤ T) : ∃ (Exc : Set ℝ), Exc.Countable ∧ ∀ (ε : ℝ), 0 < ε → ε ∉ Exc → Filter.Tendsto (fun (n : ℕ) => (DiscreteForest.offspringSeqLaw μ).map (discreteJoint B n T ε t)) Filter.atTop (nhds ((stableLocalLaw θ).map (continuumJoint T ε t)))

Fixed-ε joint convergence in law of (scaled walk, discrete ε-occupations) to (X, heightApprox ε), for ε outside a countable exceptional set (depending on the times).

theorem BGW.StableTrees.DiscreteHeightApprox.exists_bandSeq_avoiding {Exc : Set ℝ} (hExc : Exc.Countable) : ∃ (e : ℕ → ℝ), (∀ (n : ℕ), 0 < e n ∧ e n ∉ Exc) ∧ Filter.Tendsto e Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

A countable set can be avoided by a positive sequence tending to zero.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_walk_height_fdd {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) {r : ℕ} (t : Fin r → NNReal) (ht : ∀ (i : Fin r), t i ≤ T) : Filter.Tendsto (fun (n : ℕ) => (DiscreteForest.offspringSeqLaw μ).map (heightJoint B n T t)) Filter.atTop (nhds ((stableLocalLaw θ).map (heightLimitJoint θ T t)))

Joint walk/height finite-dimensional convergence (the K09 deliverable, fixed times, no H03): (forestWalkPath, (B_n/n) H_{⌊n t_i⌋}) ⇒ (X, height θ X (t_i)).

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_walk_height_fdd_two {μ : PMF ℕ} {B : ℕ → ℝ} (h : StableDomain μ 2 B) {T : NNReal} (hT : 0 < T) {r : ℕ} (t : Fin r → NNReal) (ht : ∀ (i : Fin r), t i ≤ T) : Filter.Tendsto (fun (n : ℕ) => (DiscreteForest.offspringSeqLaw μ).map (heightJoint B n T t)) Filter.atTop (nhds ((stableLocalLaw 2).map fun (f : Skorokhod.DLoc) => (Skorokhod.DLoc.restrict T f, fun (i : Fin r) => ↑f (t i) - futureInf f (t i) 0)))

Normalization at θ = 2: the limit height is X_t - I_t, with constant exactly 1 (B_n = σ√(n/2), library variance-2 process).