Documentation

BGW.ContinuumTrees.LeafLawConvergenceDeterministic

Deterministic leaf-measure transfer #

Uniform vertex and leaf measures on a finite plane tree are coupled by quantile sampling. The resulting graph-distance bound scales with the metric and gives a rooted measured Gromov--Hausdorff--Prokhorov estimate. A uniform modulus on a compact set of contours makes this estimate quantitative in the divisor-to-size ratio and the leaf-index discrepancy.

Measure change on one rooted carrier #

source
theorem BGW.MetricMeasure.dist_toRootedMeasuredGHSpace_le_levyProkhorovDist {X : Type u} [MetricSpace X] [Nonempty X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.ProbabilityMeasure X) (x : X) :
dist (toRootedMeasuredGHSpace { space := CompactMeasuredSpace.of X μ, root := x }) (toRootedMeasuredGHSpace { space := CompactMeasuredSpace.of X ν, root := x }) ≤ MeasureTheory.levyProkhorovDist ↑μ ↑ν

Measure change on one carrier. Two probability measures on the same compact metric space with the same root give rooted measured GHP classes at distance at most the Lévy–Prokhorov distance of the measures.

The leaf-measured rooted tree #

source
noncomputable def BGW.ContinuumTrees.LeafMeasure.leafLaw (t : PlaneTree) :
MeasureTheory.ProbabilityMeasure t.Vertex

The uniform probability on the leaves of a plane tree, bundled.

Equations
Instances For
    source
    @[simp]
    theorem BGW.ContinuumTrees.LeafMeasure.coe_leafLaw (t : PlaneTree) :
    ↑(leafLaw t) = leafMass t
    source
    noncomputable def BGW.ContinuumTrees.LeafMeasure.leafCompactMeasuredSpace (t : PlaneTree) :
    MetricMeasure.CompactMeasuredSpace

    The vertex set with its graph metric and the uniform probability on leaves.

    Equations
    Instances For
      source
      noncomputable def BGW.ContinuumTrees.LeafMeasure.leafRootedCompactMeasuredSpace (t : PlaneTree) :
      MetricMeasure.RootedCompactMeasuredSpace

      The same leaf-measured space, rooted at the empty address (as FiniteTree.rootedCompactMeasuredSpace).

      Equations
      Instances For

        The last depth-first leaf #

        source
        theorem BGW.ContinuumTrees.LeafMeasure.leafIndex_numLeaves_sub_one (t : PlaneTree) :
        leafIndex t (numLeaves t - 1) = t.size - 1

        The last leaf in DFS order is the last vertex in DFS order.

        source
        theorem BGW.ContinuumTrees.LeafMeasure.one_div_numLeaves_le (t : PlaneTree) {D : ℝ} (hD : ∀ k < numLeaves t, |↑(leafIndex t k) / ↑t.size - ↑k / ↑(numLeaves t)| ≤ D) :
        1 / ↑(numLeaves t) ≤ D + 1 / ↑t.size

        A leaf-index discrepancy bound forces many leaves: 1 / N ≤ D + 1 / n.

        Quantile coupling #

        source
        theorem BGW.ContinuumTrees.LeafMeasure.map_leafVertex_rank_volume (t : PlaneTree) :
        MeasureTheory.Measure.map (fun (s : ↑unitInterval) => leafVertex t (rank (numLeaves t) s)) MeasureTheory.volume = leafMass t

        The leaf quantile map sends Lebesgue measure on [0,1] to the uniform leaf measure.

        source
        theorem BGW.ContinuumTrees.LeafMeasure.dist_sampleVertex_leafVertex_le (t : PlaneTree) (hn : 2 ≤ t.size) {D ω : ℝ} (hD : ∀ k < numLeaves t, |↑(leafIndex t k) / ↑t.size - ↑k / ↑(numLeaves t)| ≤ D) (hω : ∀ (u v : ↑unitInterval), |↑u - ↑v| ≤ D + 1 / ↑(numLeaves t) + 2 * (‖t.contourFunction‖ / (2 * ↑(t.size - 1))) + 3 / ↑t.size → |t.contourFunction u - t.contourFunction v| ≤ ω) (s : ↑unitInterval) :
        dist (FiniteTree.sampleVertex t s) (leafVertex t (rank (numLeaves t) s)) ≤ 2 * ω

        Quantile coupling bound (C39(a), unscaled). The vertex and the leaf selected by the same uniform time s are within graph distance 2 ω, where ω bounds the oscillation of the contour at the time scale D + 1/N + 2 ‖c‖/(2(n-1)) + 3/n.

        source
        theorem BGW.ContinuumTrees.LeafMeasure.dist_scale_leaf_vertex_le (t : PlaneTree) (hn : 2 ≤ t.size) (c : ℝ) (hc : 0 < c) {D ω : ℝ} (hD : ∀ k < numLeaves t, |↑(leafIndex t k) / ↑t.size - ↑k / ↑(numLeaves t)| ≤ D) (hω : ∀ (u v : ↑unitInterval), |↑u - ↑v| ≤ D + 1 / ↑(numLeaves t) + 2 * (‖t.contourFunction‖ / (2 * ↑(t.size - 1))) + 3 / ↑t.size → |(c • t.contourFunction) u - (c • t.contourFunction) v| ≤ ω) :
        dist (MetricMeasure.RootedMeasuredGHSpace.scale c hc (MetricMeasure.toRootedMeasuredGHSpace (leafRootedCompactMeasuredSpace t))) (MetricMeasure.RootedMeasuredGHSpace.scale c hc (MetricMeasure.toRootedMeasuredGHSpace (FiniteTree.rootedCompactMeasuredSpace t))) ≤ 2 * ω

        Scaled vertex/leaf comparison. After multiplying the graph distance by c > 0, the leaf-measured and vertex-measured rooted trees are within rooted GHP distance 2 ω, where ω bounds the oscillation of the SCALED contour c • c_t at the time scale D + 1/N + 2 ‖c_t‖/(2(n-1)) + 3/n.

        Uniform compact estimate #

        source
        theorem BGW.ContinuumTrees.LeafMeasure.exists_leaf_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 → (∀ k < numLeaves t, |↑(leafIndex t k) / ↑t.size - ↑k / ↑(numLeaves t)| ≤ r) → dist (MetricMeasure.RootedMeasuredGHSpace.scale b⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (leafRootedCompactMeasuredSpace t))) (MetricMeasure.RootedMeasuredGHSpace.scale b⁻¹ ⋯ (MetricMeasure.toRootedMeasuredGHSpace (FiniteTree.rootedCompactMeasuredSpace t))) ≤ ε

        Uniform deterministic bound on a compact set of rescaled contours. For a compact K and ε > 0 there is r > 0 such that a tree whose rescaled contour lies in K, with divisor-to-size ratio ≤ r and all leaf-index discrepancies ≤ r, has rescaled leaf- and vertex-measured rooted trees within ε.