Commit 2023-05-26 15:32 518697a8

View on Github →

feat: port Analysis.InnerProductSpace.Projection (#4393) This PR also increase the priority of Submodule.bot_ext.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

Created Mathlib/Analysis/InnerProductSpace/Projection.lean

added theorem Dense.eq_of_inner_left

added theorem Dense.eq_of_inner_right

added theorem Dense.eq_of_sub_mem_orthogonal

added theorem Dense.eq_zero_of_inner_left

added theorem Dense.eq_zero_of_inner_right

added theorem Dense.eq_zero_of_mem_orthogonal

added theorem LinearIsometry.map_orthogonalProjection'

added theorem LinearIsometry.map_orthogonalProjection

added theorem LinearIsometryEquiv.reflections_generate

added theorem LinearIsometryEquiv.reflections_generate_dim

added theorem LinearIsometryEquiv.reflections_generate_dim_aux

added theorem OrthogonalFamily.isInternal_iff

added theorem OrthogonalFamily.isInternal_iff_of_isComplete

added theorem Submodule.IsOrtho.orthogonalProjection_comp_subtypeL

added theorem Submodule.exists_sum_mem_mem_orthogonal

added theorem Submodule.finrank_add_finrank_orthogonal'

added theorem Submodule.finrank_add_finrank_orthogonal

added theorem Submodule.finrank_add_inf_finrank_orthogonal'

added theorem Submodule.finrank_add_inf_finrank_orthogonal

added theorem Submodule.isCompl_orthogonal_of_completeSpace

added theorem Submodule.orthogonal_eq_bot_iff

added theorem Submodule.orthogonal_orthogonal

added theorem Submodule.orthogonal_orthogonal_eq_closure

added theorem Submodule.sup_orthogonal_inf_of_completeSpace

added theorem Submodule.sup_orthogonal_of_completeSpace

added theorem Submodule.topologicalClosure_eq_top_iff

added theorem Submodule.triorthogonal_eq_orthogonal

added theorem eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero

added theorem eq_orthogonalProjection_of_eq_submodule

added theorem eq_orthogonalProjection_of_mem_of_inner_eq_zero

added theorem eq_orthogonalProjection_of_mem_orthogonal'

added theorem eq_orthogonalProjection_of_mem_orthogonal

added theorem eq_sum_orthogonalProjection_self_orthogonalComplement

added theorem exists_norm_eq_iInf_of_complete_convex

added theorem exists_norm_eq_iInf_of_complete_subspace

added theorem finrank_orthogonal_span_singleton

added theorem id_eq_sum_orthogonalProjection_self_orthogonalComplement

added theorem inner_orthogonalProjection_eq_of_mem_left

added theorem inner_orthogonalProjection_eq_of_mem_right

added theorem inner_orthogonalProjection_left_eq_right

added theorem maximal_orthonormal_iff_basis_of_finiteDimensional

added theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot

added theorem norm_eq_iInf_iff_inner_eq_zero

added theorem norm_eq_iInf_iff_real_inner_eq_zero

added theorem norm_eq_iInf_iff_real_inner_le_zero

added theorem norm_sq_eq_add_norm_sq_projection

added def orthogonalProjection

added def orthogonalProjectionFn

added theorem orthogonalProjectionFn_eq

added theorem orthogonalProjectionFn_inner_eq_zero

added theorem orthogonalProjectionFn_mem

added theorem orthogonalProjectionFn_norm_sq

added theorem orthogonalProjection_bot

added theorem orthogonalProjection_coe_linearMap_eq_linearProj

added theorem orthogonalProjection_comp_subtypeL_eq_zero_iff

added theorem orthogonalProjection_eq_linear_proj

added theorem orthogonalProjection_eq_self_iff

added theorem orthogonalProjection_inner_eq_zero

added theorem orthogonalProjection_isSymmetric

added theorem orthogonalProjection_map_apply

added theorem orthogonalProjection_mem_subspace_eq_self

added theorem orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero

added theorem orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero

added theorem orthogonalProjection_minimal

added theorem orthogonalProjection_norm_le

added theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero

added theorem orthogonalProjection_orthogonalProjection_of_le

added theorem orthogonalProjection_singleton

added theorem orthogonalProjection_tendsto_closure_iSup

added theorem orthogonalProjection_tendsto_self

added theorem orthogonalProjection_unit_singleton

added def reflection

added def reflectionLinearEquiv

added theorem reflection_apply

added theorem reflection_bot

added theorem reflection_eq_self_iff

added theorem reflection_inv

added theorem reflection_involutive

added theorem reflection_map

added theorem reflection_map_apply

added theorem reflection_mem_subspace_eq_self

added theorem reflection_mem_subspace_orthogonalComplement_eq_neg

added theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg

added theorem reflection_mul_reflection

added theorem reflection_orthogonalComplement_singleton_eq_neg

added theorem reflection_reflection

added theorem reflection_sub

added theorem reflection_symm

added theorem reflection_trans_reflection

added theorem smul_orthogonalProjection_singleton

added theorem sub_orthogonalProjection_mem_orthogonal