Commit 2020-08-03 11:29 6079ef96

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.