Commit 2022-01-20 10:32 5a40c33f

feat(analysis/inner_product_space/l2): a Hilbert space is isometrically isomorphic to ℓ² (#11255) Define orthogonal_family.linear_isometry_equiv: the isometric isomorphism of a Hilbert space E with a Hilbert sum of a family of Hilbert spaces G i, induced by individual isometries of each G i into E whose images are orthogonal and span a dense subset of E. Define a Hilbert basis of E to be an isometric isomorphism of E with ℓ²(ι, 𝕜), the Hilbert sum of ι copies of 𝕜. Prove that an orthonormal family of vectors in E whose span is dense in E has an associated Hilbert basis. Prove that every Hilbert space admit a Hilbert basis. Delete three lemmas maximal_orthonormal_iff_dense_span, exists_subset_is_orthonormal_dense_span, exists_is_orthonormal_dense_span which previously expressed this existence theorem in a more awkward way (before the definition ℓ²(ι, 𝕜) was available).