Documentation

BGW.MetricMeasure.RootedMeasuredGHSpace

The metric quotient of rooted compact probability spaces #

The equivalence relation is a single whole-carrier isometry preserving both the probability measure and the distinguished point. The actual rooted GHP infimum descends to a metric because its root-preserving separation theorem has already been proved. Its topology and Borel structure are induced by this one metric instance. Completeness and separability are not asserted here.

Forgetting the root maps to the existing unrooted quotient and is 1-Lipschitz. This construction follows the existing unrooted quotient in BGW.MetricMeasure.MeasuredGHSpace, adapted from Freezing2/Geometry/MeasuredGHSpace.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

source
def BGW.MetricMeasure.RootedCompactMeasuredSpace.MeasuredIsometry (X Y : RootedCompactMeasuredSpace) :
Prop

A whole-carrier isometry preserving the measure and the distinguished point.

Equations
Instances For
    source
    theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.measuredIsometry_refl (X : RootedCompactMeasuredSpace) :
    X.MeasuredIsometry X
    source
    theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.measuredIsometry_symm {X Y : RootedCompactMeasuredSpace} (h : X.MeasuredIsometry Y) :
    Y.MeasuredIsometry X
    source
    theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.measuredIsometry_trans {X Y Z : RootedCompactMeasuredSpace} (hXY : X.MeasuredIsometry Y) (hYZ : Y.MeasuredIsometry Z) :
    X.MeasuredIsometry Z
    source
    def BGW.MetricMeasure.RootedCompactMeasuredSpace.measuredIsometrySetoid :
    Setoid RootedCompactMeasuredSpace

    Root- and measure-preserving isometry is the equivalence relation used for the quotient.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.distance_congr {X Y X' Y' : RootedCompactMeasuredSpace} (hX : X.MeasuredIsometry X') (hY : Y.MeasuredIsometry Y') :
      X.distance Y = X'.distance Y'
      source
      def BGW.MetricMeasure.RootedMeasuredGHSpace :
      Type (u + 1)

      Rooted compact metric probability spaces modulo whole-carrier measured rooted isometry.

      Equations
      Instances For
        source
        def BGW.MetricMeasure.toRootedMeasuredGHSpace (X : RootedCompactMeasuredSpace) :
        RootedMeasuredGHSpace

        Take the class under whole-carrier isometries preserving the root and measure.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable instance BGW.MetricMeasure.RootedMeasuredGHSpace.instMetricSpace :
          MetricSpace RootedMeasuredGHSpace

          The metric is the literal rooted ambient infimum descended to isometry classes.

          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[instance_reducible]
          noncomputable instance BGW.MetricMeasure.RootedMeasuredGHSpace.instMeasurableSpace :
          MeasurableSpace RootedMeasuredGHSpace
          Equations
          source
          instance BGW.MetricMeasure.RootedMeasuredGHSpace.instBorelSpace :
          BorelSpace RootedMeasuredGHSpace
          source
          theorem BGW.MetricMeasure.RootedMeasuredGHSpace.dist_toRootedMeasuredGHSpace (X Y : RootedCompactMeasuredSpace) :
          dist (toRootedMeasuredGHSpace X) (toRootedMeasuredGHSpace Y) = X.distance Y

          Quotient distances agree definitionally with the represented rooted GHP infimum.

          source
          theorem BGW.MetricMeasure.RootedMeasuredGHSpace.toRootedMeasuredGHSpace_eq_iff (X Y : RootedCompactMeasuredSpace) :
          toRootedMeasuredGHSpace X = toRootedMeasuredGHSpace Y ↔ X.MeasuredIsometry Y

          Equality remembers the root and the measure on the entire compact carrier.

          source
          def BGW.MetricMeasure.RootedMeasuredGHSpace.forgetRoot :
          RootedMeasuredGHSpace → MeasuredGHSpace

          Forget the root while keeping the whole compact measured space.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem BGW.MetricMeasure.RootedMeasuredGHSpace.forgetRoot_toRootedMeasuredGHSpace (X : RootedCompactMeasuredSpace) :
            (toRootedMeasuredGHSpace X).forgetRoot = toMeasuredGHSpace X.space
            source
            theorem BGW.MetricMeasure.RootedMeasuredGHSpace.lipschitzWith_forgetRoot :
            LipschitzWith 1 forgetRoot
            source
            theorem BGW.MetricMeasure.RootedMeasuredGHSpace.continuous_forgetRoot :
            Continuous forgetRoot
            source
            theorem BGW.MetricMeasure.RootedMeasuredGHSpace.measurable_forgetRoot :
            Measurable forgetRoot