Commit 2025-11-26 02:38 7a0e478d

View on Github →

feat(CStarAlgebra): the log is operator monotone (#30894) This PR shows that the logarithm is operator monotone, i.e. CFC.log is monotone on {a : A | IsStrictlyPositive a} where A is a unital C*-algebra.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Exponential.lean

added theorem Real.norm_exp_sub_one_sub_id_le

Created Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean

added theorem CFC.log_le_log

added theorem CFC.log_monotoneOn

added theorem CFC.tendsto_cfc_rpow_sub_one_log

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

added theorem CFC.rpow_eq_cfc_real

Created Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean

added theorem Real.norm_inv_mul_rpow_sub_one_sub_log_le

added theorem Real.tendstoLocallyUniformlyOn_rpow_sub_one_log

added theorem tendsto_rpow_sub_one_log