Commit 2025-09-26 11:53 7cc03ef3

View on Github →

feat: Define strictly positive operators (i.e. positive definite) (#29087)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/StrictPositivity.lean

added theorem IsStrictlyPositive.iff_of_unital

added theorem IsStrictlyPositive.isSelfAdjoint

added theorem IsStrictlyPositive.spectrum_pos

added def IsStrictlyPositive

added theorem IsUnit.isStrictlyPositive

added theorem isStrictlyPositive_algebraMap

added theorem isStrictlyPositive_one

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

added theorem IsStrictlyPositive.add_nonneg

added theorem IsStrictlyPositive.nonneg_add

added theorem isStrictlyPositive_add

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

added theorem StarOrderedRing.isStrictlyPositive_iff_spectrum_pos

added theorem cfcHom_isStrictlyPositive_iff

added theorem cfc_isStrictlyPositive_iff

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

modified theorem CFC.exp_log

modified theorem CFC.log_exp

modified theorem CFC.log_one

added theorem CFC.log_pow'

added theorem CFC.log_smul'

modified theorem CFC.log_zero

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

added theorem IsStrictlyPositive.nnrpow

added theorem IsStrictlyPositive.rpow

added theorem IsStrictlyPositive.sqrt

Modified Mathlib/Topology/UniformSpace/Real.lean