PublishedMeasureDuality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Measure-family duality and probability lifting.

Ambrosio–Di Marino–Savaré, JEMS 17 (2015), 1817–1853, DOI 10.4171/JEMS/546, Theorem 5.1 (p. 1830), Corollary 5.2(b) (p. 1833): positive modulus of a Suslin image yields a probability plan on finite measures with an L² barycenter. MeasureImageDuality is the p = 2 consequence for a Borel image of a standard Borel space.
Bogachev, Measure Theory, vol. II (2007), Theorem 6.9.1 gives a measure-dependent measurable selector. MeasurePlanLifting states its probability-lifting consequence, used in the proof of ADMS, Theorem 7.2, p. 1839.

The two propositions separate measure-space duality from probability lifting; neither assumes a compact-support conclusion.

def OAI.CircleDomainRigidity.measureFamilyModulus line 34
Source documentation
Pointwise admissibility, including infinite values on reference-null sets.
```
def measureFamilyModulus (σ : Measure Z) (K : A → FiniteMeasure Z) : ℝ≥0∞ :=
…
```

def OAI.CircleDomainRigidity.MeasureImageDuality line 39

Source documentation

The measure-image conclusion of ADMS Theorem 5.1 and Corollary 5.2(b).

def MeasureImageDuality (A Z : Type*) [MeasurableSpace A] [StandardBorelSpace A]
    [TopologicalSpace Z] [PolishSpace Z] [MeasurableSpace Z] [BorelSpace Z] : Prop :=
…

def OAI.CircleDomainRigidity.MeasurePlanLifting line 52

Source documentation

The probability-lifting consequence of the cited measurable selector.

def MeasurePlanLifting (A Z : Type*) [MeasurableSpace A] [StandardBorelSpace A]
    [TopologicalSpace Z] [PolishSpace Z] [MeasurableSpace Z] [BorelSpace Z] : Prop :=
…

theorem OAI.CircleDomainRigidity.indexed_measure_duality line 59