feat(analysis/inner_product_space): define orthogonal_family of sub…

…spaces (#9718)

Define `orthogonal_family` on `V : ι → submodule 𝕜 E` to mean that any two vectors from distinct subspaces are orthogonal.  Prove that an orthogonal family of subspaces is `complete_lattice.independent`.

Also prove that in finite dimension an orthogonal family `V` satisifies `direct_sum.submodule_is_internal` (i.e., it provides an internal direct sum decomposition of `E`) if and only if their joint orthogonal complement is trivial, `(supr V)ᗮ = ⊥`, and that in this case, the identification of `E` with the direct sum of `V` is an isometry.

src/analysis/inner_product_space/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis
 -/
+import algebra.direct_sum.module
 import analysis.complex.basic
 import analysis.normed_space.bounded_linear_maps
 import linear_algebra.bilinear_form
@@ -1486,6 +1487,80 @@ instance submodule.inner_product_space (W : submodule 𝕜 E) : inner_product_sp
 /-- The inner product on submodules is the same as on the ambient space. -/
 @[simp] lemma submodule.coe_inner (W : submodule 𝕜 E) (x y : W) : ⟪x, y⟫ = ⟪(x:E), ↑y⟫ := rfl
 
+/-! ### Families of mutually-orthogonal subspaces of an inner product space -/
+
+section orthogonal_family
+variables {ι : Type*} (𝕜)
+open_locale direct_sum
+
+/-- An indexed family of mutually-orthogonal subspaces of an inner product space `E`. -/
+def orthogonal_family (V : ι → submodule 𝕜 E) : Prop :=
+∀ ⦃i j⦄, i ≠ j → ∀ {v : E} (hv : v ∈ V i) {w : E} (hw : w ∈ V j), ⟪v, w⟫ = 0
+
+variables {𝕜} {V : ι → submodule 𝕜 E}
+
+lemma orthogonal_family.eq_ite (hV : orthogonal_family 𝕜 V) {i j : ι} (v : V i) (w : V j) :
+  ⟪(v:E), w⟫ = ite (i = j) ⟪(v:E), w⟫ 0 :=
+begin
+  split_ifs,
+  { refl },
+  { exact hV h v.prop w.prop }
+end
+
+lemma orthogonal_family.inner_right_dfinsupp (hV : orthogonal_family 𝕜 V)
+  (l : Π₀ i, V i) (i : ι) (v : V i) :
+  ⟪(v : E), dfinsupp.lsum ℕ (λ i, (V i).subtype) l⟫ = ⟪v, l i⟫ :=
+calc ⟪(v : E), dfinsupp.lsum ℕ (λ i, (V i).subtype) l⟫
+    = l.sum (λ j, λ w, ⟪(v:E), w⟫) :
+begin
+  let F : E →+ 𝕜 := (@inner_right 𝕜 E _ _ v).to_linear_map.to_add_monoid_hom,
+  have hF := congr_arg add_monoid_hom.to_fun
+    (dfinsupp.comp_sum_add_hom F (λ j, (V j).subtype.to_add_monoid_hom)),
+  convert congr_fun hF l using 1,
+  simp only [dfinsupp.sum_add_hom_apply, continuous_linear_map.to_linear_map_eq_coe,
+    add_monoid_hom.coe_comp, inner_right_coe, add_monoid_hom.to_fun_eq_coe,
+    linear_map.to_add_monoid_hom_coe, continuous_linear_map.coe_coe],
+  congr
+end
+... = l.sum (λ j, λ w, ite (i=j) ⟪(v:E), w⟫ 0) :
+  congr_arg l.sum $ funext $ λ j, funext $ hV.eq_ite v
+... = ⟪v, l i⟫ :
+begin
+  simp only [dfinsupp.sum, submodule.coe_inner, finset.sum_ite_eq, ite_eq_left_iff,
+    dfinsupp.mem_support_to_fun, not_not],
+  intros h,
+  simp [h]
+end
+
+lemma orthogonal_family.inner_right_fintype
+  [fintype ι] (hV : orthogonal_family 𝕜 V) (l : Π i, V i) (i : ι) (v : V i) :
+  ⟪(v : E), ∑ j : ι, l j⟫ = ⟪v, l i⟫ :=
+calc ⟪(v : E), ∑ j : ι, l j⟫
+    = ∑ j : ι, ⟪(v : E), l j⟫: by rw inner_sum
+... = ∑ j, ite (i = j) ⟪(v : E), l j⟫ 0 :
+  congr_arg (finset.sum finset.univ) $ funext $ λ j, (hV.eq_ite v (l j))
+... = ⟪v, l i⟫ : by simp
+
+/-- An orthogonal family forms an independent family of subspaces; that is, any collection of
+elements each from a different subspace in the family is linearly independent. In particular, the
+pairwise intersections of elements of the family are 0. -/
+lemma orthogonal_family.independent (hV : orthogonal_family 𝕜 V) :
+  complete_lattice.independent V :=
+begin
+  apply complete_lattice.independent_of_dfinsupp_lsum_injective,
+  rw [← @linear_map.ker_eq_bot _ _ _ _ _ _ (direct_sum.add_comm_group (λ i, V i)),
+    submodule.eq_bot_iff],
+  intros v hv,
+  rw linear_map.mem_ker at hv,
+  ext i,
+  have : ⟪(v i : E), dfinsupp.lsum ℕ (λ i, (V i).subtype) v⟫ = 0,
+  { simp [hv] },
+  simpa only [submodule.coe_zero, submodule.coe_eq_zero, direct_sum.zero_apply, inner_self_eq_zero,
+    hV.inner_right_dfinsupp] using this,
+end
+
+end orthogonal_family
+
 section is_R_or_C_to_real
 
 variables {G : Type*}

src/analysis/inner_product_space/pi_L2.lean

@@ -114,11 +114,31 @@ instance : inner_product_space 𝕜 (euclidean_space 𝕜 ι) := by apply_instan
 lemma finrank_euclidean_space_fin {n : ℕ} :
   finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 (fin n)) = n := by simp
 
+/-- A finite, mutually orthogonal family of subspaces of `E`, which span `E`, induce an isometry
+from `E` to `pi_Lp 2` of the subspaces equipped with the `L2` inner product. -/
+def direct_sum.submodule_is_internal.isometry_L2_of_orthogonal_family
+  [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.submodule_is_internal V)
+  (hV' : orthogonal_family 𝕜 V) :
+  E ≃ₗᵢ[𝕜] pi_Lp 2 one_le_two (λ i, V i) :=
+begin
+  let e₁ := direct_sum.linear_equiv_fun_on_fintype 𝕜 ι (λ i, V i),
+  let e₂ := linear_equiv.of_bijective _ hV.injective hV.surjective,
+  refine (e₂.symm.trans e₁).isometry_of_inner _,
+  suffices : ∀ v w, ⟪v, w⟫ = ⟪e₂ (e₁.symm v), e₂ (e₁.symm w)⟫,
+  { intros v₀ w₀,
+    convert this (e₁ (e₂.symm v₀)) (e₁ (e₂.symm w₀));
+    simp only [linear_equiv.symm_apply_apply, linear_equiv.apply_symm_apply] },
+  intros v w,
+  transitivity ⟪(∑ i, (v i : E)), ∑ i, (w i : E)⟫,
+  { simp [sum_inner, hV'.inner_right_fintype] },
+  { congr; simp }
+end
+
 /-- An orthonormal basis on a fintype `ι` for an inner product space induces an isometry with
 `euclidean_space 𝕜 ι`. -/
 def basis.isometry_euclidean_of_orthonormal
   (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) :
-  E ≃ₗᵢ[𝕜] (euclidean_space 𝕜 ι) :=
+  E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι :=
 v.equiv_fun.isometry_of_inner
 begin
   intros x y,

src/analysis/inner_product_space/projection.lean

@@ -862,6 +862,19 @@ submodule.finrank_add_finrank_orthogonal' $ by simp [finrank_span_singleton hv,
 
 end orthogonal
 
+section orthogonal_family
+variables {ι : Type*}
+
+/-- An orthogonal family of subspaces of `E` satisfies `direct_sum.submodule_is_internal` (that is,
+they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
+orthogonal complement. -/
+lemma orthogonal_family.submodule_is_internal_iff [finite_dimensional 𝕜 E]
+  {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 V) :
+  direct_sum.submodule_is_internal V ↔ (supr V)ᗮ = ⊥ :=
+by simp only [direct_sum.submodule_is_internal_iff_independent_and_supr_eq_top, hV.independent,
+  true_and, submodule.orthogonal_eq_bot_iff (supr V).complete_of_finite_dimensional]
+
+end orthogonal_family
 
 section orthonormal_basis