Commit 2025-10-17 18:28 6e8691ff

View on Github →

refactor(Analysis/InnerProductSpace/Positive): generalize positivity to use IsSymmetric instead of IsSelfAdjoint and CompleteSpace (#30000) The definition of ContinuousLinearMap.IsPositive remains the same in complete spaces, but this allows us to use positivity and the partial order without needing completeness. The new definition is now exactly the same as LinearMap.IsPositive but for continuous linear maps. To use the old definition (i.e., IsSelfAdjoint and ...), instead of unfolding, use ContinuousLinearMap.isPositive_def'. isPositive_iff is renamed to isPositive_iff', and isPositive_iff points to the same thing but with IsSymmetric instead of IsSelfAdjoint.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

modified theorem ContinuousLinearMap.IsIdempotentElem.TFAE

modified theorem ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint

modified theorem ContinuousLinearMap.IsPositive.adjoint_conj

modified theorem ContinuousLinearMap.IsPositive.conj_adjoint

modified theorem ContinuousLinearMap.IsPositive.inner_left_eq_inner_right

modified theorem ContinuousLinearMap.IsPositive.isSelfAdjoint

added theorem ContinuousLinearMap.IsPositive.isSymmetric

modified theorem ContinuousLinearMap.IsPositive.of_isStarProjection

modified theorem ContinuousLinearMap.isPositive_adjoint_comp_self

added theorem ContinuousLinearMap.isPositive_def'

added theorem ContinuousLinearMap.isPositive_def

added theorem ContinuousLinearMap.isPositive_id

added theorem ContinuousLinearMap.isPositive_iff'

modified theorem ContinuousLinearMap.isPositive_one

modified theorem ContinuousLinearMap.isPositive_self_comp_adjoint

modified theorem ContinuousLinearMap.isPositive_zero

modified theorem ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map

added theorem LinearMap.isPositive_id

Modified Mathlib/Analysis/InnerProductSpace/StarOrder.lean