Commit 2023-07-15 07:15 41a80d7f

View on Github →

Generalize orthogonalProjection (#5917) Introduce a typeclass HasOrthogonalProjection and use it instead of [CompleteSpace K] in the definitions of orthogonalProjection and reflection, as well as lemmas about these definitions. This way we do not need a [CompleteSpace E] assumption to talk about orthogonalProjection (𝕜 ∙ v). Fixes #5877

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

modified theorem Dense.eq_of_sub_mem_orthogonal

modified theorem Dense.eq_zero_of_inner_left

modified theorem Submodule.IsOrtho.orthogonalProjection_comp_subtypeL

added theorem Submodule.exists_add_mem_mem_orthogonal

deleted theorem Submodule.exists_sum_mem_mem_orthogonal

modified theorem Submodule.isCompl_orthogonal_of_completeSpace

modified theorem Submodule.orthogonal_eq_bot_iff

modified theorem Submodule.orthogonal_orthogonal

modified theorem Submodule.sup_orthogonal_of_completeSpace

modified theorem eq_orthogonalProjection_of_eq_submodule

modified theorem eq_orthogonalProjection_of_mem_orthogonal'

modified theorem eq_orthogonalProjection_of_mem_orthogonal

deleted theorem eq_sum_orthogonalProjection_self_orthogonalComplement

modified theorem id_eq_sum_orthogonalProjection_self_orthogonalComplement

modified theorem inner_orthogonalProjection_eq_of_mem_left

modified theorem inner_orthogonalProjection_eq_of_mem_right

modified theorem inner_orthogonalProjection_left_eq_right

modified theorem norm_sq_eq_add_norm_sq_projection

added theorem orthogonalProjection_add_orthogonalProjection_orthogonal

modified theorem orthogonalProjection_coe_linearMap_eq_linearProj

modified theorem orthogonalProjection_comp_subtypeL_eq_zero_iff

modified theorem orthogonalProjection_eq_linear_proj

modified theorem orthogonalProjection_isSymmetric

modified theorem orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero

modified theorem orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero

modified theorem orthogonalProjection_minimal

added theorem orthogonalProjection_orthogonal

modified theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero

modified theorem orthogonalProjection_orthogonalProjection_of_le

added theorem orthogonalProjection_orthogonal_val

modified theorem reflection_mem_subspace_orthogonalComplement_eq_neg

modified theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg

added theorem reflection_orthogonal

modified theorem reflection_orthogonalComplement_singleton_eq_neg

added theorem reflection_orthogonal_apply

modified theorem reflection_sub

Modified Mathlib/Geometry/Euclidean/Basic.lean

modified theorem EuclideanGeometry.dist_reflection

modified theorem EuclideanGeometry.dist_reflection_eq_of_mem

modified def EuclideanGeometry.orthogonalProjectionFn

modified theorem EuclideanGeometry.orthogonalProjectionFn_eq

modified theorem EuclideanGeometry.orthogonalProjectionFn_mem

modified theorem EuclideanGeometry.orthogonalProjection_mem

modified def EuclideanGeometry.reflection

modified theorem EuclideanGeometry.reflection_apply

modified theorem EuclideanGeometry.reflection_eq_self_iff

modified theorem EuclideanGeometry.reflection_involutive

modified theorem EuclideanGeometry.reflection_orthogonal_vadd

modified theorem EuclideanGeometry.reflection_reflection

modified theorem EuclideanGeometry.reflection_symm

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

modified theorem EuclideanGeometry.existsUnique_dist_eq_of_insert