+# From uniform contour convergence to rooted measured tree convergence

The distance divisor tends to infinity and its ratio to the number of vertices tends to zero. Uniform convergence of the contours, normalized to duration one and divided by that divisor, then implies rooted GHP convergence of the vertex spaces with uniform mass on all vertices. No probabilistic invariance principle is assumed to have been proved by this deterministic result.

theorem BGW.ContinuumTrees.Coding.eventually_oscillation_le_of_tendsto {f : ℕ → C(↑unitInterval, ℝ)} {g : C(↑unitInterval, ℝ)} (hf : Filter.Tendsto f Filter.atTop (nhds g)) {δ : ℕ → ℝ} (hδ : Filter.Tendsto δ Filter.atTop (nhds 0)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s t : ↑unitInterval), |↑s - ↑t| ≤ δ n → |(f n) s - (f n) t| ≤ ε

Uniformly converging continuous functions have uniformly small oscillations on any sequence of time scales tending to zero.

theorem BGW.ContinuumTrees.FiniteTree.contour_time_error_le (t : PlaneTree) (hn : 2 ≤ t.size) (b : ℝ) (hb : 1 ≤ b) : ‖t.contourFunction‖ / (2 * ↑(t.size - 1)) + 2 / ↑t.size ≤ (‖b⁻¹ • t.contourFunction‖ + 2) * (b / ↑t.size)

Once the divisor is at least one, the first-visit time error is controlled by its ratio to tree size and the norm of the divided contour.

theorem BGW.ContinuumTrees.FiniteTree.tendsto_rooted_scale_of_contour (t : ℕ → PlaneTree) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 < b n) (hbinfty : Filter.Tendsto b Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (n : ℕ) => b n / ↑(t n).size) Filter.atTop (nhds 0)) {g : C(↑unitInterval, ℝ)} (hcontour : Filter.Tendsto (fun (n : ℕ) => (b n)⁻¹ • (t n).contourFunction) Filter.atTop (nhds g)) : Filter.Tendsto (fun (n : ℕ) => MetricMeasure.RootedMeasuredGHSpace.scale (b n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (rootedCompactMeasuredSpace (t n)))) Filter.atTop (nhds (Coding.rootedMeasuredGHSpace g))

Contour convergence transfers to rooted GHP convergence with uniform vertex mass. The divisor and size assumptions include sequences whose sizes vary irregularly.