feat(analysis/inner_product_space/l2): a Hilbert space is isometrical…

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

docs/overview.yaml

@@ -262,7 +262,7 @@ Analysis:
     orthogonal projection: 'orthogonal_projection'
     reflection: 'reflection'
     orthogonal complement: 'submodule.orthogonal'
-    existence of Hilbert basis: 'exists_is_orthonormal_dense_span'
+    existence of Hilbert basis: 'exists_hilbert_basis'
     eigenvalues from Rayleigh quotient: 'inner_product_space.is_self_adjoint.has_eigenvector_of_is_local_extr_on'
     Fréchet-Riesz representation of the dual of a Hilbert space: 'inner_product_space.to_dual'
 

docs/undergrad.yaml

@@ -427,16 +427,18 @@ Topology:
     Arzela-Ascoli theorem: 'bounded_continuous_function.arzela_ascoli'
   Hilbert spaces:
     Hilbert projection theorem: 'exists_norm_eq_infi_of_complete_convex'
-    orthogonal projection onto closed vector subspaces: 'orthogonal_projection_fn'
+    orthogonal projection onto closed vector subspaces: 'orthogonal_projection'
     dual space: 'normed_space.dual.normed_space'
     Riesz representation theorem: 'inner_product_space.to_dual'
-    inner product spaces $l^2$ and $L^2$: 'measure_theory.L2.inner_product_space'
-    their completeness: 'measure_theory.Lp.complete_space'
-    Hilbert bases, i.e. complete orthonormal sets (in the separable case): 'exists_is_orthonormal_dense_span'
+    inner product space $l^2$: 'lp.inner_product_space'
+    its completeness: 'lp.complete_space'
+    inner product space $L^2$: 'measure_theory.L2.inner_product_space'
+    its completeness: 'measure_theory.Lp.complete_space'
+    Hilbert bases: 'hilbert_basis' # the document specifies "in the separable case" but we don't require this
     example, the Hilbert basis of trigonometric polynomials: 'fourier_Lp'
     its orthonormality: 'orthonormal_fourier'
     its completeness: 'span_fourier_Lp_closure_eq_top'
-    example, classical Hilbert bases of orthogonal polynomials, their orthonormality and completeness: ''
+    example, classical Hilbert bases of orthogonal polynomials: ''
     Lax-Milgram theorem: ''
     $H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem: ''