Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-22 17:05 d569d634

View on Github →

refactor(analysis/inner_product_space, geometry/euclidean) range of orthogonal projection (#5408) Previously, the orthogonal projection was defined for all subspaces of an inner product space, with the junk value id if the space was not complete; then all nontrivial lemmas required a hypothesis of completeness (and nonemptiness for the affine orthogonal projection). Change this to a definition only for subspaces K satisfying [complete_space K] (and [nonempty K] for the affine orthogonal projection). Previously, the orthogonal projection was a linear map from E to E. Redefine it to be a linear map from E to K. Zulip

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

modified theorem eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero

added theorem eq_orthogonal_projection_of_eq_submodule

modified theorem eq_orthogonal_projection_of_mem_of_inner_eq_zero

modified def orthogonal_projection

deleted theorem orthogonal_projection_def

modified def orthogonal_projection_fn

modified theorem orthogonal_projection_fn_eq

modified theorem orthogonal_projection_fn_inner_eq_zero

modified theorem orthogonal_projection_fn_mem

modified theorem orthogonal_projection_inner_eq_zero

deleted theorem orthogonal_projection_mem

deleted def orthogonal_projection_of_complete

Modified src/data/finset/basic.lean

Modified src/geometry/euclidean/basic.lean

modified theorem euclidean_geometry.dist_orthogonal_projection_eq_zero_iff

modified theorem euclidean_geometry.dist_orthogonal_projection_ne_zero_of_not_mem

modified theorem euclidean_geometry.dist_reflection

modified theorem euclidean_geometry.dist_reflection_eq_of_mem

added theorem euclidean_geometry.eq_orthogonal_projection_of_eq_subspace

added theorem euclidean_geometry.eq_reflection_of_eq_subspace

modified theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection

modified theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection_fn

modified def euclidean_geometry.orthogonal_projection

deleted theorem euclidean_geometry.orthogonal_projection_def

modified theorem euclidean_geometry.orthogonal_projection_eq_self_iff

modified def euclidean_geometry.orthogonal_projection_fn

modified theorem euclidean_geometry.orthogonal_projection_fn_eq

modified theorem euclidean_geometry.orthogonal_projection_fn_mem

modified theorem euclidean_geometry.orthogonal_projection_fn_mem_orthogonal

modified theorem euclidean_geometry.orthogonal_projection_fn_vsub_mem_direction_orthogonal

modified theorem euclidean_geometry.orthogonal_projection_linear

modified theorem euclidean_geometry.orthogonal_projection_mem

modified theorem euclidean_geometry.orthogonal_projection_mem_orthogonal

deleted def euclidean_geometry.orthogonal_projection_of_nonempty_of_complete

deleted theorem euclidean_geometry.orthogonal_projection_of_nonempty_of_complete_eq

modified theorem euclidean_geometry.orthogonal_projection_orthogonal_projection

modified theorem euclidean_geometry.orthogonal_projection_vadd_eq_self

modified theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction

modified theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction_orthogonal

modified def euclidean_geometry.reflection

modified theorem euclidean_geometry.reflection_apply

modified theorem euclidean_geometry.reflection_eq_iff_orthogonal_projection_eq

modified theorem euclidean_geometry.reflection_eq_self_iff

modified theorem euclidean_geometry.reflection_involutive

modified theorem euclidean_geometry.reflection_mem_of_le_of_mem

modified theorem euclidean_geometry.reflection_orthogonal_vadd

modified theorem euclidean_geometry.reflection_reflection

modified theorem euclidean_geometry.reflection_symm

modified theorem euclidean_geometry.reflection_vadd_smul_vsub_orthogonal_projection

modified theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction

modified theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction_orthogonal

Modified src/geometry/euclidean/circumcenter.lean

modified theorem euclidean_geometry.dist_eq_iff_dist_orthogonal_projection_eq

modified theorem euclidean_geometry.dist_set_eq_iff_dist_orthogonal_projection_eq

modified theorem euclidean_geometry.exists_dist_eq_iff_exists_dist_orthogonal_projection_eq

Modified src/geometry/euclidean/monge_point.lean

Modified src/linear_algebra/affine_space/affine_subspace.lean

added theorem affine_subspace.coe_vadd

added theorem affine_subspace.coe_vsub