Law-level leaf-measure transfer

Tight rescaled contour laws, a vanishing divisor-to-size ratio and a vanishing leaf-index discrepancy make the vertex and leaf measures asymptotically indistinguishable in rooted measured Gromov--Hausdorff--Prokhorov distance. Weak convergence of the contours therefore determines the law of the leaf-measured trees, with the same limit as for vertex measures.

In probability

theorem BGW.ContinuumTrees.LeafMeasure.tendsto_dist_leaf_vertex_probability {Ω : ℕ → 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) (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)) (hleaf : ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ∃ k < numLeaves (t n ω), ε < |↑(leafIndex (t n ω) k) / ↑(t n ω).size - ↑k / ↑(numLeaves (t n ω))|}) Filter.atTop (nhds 0)) (htight : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑((μ n).map fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction))) (ε : ℝ) : ε > 0 → Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ε < dist (MetricMeasure.RootedMeasuredGHSpace.scale (b n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (leafRootedCompactMeasuredSpace (t n ω)))) (MetricMeasure.RootedMeasuredGHSpace.scale (b n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (FiniteTree.rootedCompactMeasuredSpace (t n ω))))}) Filter.atTop (nhds 0)

Leaf versus vertex measure in probability (the C10(1) perturbation input of C39). If the rescaled contour laws are tight, the divisor-to-size ratio and the leaf-index discrepancy vanish in probability, then the rescaled leaf- and vertex-measured rooted trees are within o_P(1) in rooted GHP distance.

theorem BGW.ContinuumTrees.FiniteTree.tendsto_dist_vertex_coded_probability {Ω : ℕ → 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) (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)) (htight : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑((μ n).map fun (ω : Ω n) => (b n)⁻¹ • (t n ω).contourFunction))) (ε : ℝ) : ε > 0 → Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ε < dist (MetricMeasure.RootedMeasuredGHSpace.scale (b n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (rootedCompactMeasuredSpace (t n ω)))) (Coding.rootedMeasuredGHSpace ((b n)⁻¹ • (t n ω).contourFunction))}) Filter.atTop (nhds 0)

Vertex measure versus contour coding in probability (the discrepancy step inside C38, exported). Under tight rescaled contour laws and vanishing divisor-to-size ratio, the rescaled vertex-measured rooted tree is within o_P(1) of the tree coded by its rescaled contour.

Convergence in law (public CT9 interface)

theorem BGW.ContinuumTrees.LeafMeasure.tendsto_rooted_leaf_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) (hFL : ∀ (n : ℕ), Measurable fun (ω : Ω n) => MetricMeasure.RootedMeasuredGHSpace.scale (b n)⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (leafRootedCompactMeasuredSpace (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)) (hleaf : ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ∃ k < numLeaves (t n ω), ε < |↑(leafIndex (t n ω) k) / ↑(t n ω).size - ↑k / ↑(numLeaves (t n ω))|}) 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 (leafRootedCompactMeasuredSpace (t n ω)))) Filter.atTop (nhds (ν.map Coding.rootedMeasuredGHSpace))

C39, law-level form (CT9). Weak convergence of the rescaled contours on varying probability spaces, vanishing divisor-to-size tails and vanishing leaf-index discrepancy in probability give convergence in law, in the rooted measured GHP space, of the rescaled trees carrying the uniform LEAF measure, to the same limit ν.map Coding.rootedMeasuredGHSpace as for the vertex measure (C38, tendsto_rooted_laws_of_contour). The measurability of the vertex-measure map (hF of C38) is not needed.

theorem BGW.ContinuumTrees.LeafMeasure.measurable_leafRootedMeasuredGHSpace_of_top {X : Type u_1} [MeasurableSpace X] (t : X → PlaneTree) {b : ℝ} (hb : 0 < b) (ht : Measurable t) : Measurable fun (x : X) => MetricMeasure.RootedMeasuredGHSpace.scale b⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (leafRootedCompactMeasuredSpace (t x)))

Hypothesis hFL for random trees measurable for the ⊤ σ-algebra on PlaneTree.

theorem BGW.ContinuumTrees.LeafMeasure.tendsto_rooted_leaf_laws_of_contour_of_top {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) (t : (n : ℕ) → Ω n → PlaneTree) (ht : ∀ (n : ℕ), Measurable (t n)) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 < b n) (hbinfty : Filter.Tendsto b Filter.atTop Filter.atTop) (hratio : ∀ r > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | r < b n / ↑(t n ω).size}) Filter.atTop (nhds 0)) (hleaf : ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | ∃ k < numLeaves (t n ω), ε < |↑(leafIndex (t n ω) k) / ↑(t n ω).size - ↑k / ↑(numLeaves (t n ω))|}) 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 (leafRootedCompactMeasuredSpace (t n ω)))) Filter.atTop (nhds (ν.map Coding.rootedMeasuredGHSpace))

Consumer form: C39 law-level transfer for ⊤-measurable random trees, with no separate measurability hypothesis.