Commit 2025-07-27 22:47 c9e3dfad

refactor(Analysis/InnerProductSpace/Positive): changing positivity on linear maps to use IsSymmetric instead of IsSelfAdjoint and finite-dimensionality (#27089) With this definition, the partial order would be defined on linear maps without needing finite-dimensionality. Also, when continuous linear maps are positive, then so are their coercions into linear maps, again, without needing finite-dimensionality. Moving the definition of positivity for linear maps before the one for continuous linear maps allows us to use results already done in linear maps for continuous linear maps. There's no need to have duplicate proofs. In essenece:

• This changes the definition of LinearMap.IsPositive to IsSymmetric T instead of IsSelfAdjoint T and removes the finite-dimensional hypothesis.
• This changes the order of the whole file: starting with linear maps and ending with continuous linear maps, instead of the other way around.
• Adds LinearMap.IsSymmetric.natCast.
• Adds LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric, which is then used to golf ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint (note the change of order for isPositive_iff_isSelfAdjoint and IsPositive.of_isStarProjection).
• Final addition: ContinuousLinearMap.coe_le_coe_iff which just says f.toLinearMap ≤ g.toLinearMap iff f ≤ g.
• There are two results (LinearMap.IsPositive.conj_adjoint and LinearMap.IsPositive.adjoint_conj) which are in the middle of the ContinuousLinearMap namespace. The reason for this is to utilize the proofs already done for continuous maps instead of having duplicate proofs.