Order properties of CFC.rpow

This file shows that a ↦ a ^ p is monotone for p ∈ [0, 1], where a is an element of a C⋆-algebra. The proof makes use of the integral representation of rpow in Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation.

Main declarations

• CFC.monotone_nnrpow, CFC.monotone_rpow: a ↦ a ^ p is operator monotone for p ∈ [0,1]
• CFC.monotone_sqrt: CFC.sqrt is operator monotone
• CFC.concaveOn_nnrpow, CFC.concaveOn_rpow: a ↦ a ^ p is operator concave for p ∈ [0,1]
• CFC.concaveOn_sqrt: CFC.sqrt is operator concave

TODO

• Show that rpow over Icc (-1) 0 is operator antitone and operator convex
• Show operator convexity of rpow over Icc 1 2

References

• [Car10] Eric A. Carlen, "Trace inequalities and quantum entropies: An introductory course" (see Lemma 2.8)

theorem CFC.monotone_nnrpow {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : NNReal} (hp : p ∈ Set.Icc 0 1) : Monotone fun (a : A) => a ^ p

a ↦ a ^ p is operator monotone for p ∈ [0,1].

theorem CFC.monotone_sqrt {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Monotone sqrt

CFC.sqrt is operator monotone.

theorem CFC.nnrpow_le_nnrpow {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : NNReal} (hp : p ∈ Set.Icc 0 1) {a b : A} (hab : a ≤ b) : a ^ p ≤ b ^ p

theorem CFC.sqrt_le_sqrt {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a b : A) (hab : a ≤ b) : sqrt a ≤ sqrt b

theorem CFC.concaveOn_nnrpow {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : NNReal} (hp : p ∈ Set.Icc 0 1) : ConcaveOn ℝ (Set.Ici 0) fun (a : A) => a ^ p

a ↦ a ^ p is operator concave for p ∈ [0,1].

theorem CFC.concaveOn_sqrt {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : ConcaveOn ℝ (Set.Ici 0) sqrt

The square root is operator concave.

theorem CFC.monotone_rpow {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : ℝ} (hp : p ∈ Set.Icc 0 1) : Monotone fun (a : A) => a ^ p

a ↦ a ^ p is operator monotone for p ∈ [0,1].

theorem CFC.rpow_le_rpow {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : ℝ} (hp : p ∈ Set.Icc 0 1) {a b : A} (hab : a ≤ b) : a ^ p ≤ b ^ p

theorem CFC.concaveOn_rpow {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p : ℝ} (hp : p ∈ Set.Icc 0 1) : ConcaveOn ℝ (Set.Ici 0) fun (a : A) => a ^ p

a ↦ a ^ p is operator concave for p ∈ [0,1].