The distortion coefficients σ_{K,N}^{(t)}(θ) and τ_{K,N}^{(t)}(θ)

The curvature-dimension conditions CD(K, N) and CD*(K, N) of Sturm and Lott–Villani, and the measure-contraction property MCP(K, N), compare the reference measure along a Wasserstein geodesic with the model space of constant curvature K / N (or K / (N - 1)) through two families of distortion coefficients. For a curvature bound K : ℝ, a dimension bound N, a time t and a distance θ, put D = K θ² / N. Then

• σ_{K,N}^{(t)}(θ) = ∞ if D ≥ π²,
• σ_{K,N}^{(t)}(θ) = sin (t √D) / sin √D if 0 < D < π²,
• σ_{K,N}^{(t)}(θ) = t if D = 0,
• σ_{K,N}^{(t)}(θ) = sinh (t √(-D)) / sinh √(-D) if D < 0,

and, for N > 1, τ_{K,N}^{(t)}(θ) = ∞ if (N - 1) π² ≤ K θ² (exactly when σ_{K,N-1}^{(t)}(θ) = ∞) and τ_{K,N}^{(t)}(θ) = t ^ (1 / N) σ_{K,N-1}^{(t)}(θ) ^ (1 - 1 / N) otherwise, with τ_{K,1}^{(t)}(θ) = ∞ for K θ² > 0 and τ_{K,1}^{(t)}(θ) = t for K θ² ≤ 0. This N = 1 case deviates from Sturm at distance zero: Sturm puts τ_{K,1}^{(t)}(θ) = ∞ for every K > 0, including θ = 0, whereas here τ_{K,1}^{(t)}(0) = t, the limit of τ_{K,N}^{(t)}(0) = t as N ↓ 1. The two conventions agree whenever θ ≠ 0 or K ≤ 0. For 0 < D < π² and θ ≥ 0, √D = θ √(K / N), so the second case of σ is the familiar sin (t θ √(K / N)) / sin (θ √(K / N)).

Both families take values in [0, ∞] for t ∈ [0, 1], so they are ℝ≥0∞-valued here. The value ∞ records the Bonnet–Myers phenomenon: under CD(K, N) with K > 0 no two points are at distance more than π √((N - 1) / K). As in Sturm, the critical-distance case of τ is ∞ for every t, including t = 0, rather than the ℝ≥0∞ product 0 · ∞ = 0. Outside t ∈ [0, 1], N > 0 for σ and N ≥ 1 for τ, the values are junk values carrying no meaning.

The basic theory is the dependence on the parameters. For t ∈ [0, 1] the coefficient σ_{K,N}^{(t)}(θ) depends on (K, N, θ) only through D and is monotone in D (TauCeti.distortionSigma_mono). This rests on the monotonicity of the model ratios Real.monotoneOn_sin_mul_div_sin and Real.antitoneOn_sinh_mul_div_sinh, and on the comparisons Real.mul_sin_le_sin_mul and Real.sinh_mul_le_mul_sinh with the flat value t. Hence both coefficients increase with the curvature bound K. In particular they are at least t for K ≥ 0 and at most t for K ≤ 0, with equality σ_{0,N}^{(t)}(θ) = τ_{0,N}^{(t)}(θ) = t in the flat case. This monotonicity is what makes the curvature-dimension conditions weaker as K decreases, as in the implication from CD(K, N) to CD(K', N) for K' ≤ K.

Main definitions

• TauCeti.distortionSigma K N t θ: the distortion coefficient σ_{K,N}^{(t)}(θ).
• TauCeti.distortionTau K N t θ: the distortion coefficient τ_{K,N}^{(t)}(θ).

Main statements

• TauCeti.distortionSigma_mono: for t ∈ [0, 1], σ_{K,N}^{(t)}(θ) ≤ σ_{K',N'}^{(t)}(θ') whenever K θ² / N ≤ K' θ'² / N'.
• TauCeti.distortionSigma_left_monotone, TauCeti.distortionTau_left_monotone: both coefficients are monotone in the curvature bound K.
• TauCeti.antitoneOn_distortionSigma_of_nonneg, TauCeti.monotoneOn_distortionSigma_of_nonpos: σ_{K,N} decreases with N for K ≥ 0 and increases with N for K ≤ 0.
• TauCeti.distortionSigma_zero_left, TauCeti.distortionTau_zero_left: the flat coefficients are t.
• TauCeti.ofReal_le_distortionSigma, TauCeti.distortionSigma_le_ofReal and their τ analogues: comparison with the flat value t for K ≥ 0 and for K ≤ 0.
• TauCeti.distortionSigma_eq_top_iff, TauCeti.distortionTau_eq_top_iff: for N > 0, σ_{K,N}^{(t)}(θ) is infinite exactly when N π² ≤ K θ²; for N > 1, τ_{K,N}^{(t)}(θ) is infinite exactly when (N - 1) π² ≤ K θ².
• TauCeti.distortionTau_eq_top_of_lt: for K > 0, τ_{K,N}^{(t)}(θ) is infinite beyond the Bonnet–Myers distance π √((N - 1) / K), and TauCeti.distortionSigma_eq_top_of_lt: for K > 0 and N > 0, σ_{K,N}^{(t)}(θ) is infinite beyond π √(N / K).
• TauCeti.distortionSigma_time_one, TauCeti.distortionTau_time_one: below the critical distance both coefficients equal 1 at time 1.

References

• K.-T. Sturm, On the geometry of metric measure spaces. II, Acta Math. 196 (2006), 133–177.
• K. Bacher and K.-T. Sturm, Localization and tensorization properties of the curvature-dimension condition for metric measure spaces, J. Funct. Anal. 259 (2010), 28–56.
• C. Villani, Optimal Transport: Old and New, Springer 2009, Chapters 14 and 29.

noncomputable def TauCeti.distortionSigma (K N t θ : ℝ) : ENNReal

The distortion coefficient σ_{K,N}^{(t)}(θ) of the curvature-dimension condition CD*(K, N). With D = K θ² / N, it is ∞ if π² ≤ D, sin (t √D) / sin √D if 0 < D < π², t if D = 0, and sinh (t √(-D)) / sinh √(-D) if D < 0. It is meaningful for N > 0 and t ∈ [0, 1].

noncomputable def TauCeti.distortionTau (K N t θ : ℝ) : ENNReal

The distortion coefficient τ_{K,N}^{(t)}(θ) of the curvature-dimension condition CD(K, N). For N > 1 it is ∞ if (N - 1) π² ≤ K θ² and t ^ (1 / N) σ_{K,N-1}^{(t)}(θ) ^ (1 - 1 / N) otherwise, while τ_{K,1}^{(t)}(θ) is ∞ for K θ² > 0 and t for K θ² ≤ 0; unlike Sturm, who puts τ_{K,1}^{(t)}(θ) = ∞ for every K > 0, this gives τ_{K,1}^{(t)}(0) = t, the limit of τ_{K,N}^{(t)}(0) as N ↓ 1. It is meaningful for N ≥ 1 and t ∈ [0, 1].

The coefficient σ

@[simp]

theorem TauCeti.distortionSigma_eq_top_of_le {K N t θ : ℝ} (hN : 0 < N) (h : N * Real.pi ^ 2 ≤ K * θ ^ 2) : distortionSigma K N t θ = ⊤

At or beyond the critical distance, N π² ≤ K θ², the coefficient is infinite.

@[simp]

theorem TauCeti.distortionSigma_of_pos {K N t θ : ℝ} (hN : 0 < N) (h₀ : 0 < K * θ ^ 2) (h : K * θ ^ 2 < N * Real.pi ^ 2) : distortionSigma K N t θ = ENNReal.ofReal (Real.sin (t * √(K * θ ^ 2 / N)) / Real.sin √(K * θ ^ 2 / N))

The spherical formula, for 0 < K θ² < N π².

@[simp]

theorem TauCeti.distortionSigma_of_neg {K N t θ : ℝ} (hN : 0 < N) (h : K * θ ^ 2 < 0) : distortionSigma K N t θ = ENNReal.ofReal (Real.sinh (t * √(-(K * θ ^ 2 / N))) / Real.sinh √(-(K * θ ^ 2 / N)))

The hyperbolic formula, for K θ² < 0.

@[simp]

theorem TauCeti.distortionSigma_zero_left {N t θ : ℝ} : distortionSigma 0 N t θ = ENNReal.ofReal t

The flat coefficient σ_{0,N}^{(t)}(θ) is t.

@[simp]

theorem TauCeti.distortionSigma_zero_right {K N t : ℝ} : distortionSigma K N t 0 = ENNReal.ofReal t

At distance 0 the coefficient σ_{K,N}^{(t)}(0) is t.

theorem TauCeti.distortionSigma_mono {K N t θ K' N' θ' : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (h : K * θ ^ 2 / N ≤ K' * θ' ^ 2 / N') : distortionSigma K N t θ ≤ distortionSigma K' N' t θ'

Monotonicity of σ. For t ∈ [0, 1], σ_{K,N}^{(t)}(θ) is a monotone function of K θ² / N.

theorem TauCeti.distortionSigma_left_monotone {N t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hN : 0 ≤ N) : Monotone fun (K : ℝ) => distortionSigma K N t θ

For t ∈ [0, 1] and N ≥ 0, σ_{K,N}^{(t)}(θ) is monotone in the curvature bound K.

theorem TauCeti.antitoneOn_distortionSigma_of_nonneg {K t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hK : 0 ≤ K) : AntitoneOn (fun (N : ℝ) => distortionSigma K N t θ) (Set.Ioi 0)

For t ∈ [0, 1] and K ≥ 0, σ_{K,N}^{(t)}(θ) decreases with the dimension bound N > 0.

theorem TauCeti.monotoneOn_distortionSigma_of_nonpos {K t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hK : K ≤ 0) : MonotoneOn (fun (N : ℝ) => distortionSigma K N t θ) (Set.Ioi 0)

For t ∈ [0, 1] and K ≤ 0, σ_{K,N}^{(t)}(θ) increases with the dimension bound N > 0.

theorem TauCeti.ofReal_le_distortionSigma {K N t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hN : 0 ≤ N) (hK : 0 ≤ K) : ENNReal.ofReal t ≤ distortionSigma K N t θ

For K ≥ 0 the coefficient σ_{K,N}^{(t)}(θ) is at least the flat value t.

theorem TauCeti.distortionSigma_le_ofReal {K N t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hN : 0 ≤ N) (hK : K ≤ 0) : distortionSigma K N t θ ≤ ENNReal.ofReal t

For K ≤ 0 the coefficient σ_{K,N}^{(t)}(θ) is at most the flat value t.

theorem TauCeti.distortionSigma_eq_top_iff {K N t θ : ℝ} (hN : 0 < N) : distortionSigma K N t θ = ⊤ ↔ N * Real.pi ^ 2 ≤ K * θ ^ 2

The coefficient σ_{K,N}^{(t)}(θ) is infinite exactly when N π² ≤ K θ².

theorem TauCeti.distortionSigma_eq_top_of_lt {K N t θ : ℝ} (hK : 0 < K) (hN : 0 < N) (h : Real.pi * √(N / K) < θ) : distortionSigma K N t θ = ⊤

For K > 0 and N > 0, the coefficient σ_{K,N}^{(t)}(θ) is infinite beyond the critical distance π √(N / K).

@[simp]

theorem TauCeti.distortionSigma_time_one {K N θ : ℝ} (hN : 0 < N) (h : K * θ ^ 2 < N * Real.pi ^ 2) : distortionSigma K N 1 θ = 1

Below the critical distance, σ_{K,N}^{(1)}(θ) = 1.

@[simp]

theorem TauCeti.distortionSigma_time_zero {K N θ : ℝ} (hN : 0 < N) (h : K * θ ^ 2 < N * Real.pi ^ 2) : distortionSigma K N 0 θ = 0

Below the critical distance, σ_{K,N}^{(0)}(θ) = 0.

The coefficient τ

@[simp]

theorem TauCeti.distortionTau_eq_top_of_le {K N t θ : ℝ} (hN : 1 < N) (h : (N - 1) * Real.pi ^ 2 ≤ K * θ ^ 2) : distortionTau K N t θ = ⊤

For N > 1 and (N - 1) π² ≤ K θ², the coefficient τ_{K,N}^{(t)}(θ) is infinite.

@[simp]

theorem TauCeti.distortionTau_of_one_lt {K N t θ : ℝ} (hN : 1 < N) (h : K * θ ^ 2 < (N - 1) * Real.pi ^ 2) : distortionTau K N t θ = ENNReal.ofReal t ^ (1 / N) * distortionSigma K (N - 1) t θ ^ (1 - 1 / N)

For N > 1 and K θ² < (N - 1) π², τ_{K,N}^{(t)}(θ) = t ^ (1 / N) σ_{K,N-1}^{(t)}(θ) ^ (1 - 1 / N).

@[simp]

theorem TauCeti.distortionTau_one_eq_top_of_pos {K t θ : ℝ} (h : 0 < K * θ ^ 2) : distortionTau K 1 t θ = ⊤

For N = 1 and K θ² > 0, the coefficient τ_{K,1}^{(t)}(θ) is infinite.

@[simp]

theorem TauCeti.distortionTau_one_of_nonpos {K t θ : ℝ} (h : K * θ ^ 2 ≤ 0) : distortionTau K 1 t θ = ENNReal.ofReal t

For N = 1 and K θ² ≤ 0, the coefficient τ_{K,1}^{(t)}(θ) is t.

@[simp]

theorem TauCeti.distortionTau_zero_left {N t θ : ℝ} : distortionTau 0 N t θ = ENNReal.ofReal t

The flat coefficient τ_{0,N}^{(t)}(θ) is t.

@[simp]

theorem TauCeti.distortionTau_zero_right {K N t : ℝ} : distortionTau K N t 0 = ENNReal.ofReal t

At distance 0 the coefficient τ_{K,N}^{(t)}(0) is t.

theorem TauCeti.distortionTau_left_monotone {N t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : Monotone fun (K : ℝ) => distortionTau K N t θ

For t ∈ [0, 1], τ_{K,N}^{(t)}(θ) is monotone in the curvature bound K.

theorem TauCeti.ofReal_le_distortionTau {K N t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hK : 0 ≤ K) : ENNReal.ofReal t ≤ distortionTau K N t θ

For K ≥ 0 the coefficient τ_{K,N}^{(t)}(θ) is at least the flat value t.

theorem TauCeti.distortionTau_le_ofReal {K N t θ : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hK : K ≤ 0) : distortionTau K N t θ ≤ ENNReal.ofReal t

For K ≤ 0 the coefficient τ_{K,N}^{(t)}(θ) is at most the flat value t.

theorem TauCeti.distortionTau_eq_top_iff {K N t θ : ℝ} (hN : 1 < N) : distortionTau K N t θ = ⊤ ↔ (N - 1) * Real.pi ^ 2 ≤ K * θ ^ 2

For N > 1, the coefficient τ_{K,N}^{(t)}(θ) is infinite exactly when (N - 1) π² ≤ K θ².

theorem TauCeti.distortionTau_eq_top_of_lt {K N t θ : ℝ} (hK : 0 < K) (h : Real.pi * √((N - 1) / K) < θ) : distortionTau K N t θ = ⊤

For K > 0, the coefficient τ_{K,N}^{(t)}(θ) is infinite beyond the Bonnet–Myers distance π √((N - 1) / K), which is 0 for N ≤ 1.

@[simp]

theorem TauCeti.distortionTau_time_one {K N θ : ℝ} (h : K * θ ^ 2 < (N - 1) * Real.pi ^ 2) : distortionTau K N 1 θ = 1

Below the critical distance, τ_{K,N}^{(1)}(θ) = 1.

@[simp]

theorem TauCeti.distortionTau_time_zero {K N θ : ℝ} (h : K * θ ^ 2 < (N - 1) * Real.pi ^ 2) : distortionTau K N 0 θ = 0

Below the critical distance, τ_{K,N}^{(0)}(θ) = 0.