Order properties of the operator logarithm

This file shows that the logarithm is operator monotone and concave, i.e. that CFC.log is monotone and concave on the strictly positive elements of a unital C⋆-algebra.

Main declarations

• CFC.log_monotoneOn: the logarithm is operator monotone
• CFC.concaveOn_log: the logarithm is operator concave

TODO

• Show that x => x * log x is operator convex

theorem CFC.tendsto_cfc_rpow_sub_one_log {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : IsStrictlyPositive a := by cfc_tac) : Filter.Tendsto (fun (p : ℝ) => cfc (fun (x : ℝ) => p⁻¹ * (x ^ p - 1)) a) (nhdsWithin 0 (Set.Ioi 0)) (nhds (log a))

theorem CFC.tendsto_ite_cfc_rpow_sub_one_ite_log {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Filter.Tendsto (fun (p : ℝ) (a : A) => if a ∈ {b : A | IsStrictlyPositive b} then cfc (fun (x : ℝ) => p⁻¹ * (x ^ p - 1)) a else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds fun (a : A) => if a ∈ {b : A | IsStrictlyPositive b} then log a else 0)

theorem CFC.log_monotoneOn {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : MonotoneOn log {a : A | IsStrictlyPositive a}

log is operator monotone.

theorem CFC.log_le_log {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hab : a ≤ b) (ha : IsStrictlyPositive a := by cfc_tac) : log a ≤ log b

theorem CFC.concaveOn_log {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : ConcaveOn ℝ {a : A | IsStrictlyPositive a} log

log is operator concave.