feat(analysis/normed_space/real_inner_product): orthogonal projection (#3563)
`analysis.normed_space.real_inner_product` proves the existence of
orthogonal projections onto complete subspaces, but only in the form
of an existence theorem without a corresponding `def` for the function
that is proved to exist. Add the corresponding `def` of
`orthogonal_projection` as a `linear_map` and lemmas with the basic
properties, extracted from the existing results with `some` and
`some_spec`.
For convenience in constructing the `linear_map`, some lemmas are
first proved for a version of the orthogonal projection as an
unbundled function, then used in the definition of the bundled
`linear_map` version, then restarted for the bundled version (the two
versions of each lemma being definitionally equal; the bundled version
is considered the main version that should be used in all subsequent
code).
This is preparation for defining the corresponding operation for
Euclidean affine spaces as an `affine_map`.
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
mathlib
6079ef96 - feat(analysis/normed_space/real_inner_product): orthogonal projection (#3563)
