Probabilistic control of height increments on deterministic grids

K09 and portmanteau control every finite grid of discrete heights. Agreement with the continuous H03 height, uniform continuity on a compact horizon, and dominated convergence make the limiting grid-increment probabilities tend to zero.

noncomputable def BGW.StableTrees.HeightTightness.heightGridTime (R : NNReal) (N : ℕ) (i : Fin (N + 1)) : NNReal

Equally spaced observation times, including both endpoints of the horizon.

Equations

• BGW.StableTrees.HeightTightness.heightGridTime R N i = ⟨↑R * ↑↑i / ↑N, ⋯⟩

theorem BGW.StableTrees.HeightTightness.heightGridTime_le (R : NNReal) (N : ℕ) (i : Fin (N + 1)) : heightGridTime R N i ≤ R

Every uniform grid observation lies in its horizon, including the totalized zero mesh.

theorem BGW.StableTrees.HeightTightness.height_grid_limsup_probability_le {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {R : NNReal} (hR : 0 < R) (N : ℕ) (η : ℝ) : Filter.limsup (fun (n : ℕ) => (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ (i : Fin N), η ≤ |DiscreteHeightApprox.scaledHeight B n ω (heightGridTime R N i.castSucc) - DiscreteHeightApprox.scaledHeight B n ω (heightGridTime R N i.succ)|}) Filter.atTop ≤ (↑(stableLocalLaw θ)).real {f : Skorokhod.DLoc | ∃ (i : Fin N), η ≤ |height θ f (heightGridTime R N i.castSucc) - height θ f (heightGridTime R N i.succ)|}

K09 and portmanteau control every finite grid of height increments.

theorem BGW.StableTrees.HeightTightness.dist_heightGridTime_adjacent (R : NNReal) (N : ℕ) (i : Fin N) : dist (heightGridTime R N i.castSucc) (heightGridTime R N i.succ) = ↑R / ↑N

Adjacent grid times are separated by exactly one mesh width.

theorem BGW.StableTrees.HeightTightness.tendsto_height_grid_bad_probability_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (R : NNReal) {η : ℝ} (hη : 0 < η) : Filter.Tendsto (fun (N : ℕ) => (↑(stableLocalLaw θ)).real {f : Skorokhod.DLoc | ∃ (i : Fin N), η ≤ |height θ f (heightGridTime R N i.castSucc) - height θ f (heightGridTime R N i.succ)|}) Filter.atTop (nhds 0)

Continuity of the H03 height sends the limiting grid-increment probability to zero.

theorem BGW.StableTrees.HeightTightness.exists_eventually_height_grid_probability_small {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {R : NNReal} (hR : 0 < R) {η ε : ℝ} (hη : 0 < η) (hε : 0 < ε) (N₀ : ℕ) : ∃ (N : ℕ), N₀ ≤ N ∧ 0 < N ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ (i : Fin N), η ≤ |DiscreteHeightApprox.scaledHeight B n ω (heightGridTime R N i.castSucc) - DiscreteHeightApprox.scaledHeight B n ω (heightGridTime R N i.succ)|} ≤ ε

Arbitrarily fine fixed grids have uniformly small increment probabilities eventually in n.