Transferring contour laws to rooted measured tree laws

The probability space and the finite tree may vary with the index. Weak convergence of the contours divided by a deterministic distance divisor, together with vanishing divisor-to-size tails, controls the discrepancy between uniform vertex mass and contour mass in probability.

Measurability is specified for the contour and rooted-space observables. No global measurable structure is installed on finite trees or addresses. The size-ratio hypothesis uses strict tails of the real outer measure, so the proof does not require a separate measurable size map. For measurable tree-valued inputs these are the usual strict probability tails.

theorem BGW.ContinuumTrees.exists_uniform_oscillation_of_isCompact (K : Set C(↑unitInterval, ℝ)) (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ g ∈ K, ∀ (s t : ↑unitInterval), |↑s - ↑t| ≤ δ → |g s - g t| ≤ ε

A compact family of continuous contours is uniformly equicontinuous.

theorem BGW.ContinuumTrees.FiniteTree.exists_vertex_ratio_bound_on_compact (K : Set C(↑unitInterval, ℝ)) (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) : ∃ r > 0, ∀ (t : PlaneTree) (b : ℝ) (hb : 0 < b), 1 ≤ b → b⁻¹ • t.contourFunction ∈ K → b / ↑t.size ≤ r → dist (MetricMeasure.RootedMeasuredGHSpace.scale b⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (rootedCompactMeasuredSpace t))) (Coding.rootedMeasuredGHSpace (b⁻¹ • t.contourFunction)) ≤ ε

On a compact set of rescaled contours, a small divisor-to-size ratio controls the distance between a vertex-measured finite tree and its continuum contour coding.

theorem BGW.ContinuumTrees.FiniteTree.tendsto_rooted_laws_of_contour {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (t : (n : ℕ) → Ω n → PlaneTree) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 < b n) (hbinfty : Filter.Tendsto b Filter.atTop Filter.atTop) (hF : ∀ (n : ℕ), Measurable fun (ω : Ω n) => MetricMeasure.RootedMeasuredGHSpace.scale (b n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (rootedCompactMeasuredSpace (t n ω)))) (hG : ∀ (n : ℕ), Measurable fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction) (hratio : ∀ r > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | r < b n / ↑(t n ω).size}) Filter.atTop (nhds 0)) {ν : MeasureTheory.ProbabilityMeasure C(↑unitInterval, ℝ)} (hlim : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction) Filter.atTop (nhds ν)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map fun (ω : Ω n) => MetricMeasure.RootedMeasuredGHSpace.scale (b n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (rootedCompactMeasuredSpace (t n ω)))) Filter.atTop (nhds (ν.map Coding.rootedMeasuredGHSpace))

Weak contour convergence transfers to rooted GHP laws on varying probability spaces. The only probabilistic error input is the strict divisor-to-size tail condition; the rooted GHP discrepancy is proved to vanish in probability.