Order properties of the operator logarithm

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

Main declarations

• CFC.log_monotoneOn: the logarithm is operator monotone

TODO

• Show that the log is operator concave
• 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.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