Metric spaces with a boundedly finite reference measure

A metric-measure space here has a complete separable metric carrier and a Borel reference measure finite on bounded sets. The reference need not be a probability: transported probability laws are separate objects. This is the carrier used in synthetic curvature and the metric-measure specialization of measured kernels.

The reference measure can be restricted to its closed support. The resulting metric space is again complete and separable, and its measure has full support. In particular, points outside the support play no role in integration against the reference measure.

structure TauCeti.MetricMeasureSpace (X : Type u_1) [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] : Type u_1

A Borel reference measure finite on every bounded set of a complete separable metric space. The metric and measurable structures are Mathlib's existing structures on X.

• reference : MeasureTheory.Measure X

  The reference measure, distinct from any transported probability law.

• finite_bounded (s : Set X) : Bornology.IsBounded s → self.reference s < ⊤

  Every bounded set has finite reference mass.

def TauCeti.MetricMeasureSpace.ofFinite {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : MetricMeasureSpace X

A finite Borel measure gives a metric-measure space on any complete separable metric carrier.

@[simp]

theorem TauCeti.MetricMeasureSpace.reference_ofFinite {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : (ofFinite μ).reference = μ

instance TauCeti.MetricMeasureSpace.instIsLocallyFiniteMeasureReference {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : MeasureTheory.IsLocallyFiniteMeasure M.reference

A reference measure finite on bounded sets is locally finite: balls are bounded.

def TauCeti.MetricMeasureSpace.support {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : Set X

The topological support of the reference measure.

theorem TauCeti.MetricMeasureSpace.support_def {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : M.support = M.reference.support

The support of a metric-measure space is the support of its reference measure.

theorem TauCeti.MetricMeasureSpace.mem_support_iff {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) (x : X) : x ∈ M.support ↔ ∀ U ∈ nhds x, 0 < M.reference U

A point belongs to the support exactly when every neighborhood has positive reference mass.

theorem TauCeti.MetricMeasureSpace.isClosed_support {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : IsClosed M.support

The support of a metric-measure space is closed.

instance TauCeti.MetricMeasureSpace.instCompleteSpaceSupport {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : CompleteSpace ↑M.support

A closed support inherits completeness from the ambient complete metric space.

theorem TauCeti.MetricMeasureSpace.measure_compl_support {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : M.reference M.supportᶜ = 0

The reference measure is concentrated on its support.

noncomputable def TauCeti.MetricMeasureSpace.supportMeasure {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : MeasureTheory.Measure ↑M.support

The reference measure regarded as a measure on its support.

theorem TauCeti.MetricMeasureSpace.supportMeasure_def {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : M.supportMeasure = MeasureTheory.Measure.comap Subtype.val M.reference

The measure on the support is the comap of the reference measure along inclusion.

theorem TauCeti.MetricMeasureSpace.supportMeasure_apply {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) (s : Set ↑M.support) : M.supportMeasure s = M.reference (Subtype.val '' s)

The mass of a set in the support is the reference mass of its image in the carrier.

theorem TauCeti.MetricMeasureSpace.map_supportMeasure {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : MeasureTheory.Measure.map Subtype.val M.supportMeasure = M.reference

Inclusion of the support pushes its restricted measure back to the original measure.

noncomputable def TauCeti.MetricMeasureSpace.supportSpace {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : MetricMeasureSpace ↑M.support

Restrict the reference measure to its support, with the inherited metric and Borel structures. This removes points that the reference measure does not see.

@[simp]

theorem TauCeti.MetricMeasureSpace.reference_supportSpace {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : M.supportSpace.reference = M.supportMeasure

instance TauCeti.MetricMeasureSpace.instIsOpenPosMeasureSupportMeasure {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : M.supportMeasure.IsOpenPosMeasure

The reduced measure is positive on every nonempty open subset of its carrier.

theorem TauCeti.MetricMeasureSpace.support_supportMeasure {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : M.supportMeasure.support = Set.univ

The reduced measure has full support: every point of the support of the reference measure lies in the support of its restriction.

theorem TauCeti.MetricMeasureSpace.support_supportSpace {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : M.supportSpace.reference.support = Set.univ

The support reduction has full topological support.

structure TauCeti.MeasurePreservingIsometry {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompleteSpace Y] [SecondCountableTopology Y] [BorelSpace Y] (M : MetricMeasureSpace X) (N : MetricMeasureSpace Y) : Type (max u_1 u_2)

An isometric map that pushes one reference measure to another. Surjectivity is not required: the inclusion of a measure's support is an example.

• toFun : X → Y

  The underlying isometry.

• isometry : Isometry self.toFun

  The map preserves distance.

• measurePreserving : MeasureTheory.MeasurePreserving self.toFun M.reference N.reference

  The map sends the first reference measure to the second.

@[instance_reducible]

instance TauCeti.MeasurePreservingIsometry.instFunLike {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompleteSpace Y] [SecondCountableTopology Y] [BorelSpace Y] {M : MetricMeasureSpace X} {N : MetricMeasureSpace Y} : FunLike (MeasurePreservingIsometry M N) X Y

theorem TauCeti.MeasurePreservingIsometry.ext {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompleteSpace Y] [SecondCountableTopology Y] [BorelSpace Y] {M : MetricMeasureSpace X} {N : MetricMeasureSpace Y} {f g : MeasurePreservingIsometry M N} (h : ∀ (x : X), f x = g x) : f = g

theorem TauCeti.MeasurePreservingIsometry.ext_iff {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompleteSpace Y] [SecondCountableTopology Y] [BorelSpace Y] {M : MetricMeasureSpace X} {N : MetricMeasureSpace Y} {f g : MeasurePreservingIsometry M N} : f = g ↔ ∀ (x : X), f x = g x

def TauCeti.MeasurePreservingIsometry.id {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : MeasurePreservingIsometry M M

Identity is a measure-preserving isometry.

@[simp]

theorem TauCeti.MeasurePreservingIsometry.id_apply {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) (x : X) : (id M) x = x

def TauCeti.MeasurePreservingIsometry.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompleteSpace Y] [SecondCountableTopology Y] [BorelSpace Y] [MetricSpace Z] [MeasurableSpace Z] [CompleteSpace Z] [SecondCountableTopology Z] [BorelSpace Z] {M : MetricMeasureSpace X} {N : MetricMeasureSpace Y} {P : MetricMeasureSpace Z} (g : MeasurePreservingIsometry N P) (f : MeasurePreservingIsometry M N) : MeasurePreservingIsometry M P

Composition of measure-preserving isometries.

@[simp]

theorem TauCeti.MeasurePreservingIsometry.comp_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompleteSpace Y] [SecondCountableTopology Y] [BorelSpace Y] [MetricSpace Z] [MeasurableSpace Z] [CompleteSpace Z] [SecondCountableTopology Z] [BorelSpace Z] {M : MetricMeasureSpace X} {N : MetricMeasureSpace Y} {P : MetricMeasureSpace Z} (g : MeasurePreservingIsometry N P) (f : MeasurePreservingIsometry M N) (x : X) : (g.comp f) x = g (f x)

noncomputable def TauCeti.MetricMeasureSpace.supportInclusion {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) : MeasurePreservingIsometry M.supportSpace M

The inclusion of the support preserves distances and pushes the reduced reference measure back to the original one.

@[simp]

theorem TauCeti.MetricMeasureSpace.supportInclusion_apply {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) (x : ↑M.support) : M.supportInclusion x = ↑x