Commit 2026-06-10 15:26 5fd04c7e

View on Github →

refactor(Analysis/InnerProductSpace/Projection): redefine orthogonalProjectionOnto via projectionOntoL (#39041) Now that we have Submodule.IsTopCompl and Submodule.projectionOntoL, we can define Submodule.orthogonalProjectionOnto directly this way instead of needing an implementation definition that should be private anyway. This also renames Submodule.isCompl_orthogonal_of_hasOrthogonalProjection to Submodule.isCompl_orthogonal.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/ProdL2.lean

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

deleted theorem Submodule.eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero

added theorem Submodule.isCompl_orthogonal

added theorem Submodule.isTopCompl_orthogonal

added theorem Submodule.norm_projection_orthogonal_le

deleted def Submodule.orthogonalProjectionFn

deleted theorem Submodule.orthogonalProjectionFn_inner_eq_zero

deleted theorem Submodule.orthogonalProjectionFn_mem

modified theorem Submodule.orthogonalProjectionFn_norm_sq

modified def Submodule.orthogonalProjectionOnto

modified theorem Submodule.orthogonalProjectionOnto_norm_le

modified theorem Submodule.starProjection_inner_eq_zero

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

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

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

Modified Mathlib/Geometry/Euclidean/Projection.lean

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem Submodule.projectionOnto_apply_of_mem_left

added theorem Submodule.projection_apply_of_mem_left