Commit 2021-09-08 14:00 4c7d95fb

View on Github →

feat(analysis/normed_space/inner_product): reflections API (#8884) Reflections, as isometries of an inner product space, were defined in #8660. In this PR, various elementary lemmas filling out the API:

Lemmas about reflection through a subspace K, of a point which is in (i) K itself; (ii) the orthogonal complement of K.
Lemmas relating the orthogonal projection/reflection on the submodule.map of a subspace, with the orthogonal projection/reflection on the original subspace.
Lemma characterizing the reflection in the trivial subspace.

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

added theorem orthogonal_projection_eq_self_iff

added theorem orthogonal_projection_map_apply

added theorem reflection_bot

added theorem reflection_eq_self_iff

added theorem reflection_map

added theorem reflection_map_apply

added theorem reflection_mem_subspace_eq_self

added theorem reflection_mem_subspace_orthogonal_complement_eq_neg

added theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg

added theorem reflection_orthogonal_complement_singleton_eq_neg