Commit 2025-08-19 21:26 0978b662

View on Github →

feat(Analysis/InnerProductSpace/Projection): define symmetric projections (#27642) This pr defines symmetric projections (LinearMap.IsSymmetricProjection) which are simply symmetric idempotents. This generalizes most of the results concerning star projection operators (since it needs completeness). In a complete space, these two definitions obviously coincide. An operator p is a symmetric projection if and only if it equals (range p).starProjection. This is a more general version of isStarProjection_iff_eq_starProjection_range.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

deleted theorem ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range

added theorem ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection

added theorem LinearMap.isStarProjection_iff_isSymmetricProjection

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

deleted theorem LinearMap.IsPositive.of_isStarProjection

added theorem LinearMap.IsPositive.of_isSymmetricProjection

Modified Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

added theorem LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range

added theorem LinearMap.isSymmetricProjection_iff_eq_coe_starProjection

added theorem LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range

added theorem Submodule.isSymmetricProjection_starProjection

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

added theorem ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range

added theorem LinearMap.IsSymmetricProjection.ext_iff

added structure LinearMap.IsSymmetricProjection

added theorem Submodule.IsCompl.projection_isSymmetricProjection_iff