Joint finite-dimensional limits for interpolated heights

Each interpolation error is bounded by the largest adjacent height jump. Vanishing jumps transfer K09 to interpolated height observations while retaining the entire walk coordinate.

theorem BGW.StableTrees.HeightTightness.forestHeightPath_sub_scaledHeight_le {B : ℕ → ℝ} {n : ℕ} {T t : NNReal} (ht : t ≤ T) (hB : 0 ≤ B n) (ω : ℕ → ℕ) : |(DiscreteForest.forestHeightPath B n T ω) ⟨↑t, ⋯⟩ - DiscreteHeightApprox.scaledHeight B n ω t| ≤ maxHeightJump B n (↑T) ω

The interpolation error at a fixed time is bounded by the largest adjacent height jump.

noncomputable def BGW.StableTrees.HeightTightness.interpolatedHeightJoint (B : ℕ → ℝ) (n : ℕ) (T : NNReal) {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)) (ω : ℕ → ℕ) : Skorokhod.D ↑T ℝ × (Fin r → ℝ)

The walk and the interpolated height observations at finitely many times.

Equations

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

theorem BGW.StableTrees.HeightTightness.measurable_interpolatedHeightJoint (B : ℕ → ℝ) (n : ℕ) (T : NNReal) {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)) : Measurable (interpolatedHeightJoint B n T t)

Interpolated height observations are measurable.

theorem BGW.StableTrees.HeightTightness.tendsto_interpolatedHeightJoint {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)) : Filter.Tendsto (fun (n : ℕ) => (DiscreteForest.offspringSeqLaw μ).map (interpolatedHeightJoint B n T t)) Filter.atTop (nhds ((stableLocalLaw θ).map (DiscreteHeightApprox.heightLimitJoint θ T fun (i : Fin r) => ⟨↑(t i), ⋯⟩)))

K09 extends to interpolated height observations because the adjacent jumps vanish.