Documentation

BGW.MetricMeasure.RootedUnderlyingGH

Underlying Gromov--Hausdorff classes of rooted measured spaces #

Forgetting the root and the measure is continuous, and therefore transports weakly convergent probability laws. The declarations remain in their historical Coding namespace for API compatibility, although they do not depend on continuum-tree coding.

source
@[instance_reducible]
noncomputable def BGW.ContinuumTrees.Coding.ghMeasurableSpace :
MeasurableSpace GromovHausdorff.GHSpace

Local Borel structure on GHSpace, as in measurable_underlyingGH.

Equations
Instances For
    source
    theorem BGW.ContinuumTrees.Coding.instBorelSpaceGHSpace_bGW :
    BorelSpace GromovHausdorff.GHSpace
    source
    noncomputable def BGW.ContinuumTrees.Coding.forgetToGH :
    MetricMeasure.RootedMeasuredGHSpace → GromovHausdorff.GHSpace

    Forget root and measure: the GH class of a rooted measured class.

    Equations
    Instances For
      source
      theorem BGW.ContinuumTrees.Coding.continuous_forgetToGH :
      Continuous forgetToGH

      Forgetting root and measure is continuous for the GHP and GH topologies.

      source
      theorem BGW.ContinuumTrees.Coding.tendsto_map_forgetToGH {ι : Type u_1} {L : Filter ι} (P : ι → MeasureTheory.ProbabilityMeasure MetricMeasure.RootedMeasuredGHSpace) {Q : MeasureTheory.ProbabilityMeasure MetricMeasure.RootedMeasuredGHSpace} (h : Filter.Tendsto P L (nhds Q)) :
      Filter.Tendsto (fun (i : ι) => (P i).map forgetToGH) L (nhds (Q.map forgetToGH))

      Weak convergence of laws of rooted measured classes gives weak convergence of the laws of the underlying GH classes. The laws on GHSpace use its Borel σ-algebra (borel GHSpace), which callers must provide locally (letI := borel GHSpace), as in measurable_underlyingGH.