The measure-contraction property MCP(K, N)

Let M be a metric-measure space (TauCeti.MetricMeasureSpace): a complete separable metric space X with its Borel structure and a reference measure m finite on bounded sets. For a curvature bound K : ℝ and a dimension bound N : ℝ, M has the measure-contraction property MCP(K, N) of Ohta and Sturm when the reference measure contracts towards every point of its support at least as fast as in the model space of curvature K / (N - 1) and dimension N. In the form of Cavalletti–Mondino used here: for every o in the support of m and every measurable A with 0 < m(A) < ∞, the normalised restriction m[|A] = m(A)⁻¹ m|_A is joined to the Dirac mass δ_o by a dynamic plan η concentrated on geodesics such that, for every time t ∈ [0, 1],

(e_t)_# (τ_{K,N}^{(1-t)}(d(γ₀, γ₁))^N η(dγ)) ≤ m(A)⁻¹ m,

where e_t evaluates a path at time t and τ_{K,N} is the distortion coefficient TauCeti.distortionTau. In words: the mass of A, transported along geodesics to o and weighted by the distortion coefficient, never piles up above the reference measure. Since the target is a Dirac mass, the only coupling of m[|A] and δ_o is their product, so every dynamic plan concentrated on geodesics with these two time marginals is an optimal one; no separate optimality requirement is needed. Ohta states the condition with the time reversed, starting from δ_o at time 0; the two forms agree after reversing the paths.

The coefficient τ_{K,N}^{(s)}(θ) is infinite for K > 0 and θ beyond the Bonnet–Myers distance π √((N - 1) / K), at every time s, following Sturm. With this convention the condition at time t = 0 already forces the Bonnet–Myers diameter bound: under MCP(K, N) with K > 0 and N > 0, any two points of the support of m are at distance at most π √((N - 1) / K) (TauCeti.MetricMeasureSpace.MeasureContraction.dist_le).

On a finite-dimensional real normed space E of dimension n ≥ 1 with an additive Haar measure, the plan moving m[|A] along straight segments to o shows that MCP(K, N) holds for every K ≤ 0 and N ≥ n; conversely the time marginals of any plan from the unit ball to 0 are carried by smaller balls, so MCP(0, N) forces N ≥ n. Thus Haar measure on E satisfies MCP(0, N) exactly when N ≥ n (TauCeti.MetricMeasureSpace.measureContraction_zero_iff_finrank_le), and MCP(K, N) for no K > 0 and N > 0, its support being unbounded.

Main definitions

• TauCeti.MetricMeasureSpace.MeasureContraction M K N: the measure-contraction property MCP(K, N) of the metric-measure space M.

Main statements

• TauCeti.MetricMeasureSpace.MeasureContraction.mono: for N ≥ 0, MCP(K, N) implies MCP(K', N) whenever K' ≤ K.
• TauCeti.MetricMeasureSpace.MeasureContraction.dist_le, TauCeti.MetricMeasureSpace.MeasureContraction.diam_support_le: the Bonnet–Myers diameter bound diam (supp m) ≤ π √((N - 1) / K) under MCP(K, N) with K > 0 and N > 0.
• TauCeti.MetricMeasureSpace.measureContraction_of_nonpos_of_finrank_le: Haar measure on a real vector space of dimension n ≥ 1 satisfies MCP(K, N) for K ≤ 0 and N ≥ n.
• TauCeti.MetricMeasureSpace.finrank_le_of_measureContraction_zero, TauCeti.MetricMeasureSpace.measureContraction_zero_iff_finrank_le: Haar measure on a real vector space of dimension n satisfies MCP(0, N) only for N ≥ n, and, for n ≥ 1, exactly then.
• TauCeti.MetricMeasureSpace.not_measureContraction_of_pos: Haar measure on a nontrivial real vector space satisfies MCP(K, N) for no K > 0 and N > 0.

References

• S. Ohta, On the measure contraction property of metric measure spaces, Comment. Math. Helv. 82 (2007), 805–828, Definition 2.1.
• K.-T. Sturm, On the geometry of metric measure spaces. II, Acta Math. 196 (2006), 133–177, §5.
• F. Cavalletti and A. Mondino, Optimal maps in essentially non-branching spaces, Commun. Contemp. Math. 19 (2017), 1750007, Definition 2.4.

def TauCeti.MetricMeasureSpace.MeasureContraction {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) (K N : ℝ) : Prop

The measure-contraction property MCP(K, N) of Ohta and Sturm, in the form of Cavalletti–Mondino: for every point o of the support of the reference measure m and every measurable A with 0 < m(A) < ∞, some dynamic plan η concentrated on geodesics has law m[|A] = m(A)⁻¹ m|_A at time 0 and law δ_o at time 1, and for every time t the law at time t of η weighted by τ_{K,N}^{(1-t)}(d(γ₀, γ₁))^N is at most m(A)⁻¹ m.

Such a plan is automatically optimal, since m[|A] and δ_o have only one coupling.

The property is meaningful for N ≥ 1: for 0 < N ≤ 1 and K > 0 the distortion coefficient distortionTau is ⊤ at positive distances, so MCP(K, N) then only says that the support of the reference measure has at most one point.

theorem TauCeti.MetricMeasureSpace.measureContraction_iff {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N : ℝ} : M.MeasureContraction K N ↔ ∀ o ∈ M.support, ∀ (A : Set X), MeasurableSet A → 0 < M.reference A → M.reference A < ⊤ → ∃ (η : MeasureTheory.Measure C(↑unitInterval, X)), (∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) ∧ η.timeMarginal 0 = M.reference[|A] ∧ η.timeMarginal 1 = MeasureTheory.Measure.dirac o ∧ ∀ (t : ↑unitInterval), (η.withDensity fun (γ : C(↑unitInterval, X)) => distortionTau K N (1 - ↑t) (dist (γ 0) (γ 1)) ^ N).timeMarginal t ≤ (M.reference A)⁻¹ • M.reference

The measure-contraction property MCP(K, N), unfolded.

theorem TauCeti.MetricMeasureSpace.MeasureContraction.mono {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K K' N : ℝ} (h : M.MeasureContraction K N) (hK : K' ≤ K) (hN : 0 ≤ N) : M.MeasureContraction K' N

MCP(K, N) implies MCP(K', N) for every K' ≤ K, when N ≥ 0: the distortion coefficient increases with the curvature bound.

theorem TauCeti.MetricMeasureSpace.MeasureContraction.dist_le {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N : ℝ} (h : M.MeasureContraction K N) (hK : 0 < K) (hN : 0 < N) {x y : X} (hx : x ∈ M.support) (hy : y ∈ M.support) : dist x y ≤ Real.pi * √((N - 1) / K)

The Bonnet–Myers diameter bound under MCP(K, N). If M satisfies MCP(K, N) with K > 0 and N > 0, any two points of the support of the reference measure are at distance at most π √((N - 1) / K). For N ≤ 1 this bound is 0 (as √ of a nonpositive number is 0), so the lemma then says that the support has at most one point.

theorem TauCeti.MetricMeasureSpace.MeasureContraction.diam_support_le {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N : ℝ} (h : M.MeasureContraction K N) (hK : 0 < K) (hN : 0 < N) : Metric.diam M.support ≤ Real.pi * √((N - 1) / K)

The Bonnet–Myers diameter bound under MCP(K, N), for K > 0 and N > 0: the support of the reference measure has diameter at most π √((N - 1) / K).

theorem TauCeti.MetricMeasureSpace.MeasureContraction.isBounded_support {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N : ℝ} (h : M.MeasureContraction K N) (hK : 0 < K) (hN : 0 < N) : Bornology.IsBounded M.support

Under MCP(K, N) with K > 0 and N > 0, the support of the reference measure is bounded.

theorem TauCeti.MetricMeasureSpace.measureContraction_of_nonpos_of_finrank_le {K N : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {M : MetricMeasureSpace E} [M.reference.IsAddHaarMeasure] [Nontrivial E] (hK : K ≤ 0) (hN : ↑(Module.finrank ℝ E) ≤ N) : M.MeasureContraction K N

Haar measure satisfies MCP(K, N) for K ≤ 0 and N ≥ n. On a real vector space of finite dimension n ≥ 1, an additive Haar reference measure satisfies MCP(K, N) for every K ≤ 0 and N ≥ n. The plan moves m[|A] along straight segments to o; its law at time t is the image of m[|A] under the homothety of ratio 1 - t towards o.

theorem TauCeti.MetricMeasureSpace.finrank_le_of_measureContraction_zero {N : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {M : MetricMeasureSpace E} [M.reference.IsAddHaarMeasure] (h : M.MeasureContraction 0 N) : ↑(Module.finrank ℝ E) ≤ N

MCP(0, N) forces N ≥ n for Haar measure. If an additive Haar reference measure on a real vector space of finite dimension n satisfies MCP(0, N), then N ≥ n. At time 1 / 2, any plan from the closed unit ball to 0 has its law carried by the ball of radius 1 / 2, of relative volume 2^(-n), while the weight is 2^(-N).

theorem TauCeti.MetricMeasureSpace.measureContraction_zero_iff_finrank_le {N : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {M : MetricMeasureSpace E} [M.reference.IsAddHaarMeasure] [Nontrivial E] : M.MeasureContraction 0 N ↔ ↑(Module.finrank ℝ E) ≤ N

Haar measure satisfies MCP(0, N) exactly when N ≥ n. On a real vector space of finite dimension n ≥ 1, an additive Haar reference measure satisfies MCP(0, N) if and only if N ≥ n.

theorem TauCeti.MetricMeasureSpace.not_measureContraction_of_pos {K N : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {M : MetricMeasureSpace E} [M.reference.IsAddHaarMeasure] [Nontrivial E] (hK : 0 < K) (hN : 0 < N) : ¬M.MeasureContraction K N

Haar measure on a nontrivial real vector space of finite dimension satisfies MCP(K, N) for no K > 0 and N > 0: its support is the whole unbounded space, against the Bonnet–Myers bound.