mathlib

5a40c33f - feat(analysis/inner_product_space/l2): a Hilbert space is isometrically isomorphic to `ℓ²` (#11255)

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).