Consequences of McCann's condition

A function U : ℝ → ℝ satisfies McCann's condition in dimension n when φ(s) = sⁿ U(s⁻ⁿ) is convex and nonincreasing on (0, ∞). This is the hypothesis of McCann's displacement convexity of the internal energy ∫ U(dμ/dρ) dρ. This file records the scalar facts about U and φ that it is used through, independently of any transport, and McCann's pointwise inequality at a positive operator, where the dimension n is that of the underlying space.

Main results

• TauCeti.pow_mul_apply_div_pow_eq: for r, a > 0, aⁿ U(r / aⁿ) = r φ(r^{-1/n} a).
• TauCeti.pow_mul_apply_div_pow_le: McCann's pointwise inequality, comparing aⁿ U(r / aⁿ) with the convex combination of its values at 1 and a₁ when (1 - t) + t a₁ ≤ a.
• ContinuousLinearMap.IsPositive.det_mul_apply_div_det_le: McCann's pointwise inequality at a positive operator A, comparing Jₜ U(r / Jₜ) with the convex combination of its values at t = 0 and t = 1, where Jₜ = det ((1 - t) • 1 + t • A).
• TauCeti.pow_mul_apply_inv_pow_le_recessionConstant: if φ is nonincreasing on (0, ∞), then the recession constant of U bounds φ above there.
• TauCeti.measurable_apply_max_of_convexOn: if φ is convex on (0, ∞), then U is measurable on [0, ∞).
• TauCeti.convexOn_pow_mul_neg_mul_rpow_neg, TauCeti.antitoneOn_pow_mul_neg_mul_rpow_neg: the integrand U(r) = -r · r^{-1/N} of the Rényi entropy satisfies McCann's condition in every dimension n ≤ N, with φ(s) = -s^{n/N} on (0, ∞).

References

• R. J. McCann, A convexity principle for interacting gases, Adv. Math. 128 (1997), 153–179.

theorem TauCeti.pow_mul_apply_div_pow_eq {U : ℝ → ℝ} {n : ℕ} (hn : n ≠ 0) {r : ℝ} (hr : 0 < r) {a : ℝ} (ha : 0 < a) : a ^ n * U (r / a ^ n) = r * ((r⁻¹ ^ (↑n)⁻¹ * a) ^ n * U ((r⁻¹ ^ (↑n)⁻¹ * a) ^ n)⁻¹)

For r > 0 and a > 0, the function a ↦ aⁿ U(r / aⁿ) is r φ(c a) with φ(s) = sⁿ U(s⁻ⁿ) and c = r^{-1/n}.

theorem TauCeti.pow_mul_apply_inv_pow_le_recessionConstant {U : ℝ → ℝ} {n : ℕ} (hn : n ≠ 0) (ha : AntitoneOn (fun (s : ℝ) => s ^ n * U (s ^ n)⁻¹) (Set.Ioi 0)) {s : ℝ} (hs : 0 < s) : ↑(s ^ n * U (s ^ n)⁻¹) ≤ recessionConstant U

If φ(s) = sⁿ U(s⁻ⁿ) is nonincreasing on (0, ∞), with n ≠ 0, then the recession constant U'(∞) = lim U(r) / r bounds φ above on (0, ∞), because U(r) / r = φ(r^{-1/n}).

theorem TauCeti.pow_mul_apply_div_pow_le {U : ℝ → ℝ} {n : ℕ} (hn : n ≠ 0) (hU0 : U 0 = 0) (hc : ConvexOn ℝ (Set.Ioi 0) fun (s : ℝ) => s ^ n * U (s ^ n)⁻¹) (ha : AntitoneOn (fun (s : ℝ) => s ^ n * U (s ^ n)⁻¹) (Set.Ioi 0)) {r t a a₁ L : ℝ} (hr : 0 ≤ r) (ht : t ∈ Set.Icc 0 1) (hapos : 0 < a) (ha₁ : 0 ≤ a₁) (hle : 1 - t + t * a₁ ≤ a) (hL : a₁ = 0 → 0 < r → ∀ s ∈ Set.Ioi 0, s ^ n * U (s ^ n)⁻¹ ≤ L) : a ^ n * U (r / a ^ n) ≤ (1 - t) * U r + t * if a₁ = 0 then r * L else a₁ ^ n * U (r / a₁ ^ n)

McCann's pointwise inequality. Let U 0 = 0 and let φ(s) = sⁿ U(s⁻ⁿ) be convex and nonincreasing on (0, ∞), with n ≠ 0. If a > 0 and a₁ ≥ 0 satisfy the concavity bound (1 - t) + t a₁ ≤ a for some t ∈ [0, 1], then for every r ≥ 0, aⁿ U(r / aⁿ) ≤ (1 - t) U(r) + t a₁ⁿ U(r / a₁ⁿ) when a₁ > 0, and aⁿ U(r / aⁿ) ≤ (1 - t) U(r) + t r L when a₁ = 0, where L bounds φ above.

theorem ContinuousLinearMap.IsPositive.det_mul_apply_div_det_le {U : ℝ → ℝ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {A : E →L[ℝ] E} (hA : A.IsPositive) (hU0 : U 0 = 0) (hc : ConvexOn ℝ (Set.Ioi 0) fun (s : ℝ) => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹) (ha : AntitoneOn (fun (s : ℝ) => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹) (Set.Ioi 0)) {r t L : ℝ} (hr : 0 ≤ r) (ht₀ : 0 < t) (ht₁ : t < 1) (hL : A.det = 0 → 0 < r → ∀ s ∈ Set.Ioi 0, s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹ ≤ L) : ((1 - t) • ContinuousLinearMap.id ℝ E + t • A).det * U (r / ((1 - t) • ContinuousLinearMap.id ℝ E + t • A).det) ≤ (1 - t) * U r + t * if A.det = 0 then L * r else A.det * U (r / A.det)

McCann's inequality at a positive operator. Let U 0 = 0 and let φ(s) = sⁿ U(s⁻ⁿ) be convex and nonincreasing on (0, ∞), where n ≥ 1 is the dimension of E. For a positive operator A on E, write Jₛ = det ((1 - s) • 1 + s • A). For 0 < t < 1 and r ≥ 0, Jₜ U(r / Jₜ) ≤ (1 - t) U(r) + t J₁ U(r / J₁) when J₁ ≠ 0, and Jₜ U(r / Jₜ) ≤ (1 - t) U(r) + t L r when J₁ = 0, provided L then bounds φ above. The concavity of s ↦ Jₛ^{1/n} is Minkowski's determinant inequality.

theorem TauCeti.measurable_apply_max_of_convexOn {U : ℝ → ℝ} {n : ℕ} (hn : n ≠ 0) (hc : ConvexOn ℝ (Set.Ioi 0) fun (s : ℝ) => s ^ n * U (s ^ n)⁻¹) : Measurable fun (r : ℝ) => U (max r 0)

If φ(s) = sⁿ U(s⁻ⁿ) is convex on (0, ∞), with n ≠ 0, then U is measurable on [0, ∞): it is continuous on (0, ∞), where U(r) = r φ(r^{-1/n}) with φ convex.

theorem TauCeti.pow_mul_neg_mul_rpow_neg_eq {n : ℕ} {N s : ℝ} (hs : 0 < s) : s ^ n * -((s ^ n)⁻¹ * (s ^ n)⁻¹ ^ (-N⁻¹)) = -s ^ (↑n / N)

On (0, ∞), the function φ(s) = sⁿ U(s⁻ⁿ) of the Rényi integrand U(r) = -r · r^{-1/N} is -s^{n/N}.

theorem TauCeti.convexOn_pow_mul_neg_mul_rpow_neg {n : ℕ} {N : ℝ} (hN : 0 < N) (hn : ↑n ≤ N) : ConvexOn ℝ (Set.Ioi 0) fun (s : ℝ) => s ^ n * -((s ^ n)⁻¹ * (s ^ n)⁻¹ ^ (-N⁻¹))

The Rényi integrand satisfies the convexity half of McCann's condition. For 0 < N and n ≤ N, the function φ(s) = sⁿ U(s⁻ⁿ) = -s^{n/N} of U(r) = -r · r^{-1/N} is convex on (0, ∞).

theorem TauCeti.antitoneOn_pow_mul_neg_mul_rpow_neg {n : ℕ} {N : ℝ} (hN : 0 < N) : AntitoneOn (fun (s : ℝ) => s ^ n * -((s ^ n)⁻¹ * (s ^ n)⁻¹ ^ (-N⁻¹))) (Set.Ioi 0)

The Rényi integrand satisfies the monotonicity half of McCann's condition. For 0 < N, the function φ(s) = sⁿ U(s⁻ⁿ) = -s^{n/N} of U(r) = -r · r^{-1/N} is nonincreasing on (0, ∞).