feat(analysis/inner_product_space/l2_space): define is_hilbert_sum …

…predicate (#15772)

This introduces a predicate on a space `E` and a family of linear isometries `V : Π i, G i →ₗᵢ[𝕜] E` expressing that the associated map `lp G 2 →ₗᵢ[𝕜] E` is surjective. As explained in the docstring, this is *somewhat* analogous to `direct_sum.is_internal`, but **not completely**, since it is a predicate on embeddings rather than subspaces (so in a sense it is more category-theoretic, even though we don't implement it as a universal property). 

I am aware that introducing this inconsistency is not ideal, but I believe this is the cleanest thing to do here, because it follows the design of `orthogonal_family`. 

I also have a more practical motivation : in a following PR, I will introduce a way to concatenate Hilbert bases from mutually orthogonal "subspaces" with dense span to form a Hilbert basis for the whole space. Without this, the natural way would be to state this with hypotheses `orthogonal_family 𝕜 V` and `⊤ ≤ (⨆ (i : ι), (V i).to_linear_map.range).topological_closure`. First, this is quite verbose for such a common set of hypotheses, but the real problem comes with the fact that for actual subspaces you want to replace this second hypothesis by `⊤ ≤ (⨆ (i : ι), F i).topological_closure`, so you essentially have to duplicate the API. With this constructions, these two variants just correspond to two different ways of proving `is_hilbert_sum`.

I think we should consider doing a similar thing for direct sums, stating the fact that the map `direct_sum.to_module` is bijective, but it will be harder since linear maps are not injective in general like linear isometries are.

src/analysis/inner_product_space/l2_space.lean

@@ -16,17 +16,24 @@ dependent functions `f : Π i, G i` for which `∑' i, ∥f i∥ ^ 2`, the sum o
 summable.  This construction is sometimes called the *Hilbert sum* of the family `G`.  By choosing
 `G` to be `ι → 𝕜`, the Hilbert space `ℓ²(ι, 𝕜)` may be seen as a special case of this construction.
 
+We also define a *predicate* `is_hilbert_sum 𝕜 E V`, where `V : Π i, G i →ₗᵢ[𝕜] E`, expressing that
+that `V` is an `orthogonal_family` and that the associated map `lp G 2 →ₗᵢ[𝕜] E` is surjective.
+
 ## Main definitions
 
 * `orthogonal_family.linear_isometry`: Given a Hilbert space `E`, a family `G` of inner product
   spaces and a family `V : Π i, G i →ₗᵢ[𝕜] E` of isometric embeddings of the `G i` into `E` with
   mutually-orthogonal images, there is an induced isometric embedding of the Hilbert sum of `G`
   into `E`.
 
-* `orthogonal_family.linear_isometry_equiv`: Given a Hilbert space `E`, a family `G` of inner
-  product spaces and a family `V : Π i, G i →ₗᵢ[𝕜] E` of isometric embeddings of the `G i` into `E`
-  with mutually-orthogonal images whose span is dense in `E`, there is an induced isometric
-  isomorphism of the Hilbert sum of `G` with `E`.
+* `is_hilbert_sum`: Given a Hilbert space `E`, a family `G` of inner product
+  spaces and a family `V : Π i, G i →ₗᵢ[𝕜] E` of isometric embeddings of the `G i` into `E`,
+  `is_hilbert_sum 𝕜 E V` means that `V` is an `orthogonal_family` and that the above
+  linear isometry is surjective.
+
+* `is_hilbert_sum.linear_isometry_equiv`: If a Hilbert space `E` is a Hilbert sum of the
+  inner product spaces `G i` with respect to the family `V : Π i, G i →ₗᵢ[𝕜] E`, then the
+  corresponding `orthogonal_family.linear_isometry` can be upgraded to a `linear_isometry_equiv`.
 
 * `hilbert_basis`: We define a *Hilbert basis* of a Hilbert space `E` to be a structure whose single
   field `hilbert_basis.repr` is an isometric isomorphism of `E` with `ℓ²(ι, 𝕜)` (i.e., the Hilbert
@@ -242,69 +249,114 @@ begin
     exact hV.linear_isometry.isometry.uniform_inducing.is_complete_range.is_closed }
 end
 
-/-- A mutually orthogonal family of complete subspaces of `E`, whose range is dense in `E`, induces
-a isometric isomorphism from E to `lp 2` of the subspaces.
+end orthogonal_family
+
+section is_hilbert_sum
+
+variables (𝕜 E) (V : Π i, G i →ₗᵢ[𝕜] E) (F : ι → submodule 𝕜 E)
+include cplt
+
+/-- Given a family of Hilbert spaces `G : ι → Type*`, a Hilbert sum of `G` consists of a Hilbert
+space `E` and an orthogonal family `V : Π i, G i →ₗᵢ[𝕜] E` such that the induced isometry
+`Φ : lp G 2 → E` is surjective.
+
+Keeping in mind that `lp G 2` is "the" external Hilbert sum of `G : ι → Type*`, this is analogous
+to `direct_sum.is_internal`, except that we don't express it in terms of actual submodules. -/
+@[protect_proj] structure is_hilbert_sum : Prop := of_surjective ::
+(orthogonal_family : orthogonal_family 𝕜 V)
+(surjective_isometry : function.surjective (orthogonal_family.linear_isometry))
+
+variables {𝕜 E V}
+
+/-- If `V : Π i, G i →ₗᵢ[𝕜] E` is an orthogonal family such that the supremum of the ranges of
+`V i` is dense, then `(E, V)` is a Hilbert sum of `G`. -/
+lemma is_hilbert_sum.mk [Π i, complete_space $ G i]
+  (hVortho : orthogonal_family 𝕜 V)
+  (hVtotal : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) :
+  is_hilbert_sum 𝕜 E V :=
+{ orthogonal_family := hVortho,
+  surjective_isometry :=
+  begin
+    rw [←linear_isometry.coe_to_linear_map],
+    exact linear_map.range_eq_top.mp (eq_top_iff.mpr $
+      hVtotal.trans_eq hVortho.range_linear_isometry.symm)
+  end }
+
+/-- This is `orthogonal_family.is_hilbert_sum` in the case of actual inclusions from subspaces. -/
+lemma is_hilbert_sum.mk_internal [Π i, complete_space $ F i]
+  (hFortho : @orthogonal_family 𝕜 E _ _ _ (λ i, F i) _ (λ i, (F i).subtypeₗᵢ))
+  (hFtotal : ⊤ ≤ (⨆ i, (F i)).topological_closure) :
+  @is_hilbert_sum _ 𝕜 _ E _ _ (λ i, F i) _ (λ i, (F i).subtypeₗᵢ) :=
+is_hilbert_sum.mk hFortho (by simpa [subtypeₗᵢ_to_linear_map, range_subtype] using hFtotal)
+
+/-- *A* Hilbert sum `(E, V)` of `G` is canonically isomorphic to *the* Hilbert sum of `G`,
+i.e `lp G 2`.
 
 Note that this goes in the opposite direction from `orthogonal_family.linear_isometry`. -/
-noncomputable def linear_isometry_equiv [Π i, complete_space (G i)]
-  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) :
+noncomputable def is_hilbert_sum.linear_isometry_equiv (hV : is_hilbert_sum 𝕜 E V) :
   E ≃ₗᵢ[𝕜] lp G 2 :=
 linear_isometry_equiv.symm $
 linear_isometry_equiv.of_surjective
-hV.linear_isometry
-begin
-  rw [←linear_isometry.coe_to_linear_map],
-  exact linear_map.range_eq_top.mp (eq_top_iff.mpr $ hV'.trans_eq hV.range_linear_isometry.symm)
-end
+hV.orthogonal_family.linear_isometry hV.surjective_isometry
 
-/-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an orthogonal family `G`,
+/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G` and `lp G 2`,
 a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`. -/
-protected lemma linear_isometry_equiv_symm_apply [Π i, complete_space (G i)]
-  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (w : lp G 2) :
-  (hV.linear_isometry_equiv hV').symm w = ∑' i, V i (w i) :=
-by simp [orthogonal_family.linear_isometry_equiv, orthogonal_family.linear_isometry_apply]
+protected lemma is_hilbert_sum.linear_isometry_equiv_symm_apply
+  (hV : is_hilbert_sum 𝕜 E V) (w : lp G 2) :
+  hV.linear_isometry_equiv.symm w = ∑' i, V i (w i) :=
+by simp [is_hilbert_sum.linear_isometry_equiv, orthogonal_family.linear_isometry_apply]
 
-/-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an orthogonal family `G`,
+/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G` and `lp G 2`,
 a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`, and this
 sum indeed converges. -/
-protected lemma has_sum_linear_isometry_equiv_symm [Π i, complete_space (G i)]
-  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (w : lp G 2) :
-  has_sum (λ i, V i (w i)) ((hV.linear_isometry_equiv hV').symm w) :=
-by simp [orthogonal_family.linear_isometry_equiv, orthogonal_family.has_sum_linear_isometry]
+protected lemma is_hilbert_sum.has_sum_linear_isometry_equiv_symm
+  (hV : is_hilbert_sum 𝕜 E V) (w : lp G 2) :
+  has_sum (λ i, V i (w i)) (hV.linear_isometry_equiv.symm w) :=
+by simp [is_hilbert_sum.linear_isometry_equiv, orthogonal_family.has_sum_linear_isometry]
 
-/-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an `ι`-indexed orthogonal
-family `G`, an "elementary basis vector" in `lp G 2` supported at `i : ι` is the image of the
+/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
+`lp G 2`, an "elementary basis vector" in `lp G 2` supported at `i : ι` is the image of the
 associated element in `E`. -/
-@[simp] protected lemma linear_isometry_equiv_symm_apply_single [Π i, complete_space (G i)]
-  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) {i : ι} (x : G i) :
-  (hV.linear_isometry_equiv hV').symm (lp.single 2 i x) = V i x :=
-by simp [orthogonal_family.linear_isometry_equiv, orthogonal_family.linear_isometry_apply_single]
+@[simp] protected lemma is_hilbert_sum.linear_isometry_equiv_symm_apply_single
+  (hV : is_hilbert_sum 𝕜 E V) {i : ι} (x : G i) :
+  hV.linear_isometry_equiv.symm (lp.single 2 i x) = V i x :=
+by simp [is_hilbert_sum.linear_isometry_equiv, orthogonal_family.linear_isometry_apply_single]
 
-/-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an `ι`-indexed orthogonal
-family `G`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
+/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
+`lp G 2`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
 elements of `E`. -/
-@[simp] protected lemma linear_isometry_equiv_symm_apply_dfinsupp_sum_single
-  [Π i, complete_space (G i)]
-  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (W₀ : Π₀ (i : ι), G i) :
-  (hV.linear_isometry_equiv hV').symm (W₀.sum (lp.single 2)) = (W₀.sum (λ i, V i)) :=
-by simp [orthogonal_family.linear_isometry_equiv,
+@[simp] protected lemma is_hilbert_sum.linear_isometry_equiv_symm_apply_dfinsupp_sum_single
+  (hV : is_hilbert_sum 𝕜 E V) (W₀ : Π₀ (i : ι), G i) :
+  hV.linear_isometry_equiv.symm (W₀.sum (lp.single 2)) = (W₀.sum (λ i, V i)) :=
+by simp [is_hilbert_sum.linear_isometry_equiv,
   orthogonal_family.linear_isometry_apply_dfinsupp_sum_single]
 
-/-- In the canonical isometric isomorphism `E ≃ₗᵢ[𝕜] lp G 2` induced by an `ι`-indexed orthogonal
-family `G`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
+/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
+`lp G 2`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
 elements of `E`. -/
-@[simp] protected lemma linear_isometry_equiv_apply_dfinsupp_sum_single
-  [Π i, complete_space (G i)]
-  (hV' : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) (W₀ : Π₀ (i : ι), G i) :
-  (hV.linear_isometry_equiv hV' (W₀.sum (λ i, V i)) : Π i, G i) = W₀ :=
+@[simp] protected lemma is_hilbert_sum.linear_isometry_equiv_apply_dfinsupp_sum_single
+  (hV : is_hilbert_sum 𝕜 E V) (W₀ : Π₀ (i : ι), G i) :
+  (hV.linear_isometry_equiv (W₀.sum (λ i, V i)) : Π i, G i) = W₀ :=
 begin
-  rw ← hV.linear_isometry_equiv_symm_apply_dfinsupp_sum_single hV',
+  rw ← hV.linear_isometry_equiv_symm_apply_dfinsupp_sum_single,
   rw linear_isometry_equiv.apply_symm_apply,
   ext i,
   simp [dfinsupp.sum, lp.single_apply] {contextual := tt},
 end
 
-end orthogonal_family
+/-- Given a total orthonormal family `v : ι → E`, `E` is a Hilbert sum of `λ i : ι, 𝕜` relative to
+the family of linear isometries `λ i, λ k, k • v i`. -/
+lemma orthonormal.is_hilbert_sum {v : ι → E} (hv : orthonormal 𝕜 v)
+  (hsp : ⊤ ≤ (span 𝕜 (set.range v)).topological_closure) :
+  @is_hilbert_sum _ 𝕜 _ _ _ _ (λ i : ι, 𝕜) _
+    (λ i, linear_isometry.to_span_singleton 𝕜 E (hv.1 i)) :=
+is_hilbert_sum.mk hv.orthogonal_family
+begin
+  convert hsp,
+  simp [← linear_map.span_singleton_eq_range, ← submodule.span_Union],
+end
+
+end is_hilbert_sum
 
 /-! ### Hilbert bases -/
 
@@ -426,15 +478,11 @@ include hv cplt
 protected def mk (hsp : ⊤ ≤ (span 𝕜 (set.range v)).topological_closure) :
   hilbert_basis ι 𝕜 E :=
 hilbert_basis.of_repr $
-hv.orthogonal_family.linear_isometry_equiv
-begin
-  convert hsp,
-  simp [← linear_map.span_singleton_eq_range, ← submodule.span_Union],
-end
+(hv.is_hilbert_sum hsp).linear_isometry_equiv
 
 lemma _root_.orthonormal.linear_isometry_equiv_symm_apply_single_one (h i) :
-  (hv.orthogonal_family.linear_isometry_equiv h).symm (lp.single 2 i 1) = v i :=
-by rw [orthogonal_family.linear_isometry_equiv_symm_apply_single,
+  (hv.is_hilbert_sum h).linear_isometry_equiv.symm (lp.single 2 i 1) = v i :=
+by rw [is_hilbert_sum.linear_isometry_equiv_symm_apply_single,
   linear_isometry.to_span_singleton_apply, one_smul]
 
 @[simp] protected lemma coe_mk (hsp : ⊤ ≤ (span 𝕜 (set.range v)).topological_closure) :