Represented compact metric probability spaces

The carrier, its genuine metric, compactness, and Borel probability measure are bundled together. Nonempty carriers are explicit. The Borel condition prevents a separate measurable structure from changing the intended measure.

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

structure BGW.MetricMeasure.CompactMeasuredSpace : Type (u + 1)

A nonempty compact metric space equipped with a Borel probability measure. Carriers lie in one fixed universe; the type of all represented spaces lies in the next universe. No full-support assumption is imposed.

• carrier : Type u

  The whole underlying space, including points outside the measure support.

• metric : MetricSpace self.carrier

  The metric structure on the carrier.

• nonempty : Nonempty self.carrier
• compact : CompactSpace self.carrier
• measurable : MeasurableSpace self.carrier

  The measurable structure, required below to be the Borel structure.

• borel : BorelSpace self.carrier
• law : MeasureTheory.ProbabilityMeasure self.carrier

  The probability measure on the carrier, without a full-support requirement.

@[instance_reducible]

instance BGW.MetricMeasure.CompactMeasuredSpace.instCoeSortType : CoeSort CompactMeasuredSpace (Type u)

Equations

• BGW.MetricMeasure.CompactMeasuredSpace.instCoeSortType = { coe := BGW.MetricMeasure.CompactMeasuredSpace.carrier }

@[instance_reducible]

instance BGW.MetricMeasure.CompactMeasuredSpace.instMetricSpaceCarrier (X : CompactMeasuredSpace) : MetricSpace X.carrier

Equations

• X.instMetricSpaceCarrier = X.metric

instance BGW.MetricMeasure.CompactMeasuredSpace.instNonemptyCarrier (X : CompactMeasuredSpace) : Nonempty X.carrier

instance BGW.MetricMeasure.CompactMeasuredSpace.instCompactSpaceCarrier (X : CompactMeasuredSpace) : CompactSpace X.carrier

@[instance_reducible]

instance BGW.MetricMeasure.CompactMeasuredSpace.instMeasurableSpaceCarrier (X : CompactMeasuredSpace) : MeasurableSpace X.carrier

Equations

• X.instMeasurableSpaceCarrier = X.measurable

instance BGW.MetricMeasure.CompactMeasuredSpace.instBorelSpaceCarrier (X : CompactMeasuredSpace) : BorelSpace X.carrier

def BGW.MetricMeasure.CompactMeasuredSpace.of (X : Type u) [MetricSpace X] [Nonempty X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.ProbabilityMeasure X) : CompactMeasuredSpace

Bundle an existing space and its actual probability measure.

Equations

• BGW.MetricMeasure.CompactMeasuredSpace.of X μ = { carrier := X, metric := inferInstance, nonempty := ⋯, compact := ⋯, measurable := inferInstance, borel := ⋯, law := μ }

noncomputable def BGW.MetricMeasure.CompactMeasuredSpace.distance (X Y : CompactMeasuredSpace) : ℝ

The GHP infimum on represented spaces.

Equations

• X.distance Y = BGW.MetricMeasure.ghpDistance ↑X.law ↑Y.law

theorem BGW.MetricMeasure.CompactMeasuredSpace.distance_nonneg (X Y : CompactMeasuredSpace) : 0 ≤ X.distance Y

theorem BGW.MetricMeasure.CompactMeasuredSpace.distance_comm (X Y : CompactMeasuredSpace) : X.distance Y = Y.distance X

theorem BGW.MetricMeasure.CompactMeasuredSpace.distance_of (X Y : Type u) [MetricSpace X] [Nonempty X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] [MetricSpace Y] [Nonempty Y] [CompactSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.ProbabilityMeasure X) (ν : MeasureTheory.ProbabilityMeasure Y) : (of X μ).distance (of Y ν) = ghpDistance ↑μ ↑ν

Exact agreement with the original infimum, with no surrogate distance.