Documentation

TauCeti.MeasureTheory.OptimalTransport.MetricMeasure.CurvatureDimension.Basic

The curvature-dimension conditions CD(K, ∞) and 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. Following Sturm and Lott–Villani, M satisfies the curvature-dimension condition CD(K, ∞), for K : ℝ, when m has full support and the Boltzmann entropy μ ↦ Ent_m(μ) relative to m is weakly K-convex on the quadratic Wasserstein space P₂(X): any two laws μ₀, μ₁ of finite second moment with Ent_m(μᵢ) < ∞ are joined by a W₂-geodesic (μ_t) along which

Ent_m(μ_t) ≤ (1 - t) Ent_m(μ₀) + t Ent_m(μ₁) - (K / 2) t (1 - t) W₂(μ₀, μ₁)².

This is the synthetic form of the lower Ricci bound Ric ≥ K: on a smooth Riemannian manifold with its volume measure the two are equivalent, by a theorem of von Renesse and Sturm. As in Sturm's definition, the endpoints range over the laws with Ent_m(μᵢ) < ∞, the effective domain of the entropy, and the inequality is read in [-∞, ∞]. The entropy may be ⊥ when m is infinite and grows fast at infinity, and such laws are endpoints too. In the usual setting, where m satisfies a growth bound such as ∫ exp (-c d(x₀, x)²) dm(x) < ∞ (for instance when m is finite), the entropy is never ⊥ on P₂(X), so the endpoints are the laws of finite entropy. Given full support, the condition is TauCeti.GeodesicallyConvex for the energy TauCeti.boltzmannEntropy m on TauCeti.WassersteinSpace 2 X (TauCeti.MetricMeasureSpace.curvatureDimensionInfinity_iff_geodesicallyConvex), and the slope formula and the rest of the theory of geodesically convex energies apply to it.

Full support is part of the condition, following the standing convention supp m = X of the metric-measure theory of curvature bounds. A reference measure without full support is handled by passing to its support, TauCeti.MetricMeasureSpace.supportSpace. In particular CD(K, ∞) fails for m = 0 on a nonempty space.

The condition constrains the geometry of X:

The finite-dimensional condition CD(K, N) #

For a dimension bound N ≥ 1, Sturm's condition CD(K, N) (TauCeti.MetricMeasureSpace.CurvatureDimension M K N) replaces the Boltzmann entropy by the Rényi entropies S_{N'}(· | m) (TauCeti.renyiEntropy) for N' ≥ N, and the term (K / 2) t (1 - t) W₂² by the distortion coefficients τ_{K,N'} (TauCeti.distortionTau). Write P_∞(m) for the laws absolutely continuous with respect to m with bounded support. Any μ₀ = ρ₀ m and μ₁ = ρ₁ m in P_∞(m) admit a quadratically optimal coupling q and a W₂-geodesic (μ_t) in P_∞(m) from μ₀ to μ₁ with

S_{N'}(μ_t | m) ≤ -∫ (τ₀ ρ₀(x₀)^{-1/N'} + τ₁ ρ₁(x₁)^{-1/N'}) dq(x₀, x₁),

where τ₀ = τ_{K,N'}^{(1-t)}(d(x₀, x₁)) and τ₁ = τ_{K,N'}^{(t)}(d(x₀, x₁)), for every t ∈ [0, 1] and every N' ≥ N. Here ρ₀ and ρ₁ are Radon–Nikodym derivatives with respect to m. As in Sturm's definition, the geodesic need not be induced by q, and full support of m is not part of the condition, as for the measure-contraction property TauCeti.MetricMeasureSpace.MeasureContraction.

Following Sturm, the coefficient τ_{K,N'}^{(s)}(θ) is infinite at every time s, including s = 1, once K > 0 and θ exceeds the Bonnet–Myers distance π √((N' - 1) / K). Hence the condition at t = 0 already forces the generalised Bonnet–Myers theorem: under CD(K, N) with K > 0 and N ≥ 1, the support of m has diameter at most π √((N - 1) / K) (TauCeti.MetricMeasureSpace.CurvatureDimension.dist_le).

Main definitions #

Main statements #

References #

source
theorem TauCeti.exists_boltzmannEntropy_ne_top_and_ne_bot_and_wassersteinEDist_dirac_le {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] {m : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure m] {p : ENNReal} {x : X} (hx : x ∈ m.support) {r : ℝ} (hr : 0 < r) :
∃ (μ : WassersteinSpace p X), boltzmannEntropy m ↑↑μ ≠ ⊤ ∧ boltzmannEntropy m ↑↑μ ≠ ⊥ ∧ wassersteinEDist p (MeasureTheory.Measure.dirac x) ↑↑μ ≤ ENNReal.ofReal r

Dirac masses on the support are limits of laws of finite entropy. If m is locally finite and x lies in the support of m, then for every r > 0 some law μ of finite p-moment and finite entropy, Ent_m(μ) ∉ {⊥, ⊤}, is within W_p-distance r of δ_x. One can take μ to be the normalised restriction of m to a small ball about x.

source
structure TauCeti.MetricMeasureSpace.CurvatureDimensionInfinity {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) (K : ℝ) :
Prop

The curvature-dimension condition CD(K, ∞) of Sturm and Lott–Villani for the metric-measure space M: the reference measure has full support, and the Boltzmann entropy relative to it is K-geodesically convex on the quadratic Wasserstein space P₂(X). That is, any two laws of finite second moment with Ent_m(μᵢ) < ∞ (the entropy may be ⊥) are joined by a W₂-geodesic (μ_t) along which Ent_m(μ_t) ≤ (1 - t) Ent_m(μ₀) + t Ent_m(μ₁) - (K / 2) t (1 - t) W₂(μ₀, μ₁)².

The carrier is complete and separable and the reference measure is finite on bounded sets, as TauCeti.MetricMeasureSpace requires. For a reference measure without full support, apply the condition to the support reduction TauCeti.MetricMeasureSpace.supportSpace.

Instances For
    source
    theorem TauCeti.MetricMeasureSpace.curvatureDimensionInfinity_iff_geodesicallyConvex {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K : ℝ} (hM : M.support = Set.univ) :
    M.CurvatureDimensionInfinity K ↔ GeodesicallyConvex K fun (μ : WassersteinSpace 2 X) => boltzmannEntropy M.reference ↑↑μ

    For a reference measure of full support, CD(K, ∞) is the K-geodesic convexity of the Boltzmann entropy.

    source
    theorem TauCeti.MetricMeasureSpace.CurvatureDimensionInfinity.mono {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K K' : ℝ} (h : M.CurvatureDimensionInfinity K) (hK : K' ≤ K) :
    M.CurvatureDimensionInfinity K'

    CD(K, ∞) implies CD(K', ∞) for every K' ≤ K.

    source
    theorem TauCeti.MetricMeasureSpace.CurvatureDimensionInfinity.exists_dist_sq_add_dist_sq_le {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K : ℝ} (h : M.CurvatureDimensionInfinity K) (x₀ x₁ : X) {ε : ℝ} (hε : 0 < ε) :
    ∃ (z : X), dist x₀ z ^ 2 + dist z x₁ ^ 2 ≤ dist x₀ x₁ ^ 2 / 2 + ε

    Approximate midpoints under CD(K, ∞). If M satisfies CD(K, ∞), any two points x₀, x₁ have approximate midpoints: for every ε > 0 some z has d(x₀, z)² + d(z, x₁)² ≤ d(x₀, x₁)² / 2 + ε. The left side is at least d(x₀, x₁)² / 2 for every z, with equality exactly at midpoints.

    source
    theorem TauCeti.MetricMeasureSpace.not_curvatureDimensionInfinity_of_support_eq_pair {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {x₀ x₁ : X} (hne : x₀ ≠ x₁) (hM : M.support = {x₀, x₁}) (K : ℝ) :
    ¬M.CurvatureDimensionInfinity K

    Two-point supports violate CD(K, ∞). A metric-measure space whose reference measure is supported on two distinct points satisfies CD(K, ∞) for no K: neither point is an approximate midpoint of the two.

    The finite-dimensional condition CD(K, N) #

    source
    def TauCeti.MetricMeasureSpace.CurvatureDimension {X : Type u_2} [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 with reference measure m. Write P_∞(m) for the laws absolutely continuous with respect to m with bounded support. Any two laws μ₀ = ρ₀ m and μ₁ = ρ₁ m in P_∞(m) admit a coupling q that is optimal for the quadratic cost and a W₂-geodesic (μ_t) from μ₀ to μ₁ running in P_∞(m) such that, for every t ∈ [0, 1] and every N' ≥ N,

    S_{N'}(μ_t | m) ≤ -∫ (τ₀ ρ₀(x₀)^{-1/N'} + τ₁ ρ₁(x₁)^{-1/N'}) dq(x₀, x₁),

    where τ₀ = τ_{K,N'}^{(1-t)}(d(x₀, x₁)) and τ₁ = τ_{K,N'}^{(t)}(d(x₀, x₁)).

    Here S_{N'} is the Rényi entropy TauCeti.renyiEntropy, τ_{K,N'} is the distortion coefficient TauCeti.distortionTau and ρᵢ is the Radon–Nikodym derivative of μᵢ with respect to m. Laws of bounded support have finite second moment, so the laws involved are points of TauCeti.WassersteinSpace 2 X. As in Sturm's definition, the geodesic need not be induced by q, and m need not have full support. The condition is meaningful for N ≥ 1.

    Instances For
      source
      theorem TauCeti.MetricMeasureSpace.curvatureDimension_iff {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N : ℝ} :
      M.CurvatureDimension K N ↔ ∀ ⦃μ₀ μ₁ : WassersteinSpace 2 X⦄, (↑↑μ₀).AbsolutelyContinuous M.reference → (↑↑μ₁).AbsolutelyContinuous M.reference → Bornology.IsBounded (↑↑μ₀).support → Bornology.IsBounded (↑↑μ₁).support → ∃ (q : MeasureTheory.Measure (X × X)), IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ 2) q ↑↑μ₀ ↑↑μ₁ ∧ ∃ (γ : ℝ → WassersteinSpace 2 X), IsGeodesicSegment γ μ₀ μ₁ ∧ ∀ t ∈ Set.Icc 0 1, (↑↑(γ t)).AbsolutelyContinuous M.reference ∧ Bornology.IsBounded (↑↑(γ t)).support ∧ ∀ N' ≥ N, renyiEntropy N' M.reference ↑↑(γ t) ≤ -↑(∫⁻ (z : X × X), distortionTau K N' (1 - t) (dist z.1 z.2) * (↑↑μ₀).rnDeriv M.reference z.1 ^ (-N'⁻¹) + distortionTau K N' t (dist z.1 z.2) * (↑↑μ₁).rnDeriv M.reference z.2 ^ (-N'⁻¹) ∂q)

      The curvature-dimension condition CD(K, N), unfolded.

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

      CD(K, N) implies CD(K', N) for every K' ≤ K: the distortion coefficient increases with the curvature bound.

      source
      theorem TauCeti.MetricMeasureSpace.CurvatureDimension.mono_dimension {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N N' : ℝ} (h : M.CurvatureDimension K N) (hN : N ≤ N') :
      M.CurvatureDimension K N'

      CD(K, N) implies CD(K, N') for every N' ≥ N: the defining inequality is required for every dimension bound above N.

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

      The generalised Bonnet–Myers theorem under CD(K, N). If M satisfies CD(K, N) with K > 0 and N ≥ 1, any two points of the support of the reference measure are at distance at most π √((N - 1) / K).

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

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

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

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