Commit 2025-07-15 08:11 e7670e56

View on Github →

chore(Analysis/InnerProductSpace/Projection): deprecating subtypeL ∘ orthogonalProjection in favor of starProjection (#26877) This deprecates all U.subtypeL ∘L U.orthogonalProjection and (U.orthogonalProjection v : E) in favor of U.starProjection and U.starProjection v respectively in Analysis/InnerProductSpace/Projection and other files.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

modified theorem isStarProjection_starProjection

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

deleted theorem LinearIsometry.map_orthogonalProjection'

deleted theorem LinearIsometry.map_orthogonalProjection

added theorem LinearIsometry.map_starProjection'

added theorem LinearIsometry.map_starProjection

added theorem Submodule.coe_orthogonalProjection_apply

deleted theorem Submodule.eq_orthogonalProjection_of_eq_submodule

deleted theorem Submodule.eq_orthogonalProjection_of_mem_of_inner_eq_zero

deleted theorem Submodule.eq_orthogonalProjection_of_mem_orthogonal'

deleted theorem Submodule.eq_orthogonalProjection_of_mem_orthogonal

added theorem Submodule.eq_starProjection_of_eq_submodule

added theorem Submodule.eq_starProjection_of_mem_of_inner_eq_zero

added theorem Submodule.eq_starProjection_of_mem_orthogonal'

added theorem Submodule.eq_starProjection_of_mem_orthogonal

deleted theorem Submodule.id_eq_sum_orthogonalProjection_self_orthogonalComplement

added theorem Submodule.id_eq_sum_starProjection_self_orthogonalComplement

deleted theorem Submodule.inner_orthogonalProjection_left_eq_right

added theorem Submodule.inner_starProjection_left_eq_right

deleted theorem Submodule.orthogonalProjection_add_orthogonalProjection_orthogonal

deleted theorem Submodule.orthogonalProjection_eq_self_iff

deleted theorem Submodule.orthogonalProjection_inner_eq_zero

deleted theorem Submodule.orthogonalProjection_isSymmetric

deleted theorem Submodule.orthogonalProjection_map_apply

deleted theorem Submodule.orthogonalProjection_minimal

deleted theorem Submodule.orthogonalProjection_orthogonalProjection_of_le

deleted theorem Submodule.orthogonalProjection_orthogonal_val

deleted theorem Submodule.orthogonalProjection_singleton

added theorem Submodule.orthogonalProjection_starProjection_of_le

deleted theorem Submodule.orthogonalProjection_tendsto_closure_iSup

deleted theorem Submodule.orthogonalProjection_tendsto_self

deleted theorem Submodule.orthogonalProjection_unit_singleton

deleted theorem Submodule.re_inner_orthogonalProjection_eq_normSq

deleted theorem Submodule.re_inner_orthogonalProjection_nonneg

added theorem Submodule.re_inner_starProjection_eq_normSq

added theorem Submodule.re_inner_starProjection_nonneg

modified theorem Submodule.reflection_apply

deleted theorem Submodule.smul_orthogonalProjection_singleton

added theorem Submodule.smul_starProjection_singleton

added theorem Submodule.starProjection_add_starProjection_orthogonal

added theorem Submodule.starProjection_eq_self_iff

added theorem Submodule.starProjection_inner_eq_zero

added theorem Submodule.starProjection_isSymmetric

added theorem Submodule.starProjection_map_apply

added theorem Submodule.starProjection_minimal

added theorem Submodule.starProjection_orthogonal_val

added theorem Submodule.starProjection_singleton

added theorem Submodule.starProjection_tendsto_closure_iSup

added theorem Submodule.starProjection_tendsto_self

added theorem Submodule.starProjection_unit_singleton

deleted theorem Submodule.sub_orthogonalProjection_mem_orthogonal

added theorem Submodule.sub_starProjection_mem_orthogonal

Modified Mathlib/Geometry/Euclidean/Projection.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean