C27--C29 for arbitrary admissible normings

A real attracted norming is first converted to the integer attraction predicate. The canonical monotone norming and convergence of types provide a stable-domain norming whose ratio to the given one tends to one. Deterministic spatial scaling then transfers the sealed forest, tail, and exact-size convergence theorems.

theorem BGW.StableTrees.ForestTriple.tendsto_forestTripleLaw_of_attracted {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hB : IsRealStableAttracted (realOffspringStepLaw μ) θ B) {T : NNReal} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => forestTripleLaw μ B n T) Filter.atTop (nhds (forestTripleLimit θ T))

C27 for an arbitrary admissible norming.

theorem BGW.StableTrees.ForestTriple.tendsto_forestTripleVecLaw_of_attracted {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hB : IsRealStableAttracted (realOffspringStepLaw μ) θ B) {T : NNReal} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => forestTripleVecLaw μ B n T) Filter.atTop (nhds (forestTripleVecLimit θ T))

C27, vector-path form, for an arbitrary admissible norming.

theorem BGW.StableTrees.TailPair.tendsto_tailPairLaw_of_attracted {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hB : IsRealStableAttracted (realOffspringStepLaw μ) θ B) {T : NNReal} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => tailPairLaw μ B n T) Filter.atTop (nhds (tailExcLaw θ T))

C28 for an arbitrary admissible norming.

theorem BGW.StableTrees.ExactContour.tendsto_exactHeightContourLaw_of_attracted {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hB : IsRealStableAttracted (realOffspringStepLaw μ) θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => exactHeightContourLaw μ B (q k) ⋯) Filter.atTop (nhds ((excLaw θ).map fun (p : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) => (p.2, p.2)))

C29 for an arbitrary admissible norming.

theorem BGW.StableTrees.ExactContour.tendsto_exactHeightLibContourLaw_of_attracted {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hB : IsRealStableAttracted (realOffspringStepLaw μ) θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => exactHeightLibContourLaw μ B (q k) ⋯) Filter.atTop (nhds ((excLaw θ).map fun (p : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) => (p.2, p.2)))

C29 in the library contour convention, for an arbitrary admissible norming.