Documentation

BGW.MetricMeasure.MeasuredGHSpace

The GHP topology on measured isometry classes #

The equivalence relation identifies the entire compact metric space by a measure-preserving isometry, with the whole carrier retained. The ambient-isometry GHP infimum descends to this quotient and satisfies the pseudometric axioms. Its topology and Borel structure are therefore available for weak convergence. Separation, completeness, and separability are separate background results; none is assumed in this construction or the deterministic-limit argument.

Adapted from Freezing2/Geometry/MeasuredGHSpace.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

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

Measure-preserving isometry of the whole compact space. Null-measure points are retained, unlike a quotient identifying only the measure supports.

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

    The whole-space measured-isometry equivalence relation on compact measured spaces.

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

      Compact measured spaces modulo measure-preserving isometry of the whole space, equipped below with the GHP topology.

      Equations
      Instances For
        source
        def BGW.MetricMeasure.toMeasuredGHSpace (X : CompactMeasuredSpace) :
        MeasuredGHSpace

        Take the class of a compact measured space under whole-space measured isometry.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable instance BGW.MetricMeasure.MeasuredGHSpace.instPseudoMetricSpace :
          PseudoMetricSpace MeasuredGHSpace
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[instance_reducible]
          noncomputable instance BGW.MetricMeasure.MeasuredGHSpace.instMeasurableSpace :
          MeasurableSpace MeasuredGHSpace
          Equations
          source
          instance BGW.MetricMeasure.MeasuredGHSpace.instBorelSpace :
          BorelSpace MeasuredGHSpace
          source
          theorem BGW.MetricMeasure.MeasuredGHSpace.dist_toMeasuredGHSpace (X Y : CompactMeasuredSpace) :
          dist (toMeasuredGHSpace X) (toMeasuredGHSpace Y) = X.distance Y

          Distances in the quotient are literally the original ambient infima.

          source
          theorem BGW.MetricMeasure.MeasuredGHSpace.toMeasuredGHSpace_eq_iff (X Y : CompactMeasuredSpace) :
          toMeasuredGHSpace X = toMeasuredGHSpace Y ↔ X.MeasuredIsometry Y

          Equality in this quotient means whole-space measured isometry, including points outside the measure support.