Operator convexity of x^p on [1,2] and of x log x

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Two results that close named TODOs in Mathlib's own source, in the C⋆-generic setting where upstream states the rest of this tier:

• convexOn_rpow_Ioo12 / convexOn_nnrpow_Ioo12 — a ↦ a ^ p is operator convex for p ∈ (1,2). Upstream's …/Rpow/Order.lean lists "Show operator convexity of rpow over Icc 1 2". MATHLIB-ABSENT(CFC.convexOn_rpow_Ioo12)
• ★ convexOn_mul_log — a ↦ a * log a is operator convex on the strictly positive elements. Upstream's …/ExpLog/Order.lean lists "Show that x => x * log x is operator convex" as its remaining TODO. MATHLIB-ABSENT(CFC.convexOn_mul_log)

Why these are cheap, and why that was not obvious

The x^p rung mirrors upstream's own ₀₁ proof with the ₁₂ integrand, and the reason it works is algebraic: rpowIntegrand₁₂ p t x = t^(p−1)·t⁻¹·x + t^p·(t+x)⁻¹ − t^(p−1) is affine plus a nonnegative multiple of the resolvent, whose operator convexity (CStarAlgebra.convexOn_ringInverse_algebraMap_add) is already upstream. Every other input — Real.rpowIntegrand₁₂, CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₁₂, integral_convexOn_of_integrand_ae, convexOn_cfcₙ_of_convexOn_cfc, isClosed_setOfPred_convexOn — is present at the pin.

★ x log x then needs no new analysis at all: a · cfc (p⁻¹(x^p − 1)) a → a · log a by Tendsto.const_mul applied to the existing CFC.tendsto_cfc_rpow_sub_one_log, closed with isClosed_setOfPred_convexOn.mem_of_tendsto — the same shape as CFC.concaveOn_log. The expected route (a new uniform-convergence lemma for (x^{1+p} − x)/p) is not needed.

Honest scope

⚠️ This is the ladder's rung L.4, and it does NOT give the data-processing inequality. Operator convexity of x log x is one input to the Effros/Lieb summit (L.5); the summit itself — the noncommutative perspective, operator Jensen, joint convexity of relative entropy — is not attempted, is absent from Mathlib entirely, and is scoped at 3–5 months in specs/lieb-dpi-scoping.md. The hDPI hypothesis of QuantumInfo.strong_subadditivity_of_relEntropy_monotone therefore remains an explicit hypothesis, which is its recorded terminal status (ledger CL-023, qualified-by-design).

The declarations sit in a corpus namespace (OperatorConvexCFC) rather than CFC, so that they cannot shadow upstream while it still lacks them; the MATHLIB-ABSENT tags above make scripts/check-mathlib-absence.sh fail the moment Mathlib lands either, which is the signal to delete this file rather than let the two spellings drift.

Reference: Hansen–Pedersen, Jensen's inequality for operators and Löwner's theorem, Math. Ann. 258 (1982). In-corpus: Mathlib/Analysis/Matrix/OperatorConvex.lean (the Matrix predicate), OperatorConvexBridge.lean (the transport, where Matrix.operatorConvexOn_mul_log lands this on the matrix carrier), specs/operator-convexity-plan.md (L.4).

The Icc 1 2 rpow rung

theorem OperatorConvexCFC.convexOn_cfc_rpowIntegrand₁₂ {B : Type u_2} [CStarAlgebra B] [PartialOrder B] [StarOrderedRing B] {p t : ℝ} (ht : 0 < t) : ConvexOn ℝ (Set.Ici 0) (cfc (p.rpowIntegrand₁₂ t))

theorem OperatorConvexCFC.convexOn_cfcₙ_rpowIntegrand₁₂ {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p t : ℝ} (ht : 0 < t) : ConvexOn ℝ (Set.Ici 0) (cfcₙ (p.rpowIntegrand₁₂ t))

theorem OperatorConvexCFC.convexOn_nnrpow_Ioo12 {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : NNReal} (hp : p ∈ Set.Ioo 1 2) : ConvexOn ℝ (Set.Ici 0) fun (a : A) => a ^ p

★ x log x

theorem OperatorConvexCFC.convexOn_rpow_Ioo12 {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : ℝ} (hp : p ∈ Set.Ioo 1 2) : ConvexOn ℝ (Set.Ici 0) fun (a : A) => a ^ p

Real-exponent version of the Ioo 1 2 operator convexity (mirror of CFC.concaveOn_rpow).

theorem OperatorConvexCFC.convexOn_mul_log {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : ConvexOn ℝ {a : A | IsStrictlyPositive a} fun (a : A) => a * CFC.log a

★ x ↦ x * log x is OPERATOR CONVEX on the strictly positive elements.