Documentation

TauCeti.MeasureTheory.OptimalTransport.MetricMeasure.CurvatureDimension.Finite

The curvature-dimension conditions CD(K, N) 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. For a curvature bound K : ℝ and a dimension bound N, Sturm's curvature-dimension condition CD(K, N) compares the Rényi entropy S_N(μ | m) = -∫ ρ^{1-1/N} dm (TauCeti.renyiEntropy) along Wasserstein geodesics with the model space of curvature K / (N - 1) and dimension N. For a plan q on X × X whose marginals have densities ρ₀, ρ₁ with respect to m, and a family β^{(s)}(θ) of distortion coefficients, write

T_β^{(t)}(q | m) = -∫ [β^{(1-t)}(d(x₀, x₁)) ρ₀(x₀)^{-1/N} + β^{(t)}(d(x₀, x₁)) ρ₁(x₁)^{-1/N}] dq

(TauCeti.distortedRenyiEntropy). The full-support distorted condition requires that m has full support and any two laws μ₀, μ₁ of bounded support, absolutely continuous with respect to m (Sturm's space P_∞(X, d, m)), admit an optimal coupling q for the quadratic cost and a W₂-geodesic (μ_t) in P_∞(X, d, m) such that

S_{N'}(μ_t | m) ≤ T_{τ_{K,N'}}^{(t)}(q | m) for all t ∈ [0, 1] and all N' ≥ N,

where τ_{K,N'} is the distortion coefficient TauCeti.distortionTau. The reduced curvature-dimension condition CD*(K, N) of Bacher and Sturm is the same inequality with the coefficient σ_{K,N'} (TauCeti.distortionSigma) in place of τ_{K,N'}. The full-support distorted and reduced conditions are instances of one condition for a general family of coefficients, stated once with its monotonicity and diameter bound. The canonical CurvatureDimension condition is defined on the measure support in the imported Basic module. By theorems of Sturm and of Bacher–Sturm, not formalized here, on an n-dimensional weighted Riemannian manifold with N > n both conditions are equivalent to the lower bound Ric + Hess V - dV ⊗ dV / (N - n) ≥ K on the Bakry–Émery Ricci tensor; on general metric-measure spaces they are two distinct predicates. Full support follows the convention of TauCeti.MetricMeasureSpace.CurvatureDimensionInfinity; a reference measure without full support is handled by passing to TauCeti.MetricMeasureSpace.supportSpace.

The coefficients τ_{K,N}^{(s)}(θ) and σ_{K,N}^{(s)}(θ) are infinite at every time s once θ exceeds π √((N - 1) / K), respectively π √(N / K), for K > 0. With this convention the condition at time t = 0 alone gives the Bonnet–Myers diameter bound: if two points were farther apart, the uniform laws on two small balls about them would have T^{(0)}(q | m) = -∞ for every coupling q, while their Rényi entropy is finite.

Main definitions #

Main statements #

References #

source
structure TauCeti.MetricMeasureSpace.DistortedCurvatureDimension {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] (M : MetricMeasureSpace X) (β : ℝ → ℝ → ℝ → ENNReal) (N : ℝ) :
Prop

The curvature-dimension condition for a family of distortion coefficients β, where β N' s θ = β_{N'}^{(s)}(θ): the reference measure m has full support, and any two laws μ₀, μ₁ of bounded support, absolutely continuous with respect to m, admit an optimal coupling q for the quadratic cost and a W₂-geodesic (μ_t) of laws of bounded support, absolutely continuous with respect to m, along which S_{N'}(μ_t | m) ≤ T_{β_{N'}}^{(t)}(q | m) for every t ∈ [0, 1] and every N' ≥ N. Here S_{N'} is the Rényi entropy and T the distorted Rényi entropy (TauCeti.distortedRenyiEntropy). The laws range over Sturm's space P_∞(X, d, m).

With β = τ_K this is CD(K, N) (TauCeti.MetricMeasureSpace.CurvatureDimension), with β = σ_K it is CD*(K, N) (TauCeti.MetricMeasureSpace.ReducedCurvatureDimension).

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

    The reduced curvature-dimension condition CD*(K, N) of Bacher and Sturm: the condition CD(K, N) (TauCeti.MetricMeasureSpace.CurvatureDimension) with the distortion coefficient σ_{K,N'} (TauCeti.distortionSigma) in place of τ_{K,N'}. That is, m has full support, and any two laws μ₀, μ₁ of bounded support, absolutely continuous with respect to m, admit an optimal coupling q for the quadratic cost and a W₂-geodesic (μ_t) of such laws along which S_{N'}(μ_t | m) ≤ T_{σ_{K,N'}}^{(t)}(q | m) for every t ∈ [0, 1] and every N' ≥ N.

    The condition is meant for N ≥ 1, where the coefficients carry their geometric meaning.

    Instances For
      source
      theorem TauCeti.MetricMeasureSpace.reducedCurvatureDimension_iff {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N : ℝ} :
      M.ReducedCurvatureDimension K N ↔ M.DistortedCurvatureDimension (distortionSigma K) N

      CD*(K, N) is the curvature-dimension condition for the coefficients σ_{K,N'}.

      source
      theorem TauCeti.MetricMeasureSpace.DistortedCurvatureDimension.mono {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {β β' : ℝ → ℝ → ℝ → ENNReal} {N N' : ℝ} (h : M.DistortedCurvatureDimension β N) (hN : N ≤ N') (hβ : ∀ N'' ≥ N', ∀ s ∈ Set.Icc 0 1, ∀ (θ : ℝ), β' N'' s θ ≤ β N'' s θ) :
      M.DistortedCurvatureDimension β' N'

      The condition for the coefficients β implies the condition for N ≤ N' and any smaller coefficients β' ≤ β on the times [0, 1].

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

      CD*(K, N) implies CD*(K', N') for K' ≤ K and 0 ≤ N ≤ N'.

      source
      theorem TauCeti.MetricMeasureSpace.DistortedCurvatureDimension.dist_le {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {β : ℝ → ℝ → ℝ → ENNReal} {N D : ℝ} (h : M.DistortedCurvatureDimension β N) (hN : 0 < N) (hβ : ∀ (θ : ℝ), D < θ → β N 1 θ = ⊤) (x y : X) :
      dist x y ≤ D

      The Bonnet–Myers mechanism. Let β_N^{(1)}(θ) = ∞ for every distance θ > D. Under the curvature-dimension condition for the coefficients β, any two points are at distance at most D: otherwise the uniform laws on two small balls about them would violate the inequality at time 0, since T_{β_N}^{(0)}(q | m) = -∞ for every coupling q while their Rényi entropy is finite.

      source
      theorem TauCeti.MetricMeasureSpace.DistortedCurvatureDimension.diam_univ_le {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {β : ℝ → ℝ → ℝ → ENNReal} {N D : ℝ} (h : M.DistortedCurvatureDimension β N) (hN : 0 < N) (hD : 0 ≤ D) (hβ : ∀ (θ : ℝ), D < θ → β N 1 θ = ⊤) :
      Metric.diam Set.univ ≤ D

      The Bonnet–Myers diameter bound for the coefficients β: if β_N^{(1)}(θ) = ∞ for every distance θ > D ≥ 0, the space has diameter at most D.

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

      The diameter bound under CD*(K, N). If M satisfies CD*(K, N) with K > 0 and N > 0, any two points are at distance at most π √(N / K).

      source
      theorem TauCeti.MetricMeasureSpace.ReducedCurvatureDimension.diam_univ_le {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X] {M : MetricMeasureSpace X} {K N : ℝ} (h : M.ReducedCurvatureDimension K N) (hK : 0 < K) (hN : 0 < N) :
      Metric.diam Set.univ ≤ Real.pi * √(N / K)

      The diameter bound under CD*(K, N), for K > 0 and N > 0: the space has diameter at most π √(N / K).