The curvature-dimension condition CD(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 ≥ 1, M satisfies Sturm's curvature-dimension condition CD(K, N) when m has full support and, for any two probability laws μ₀ = ρ₀ m and μ₁ = ρ₁ m with bounded support, some quadratic optimal dynamic plan η from μ₀ to μ₁, with laws μ_t = (e_t)_# η, satisfies for every t ∈ [0, 1] and every N' ≥ N

S_{N'}(μ_t | m) ≤ -∫ [τ_{K,N'}^{(1-t)}(d(γ₀, γ₁)) ρ₀(γ₀)^{-1/N'} + τ_{K,N'}^{(t)}(d(γ₀, γ₁)) ρ₁(γ₁)^{-1/N'}] dη(γ).

Here S_{N'}(μ | m) = -∫ ρ^{1-1/N'} dm is the Rényi entropy (TauCeti.renyiEntropy), taken over the absolutely continuous part of μ, and τ_{K,N'} is the distortion coefficient TauCeti.distortionTau. This is the synthetic form of the bounds Ric ≥ K and dim ≤ N: the coefficients compare the contraction of volume along the transport with the model space of constant curvature K / (N - 1). The quantification over all N' ≥ N follows Sturm and makes the condition weaker as N grows; the condition weakens as K decreases since the coefficients increase with the curvature bound (TauCeti.MetricMeasureSpace.DynamicCurvatureDimension.mono).

The endpoint laws are those of Sturm's space P_∞(X, m): absolutely continuous with respect to m, with bounded support. Sturm asks for an optimal coupling q and a geodesic (μ_t) of such laws, integrating the right side against q. Here, as in the dynamic formulation of Cavalletti–Mondino, one dynamic plan concentrated on constant-speed geodesics carries both: its endpoint law is the coupling and its time marginals are the geodesic. The plan is not required to be unique or to be selected measurably in the endpoints, and the intermediate laws are not required to be absolutely continuous: as in TauCeti.renyiEntropy, the entropy ignores their singular part.

In the flat case the coefficients are τ_{0,N'}^{(s)}(θ) = s, and since μ₀ ≪ m the right side is (1 - t) S_{N'}(μ₀ | m) + t S_{N'}(μ₁ | m) (TauCeti.renyiEntropy_eq_neg_lintegral_rpow_neg). So CD(0, N) is the convexity of every Rényi entropy S_{N'}, N' ≥ N, along a common optimal dynamic plan (TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_zero_iff).

On a real inner product space of finite dimension n ≥ 1 with an additive Haar measure, the Rényi integrand U(r) = -r^{1-1/N'} satisfies McCann's condition for N' ≥ n: here sⁿ U(s⁻ⁿ) = -s^{n/N'} is convex and nonincreasing. McCann's displacement convexity (TauCeti.internalEnergy_map_smul_add_smul_gradient_le) along the Brenier interpolation therefore gives CD(0, N) for every N ≥ n, and hence CD(K, N) for every K ≤ 0 (TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_of_nonpos_of_finrank_le). Conversely, for N ≥ 1, CD(0, N) forces N ≥ n, already on a finite-dimensional real normed space with an additive Haar measure: transporting the uniform law on the unit ball to the uniform law on a ball of radius δ, the law at time 1 / 2 is carried by the ball of radius 1 / 2 + 3 δ / 2, so Hölder's bound TauCeti.neg_rpow_mul_rpow_le_renyiEntropy and the convexity inequality give 1 / 2 ≤ (1 / 2 + 3 δ / 2)^{n/N}; letting δ → 0 gives n ≤ N. Thus Haar measure satisfies CD(0, N) exactly when N ≥ n (TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_zero_iff_finrank_le).

Main definitions

• TauCeti.MetricMeasureSpace.DynamicCurvatureDimension M K N: the curvature-dimension condition CD(K, N) of the metric-measure space M.

Main statements

• TauCeti.MetricMeasureSpace.DynamicCurvatureDimension.mono: CD(K, N) implies CD(K', N') for K' ≤ K and N ≤ N'.
• TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_zero_iff: CD(0, N) is the convexity of the Rényi entropies S_{N'}, N' ≥ N, along a common optimal dynamic plan.
• TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_of_nonpos_of_finrank_le: Haar measure on a real inner product space of dimension n ≥ 1 satisfies CD(K, N) for K ≤ 0 and N ≥ n.
• TauCeti.MetricMeasureSpace.finrank_le_of_dynamicCurvatureDimension_zero, TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_zero_iff_finrank_le: for N ≥ 1, Haar measure on a real normed space of dimension n satisfies CD(0, N) only for N ≥ n, and, on an inner product space with n ≥ 1, exactly then.

References

• K.-T. Sturm, On the geometry of metric measure spaces. II, Acta Math. 196 (2006), 133–177, Definition 1.3 and Proposition 1.6.
• F. Cavalletti and A. Mondino, Optimal maps in essentially non-branching spaces, Commun. Contemp. Math. 19 (2017), 1750007, §2.
• R. J. McCann, A convexity principle for interacting gases, Adv. Math. 128 (1997), 153–179.
• C. Villani, Optimal Transport: Old and New, Springer 2009, Chapters 17 and 29.

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

The curvature-dimension condition CD(K, N) of Sturm for the metric-measure space M: the reference measure m has full support, and any two probability laws μ₀ = ρ₀ m, μ₁ = ρ₁ m with bounded support are joined by a quadratic optimal dynamic plan η such that, for every time t and every N' ≥ N, the Rényi entropy of the law μ_t at time t satisfies S_{N'}(μ_t | m) ≤ -∫ [τ_{K,N'}^{(1-t)}(d(γ₀, γ₁)) ρ₀(γ₀)^{-1/N'} + τ_{K,N'}^{(t)}(d(γ₀, γ₁)) ρ₁(γ₁)^{-1/N'}] dη(γ).

It is meaningful for N ≥ 1. This is the dynamic-plan form of the condition, with full support of the reference measure; TauCeti.MetricMeasureSpace.CurvatureDimension is the form with an optimal coupling and a W₂-geodesic.

• support_eq_univ : M.support = Set.univ

  The reference measure has full support.

• exists_isQuadraticOptimalDynamicPlan_renyiEntropy_le ⦃μ₀ μ₁ : MeasureTheory.ProbabilityMeasure X⦄ : (↑μ₀).AbsolutelyContinuous M.reference → (↑μ₁).AbsolutelyContinuous M.reference → Bornology.IsBounded (↑μ₀).support → Bornology.IsBounded (↑μ₁).support → ∃ (η : MeasureTheory.Measure C(↑unitInterval, X)), η.IsQuadraticOptimalDynamicPlan μ₀ μ₁ ∧ ∀ (t : ↑unitInterval) (N' : ℝ), N ≤ N' → renyiEntropy N' M.reference (η.timeMarginal t) ≤ -↑(∫⁻ (γ : C(↑unitInterval, X)), distortionTau K N' (1 - ↑t) (dist (γ 0) (γ 1)) * (↑μ₀).rnDeriv M.reference (γ 0) ^ (-N'⁻¹) + distortionTau K N' (↑t) (dist (γ 0) (γ 1)) * (↑μ₁).rnDeriv M.reference (γ 1) ^ (-N'⁻¹) ∂η)

  Any two absolutely continuous laws with bounded support are joined by a quadratic optimal dynamic plan along which the Rényi entropies satisfy the distorted convexity inequality.

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

CD(K, N) implies CD(K', N') whenever K' ≤ K and N ≤ N': the distortion coefficients increase with the curvature bound, and the condition already quantifies over all larger dimension bounds.

theorem TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_zero_iff {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {N : ℝ} (hN : 0 < N) : M.DynamicCurvatureDimension 0 N ↔ M.support = Set.univ ∧ ∀ ⦃μ₀ μ₁ : MeasureTheory.ProbabilityMeasure X⦄, (↑μ₀).AbsolutelyContinuous M.reference → (↑μ₁).AbsolutelyContinuous M.reference → Bornology.IsBounded (↑μ₀).support → Bornology.IsBounded (↑μ₁).support → ∃ (η : MeasureTheory.Measure C(↑unitInterval, X)), η.IsQuadraticOptimalDynamicPlan μ₀ μ₁ ∧ ∀ (t : ↑unitInterval) (N' : ℝ), N ≤ N' → renyiEntropy N' M.reference (η.timeMarginal t) ≤ ↑(1 - ↑t) * renyiEntropy N' M.reference ↑μ₀ + ↑↑t * renyiEntropy N' M.reference ↑μ₁

The flat curvature-dimension condition. For N > 0, CD(0, N) holds exactly when the reference measure has full support and any two absolutely continuous laws with bounded support are joined by a quadratic optimal dynamic plan along which every Rényi entropy S_{N'}, N' ≥ N, is convex: S_{N'}(μ_t | m) ≤ (1 - t) S_{N'}(μ₀ | m) + t S_{N'}(μ₁ | m).

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

CD(0, N) forces N ≥ n for Haar measure. If an additive Haar reference measure on a real normed space of finite dimension n satisfies CD(0, N) with N ≥ 1, then N ≥ n.

theorem TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_zero_of_finrank_le {N : ℝ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {M : MetricMeasureSpace E} [M.reference.IsAddHaarMeasure] [Nontrivial E] (hN : ↑(Module.finrank ℝ E) ≤ N) : M.DynamicCurvatureDimension 0 N

Haar measure satisfies CD(0, N) for N ≥ n. On a real inner product space of finite dimension n ≥ 1, an additive Haar reference measure satisfies CD(0, N) for every N ≥ n. The dynamic plan is the Brenier interpolation, along which every Rényi entropy S_{N'}, N' ≥ n, is convex by McCann's displacement convexity.

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

Haar measure satisfies CD(K, N) for K ≤ 0 and N ≥ n. On a real inner product space of finite dimension n ≥ 1, an additive Haar reference measure satisfies CD(K, N) for every K ≤ 0 and N ≥ n.

theorem TauCeti.MetricMeasureSpace.dynamicCurvatureDimension_zero_iff_finrank_le {N : ℝ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {M : MetricMeasureSpace E} [M.reference.IsAddHaarMeasure] [Nontrivial E] (hN : 1 ≤ N) : M.DynamicCurvatureDimension 0 N ↔ ↑(Module.finrank ℝ E) ≤ N

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