feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an orthogonal_family (#10208)

In a finite-dimensional inner product space of `E`, there exists an orthonormal basis subordinate to a given direct sum decomposition into an `orthogonal_family` of subspaces `E`.

Author: hrmacbeth

src/algebra/direct_sum/module.lean

@@ -236,6 +236,35 @@ lemma submodule_is_internal.independent (h : submodule_is_internal A) :
   complete_lattice.independent A :=
 complete_lattice.independent_of_dfinsupp_lsum_injective _ h.injective
 
+/-- Given an internal direct sum decomposition of a module `M`, and a basis for each of the
+components of the direct sum, the disjoint union of these bases is a basis for `M`. -/
+noncomputable def submodule_is_internal.collected_basis
+  (h : submodule_is_internal A) {α : ι → Type*} (v : Π i, basis (α i) R (A i)) :
+  basis (Σ i, α i) R M :=
+{ repr := (linear_equiv.of_bijective _ h.injective h.surjective).symm ≪≫ₗ
+      (dfinsupp.map_range.linear_equiv (λ i, (v i).repr)) ≪≫ₗ
+      (sigma_finsupp_lequiv_dfinsupp R).symm }
+
+@[simp] lemma submodule_is_internal.collected_basis_coe
+  (h : submodule_is_internal A) {α : ι → Type*} (v : Π i, basis (α i) R (A i)) :
+  ⇑(h.collected_basis v) = λ a : Σ i, (α i), ↑(v a.1 a.2) :=
+begin
+  funext a,
+  simp only [submodule_is_internal.collected_basis, to_module, submodule_coe,
+    add_equiv.to_fun_eq_coe, basis.coe_of_repr, basis.repr_symm_apply, dfinsupp.lsum_apply_apply,
+    dfinsupp.map_range.linear_equiv_apply, dfinsupp.map_range.linear_equiv_symm,
+    dfinsupp.map_range_single, finsupp.total_single, linear_equiv.of_bijective_apply,
+    linear_equiv.symm_symm, linear_equiv.symm_trans_apply, one_smul,
+    sigma_finsupp_add_equiv_dfinsupp_apply, sigma_finsupp_equiv_dfinsupp_single,
+    sigma_finsupp_lequiv_dfinsupp_apply],
+  convert dfinsupp.sum_add_hom_single (λ i, (A i).subtype.to_add_monoid_hom) a.1 (v a.1 a.2),
+end
+
+lemma submodule_is_internal.collected_basis_mem
+  (h : submodule_is_internal A) {α : ι → Type*} (v : Π i, basis (α i) R (A i)) (a : Σ i, α i) :
+  h.collected_basis v a ∈ A a.1 :=
+by simp
+
 end semiring
 
 section ring

src/analysis/inner_product_space/basic.lean

@@ -1494,7 +1494,7 @@ instance submodule.inner_product_space (W : submodule 𝕜 E) : inner_product_sp
 /-! ### Families of mutually-orthogonal subspaces of an inner product space -/
 
 section orthogonal_family
-variables {ι : Type*} (𝕜)
+variables {ι : Type*} [dec_ι : decidable_eq ι] (𝕜)
 open_locale direct_sum
 
 /-- An indexed family of mutually-orthogonal subspaces of an inner product space `E`. -/
@@ -1503,6 +1503,7 @@ def orthogonal_family (V : ι → submodule 𝕜 E) : Prop :=
 
 variables {𝕜} {V : ι → submodule 𝕜 E}
 
+include dec_ι
 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
@@ -1535,6 +1536,7 @@ begin
   intros h,
   simp [h]
 end
+omit dec_ι
 
 lemma orthogonal_family.inner_right_fintype
   [fintype ι] (hV : orthogonal_family 𝕜 V) (l : Π i, V i) (i : ι) (v : V i) :
@@ -1570,6 +1572,29 @@ lemma orthogonal_family.comp (hV : orthogonal_family 𝕜 V) {γ : Type*} {f : 
   orthogonal_family 𝕜 (V ∘ f) :=
 λ i j hij v hv w hw, hV (hf.ne hij) hv hw
 
+lemma orthogonal_family.orthonormal_sigma_orthonormal (hV : orthogonal_family 𝕜 V) {α : ι → Type*}
+  {v_family : Π i, (α i) → V i} (hv_family : ∀ i, orthonormal 𝕜 (v_family i)) :
+  orthonormal 𝕜 (λ a : Σ i, α i, (v_family a.1 a.2 : E)) :=
+begin
+  split,
+  { rintros ⟨i, vi⟩,
+    exact (hv_family i).1 vi },
+  rintros ⟨i, vi⟩ ⟨j, vj⟩ hvij,
+  by_cases hij : i = j,
+  { subst hij,
+    have : vi ≠ vj := by simpa using hvij,
+    exact (hv_family i).2 this },
+  { exact hV hij (v_family i vi : V i).prop (v_family j vj : V j).prop }
+end
+
+include dec_ι
+lemma direct_sum.submodule_is_internal.collected_basis_orthonormal (hV : orthogonal_family 𝕜 V)
+  (hV_sum : direct_sum.submodule_is_internal V) {α : ι → Type*}
+  {v_family : Π i, basis (α i) 𝕜 (V i)} (hv_family : ∀ i, orthonormal 𝕜 (v_family i)) :
+  orthonormal 𝕜 (hV_sum.collected_basis v_family) :=
+by simpa using hV.orthonormal_sigma_orthonormal hv_family
+omit dec_ι
+
 end orthogonal_family
 
 section is_R_or_C_to_real

src/analysis/inner_product_space/projection.lean

@@ -974,10 +974,14 @@ let ⟨u, hus, hu, hu_max⟩ := exists_subset_is_orthonormal_dense_span (orthono
 ⟨u, hu, hu_max⟩
 variables {𝕜 E}
 
+section finite_dimensional
+
+variables [finite_dimensional 𝕜 E]
+
 /-- An orthonormal set in a finite-dimensional `inner_product_space` is maximal, if and only if it
 is a basis. -/
 lemma maximal_orthonormal_iff_basis_of_finite_dimensional
-  [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 (coe : v → E)) :
+  (hv : orthonormal 𝕜 (coe : v → E)) :
   (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ ∃ b : basis v 𝕜 E, ⇑b = coe :=
 begin
   rw maximal_orthonormal_iff_orthogonal_complement_eq_bot hv,
@@ -994,7 +998,7 @@ end
 /-- In a finite-dimensional `inner_product_space`, any orthonormal subset can be extended to an
 orthonormal basis. -/
 lemma exists_subset_is_orthonormal_basis
-  [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 (coe : v → E)) :
+  (hv : orthonormal 𝕜 (coe : v → E)) :
   ∃ (u ⊇ v) (b : basis u 𝕜 E), orthonormal 𝕜 b ∧ ⇑b = coe :=
 begin
   obtain ⟨u, hus, hu, hu_max⟩ := exists_maximal_orthonormal hv,
@@ -1005,39 +1009,89 @@ end
 variables (𝕜 E)
 
 /-- Index for an arbitrary orthonormal basis on a finite-dimensional `inner_product_space`. -/
-def orthonormal_basis_index [finite_dimensional 𝕜 E] : set E :=
+def orthonormal_basis_index : set E :=
 classical.some (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E))
 
 /-- A finite-dimensional `inner_product_space` has an orthonormal basis. -/
-def orthonormal_basis [finite_dimensional 𝕜 E] :
+def orthonormal_basis :
   basis (orthonormal_basis_index 𝕜 E) 𝕜 E :=
 (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some
 
-lemma orthonormal_basis_orthonormal [finite_dimensional 𝕜 E] :
+lemma orthonormal_basis_orthonormal :
   orthonormal 𝕜 (orthonormal_basis 𝕜 E) :=
 (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.1
 
-@[simp] lemma coe_orthonormal_basis [finite_dimensional 𝕜 E] :
+@[simp] lemma coe_orthonormal_basis :
   ⇑(orthonormal_basis 𝕜 E) = coe :=
 (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.2
 
-instance [finite_dimensional 𝕜 E] : fintype (orthonormal_basis_index 𝕜 E) :=
+instance : fintype (orthonormal_basis_index 𝕜 E) :=
 @is_noetherian.fintype_basis_index _ _ _ _ _ _ _
   (is_noetherian.iff_fg.2 infer_instance) (orthonormal_basis 𝕜 E)
 
 variables {𝕜 E}
 
 /-- An `n`-dimensional `inner_product_space` has an orthonormal basis indexed by `fin n`. -/
-def fin_orthonormal_basis [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
+def fin_orthonormal_basis {n : ℕ} (hn : finrank 𝕜 E = n) :
   basis (fin n) 𝕜 E :=
 have h : fintype.card (orthonormal_basis_index 𝕜 E) = n,
 by rw [← finrank_eq_card_basis (orthonormal_basis 𝕜 E), hn],
 (orthonormal_basis 𝕜 E).reindex (fintype.equiv_fin_of_card_eq h)
 
-lemma fin_orthonormal_basis_orthonormal [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
+lemma fin_orthonormal_basis_orthonormal {n : ℕ} (hn : finrank 𝕜 E = n) :
   orthonormal 𝕜 (fin_orthonormal_basis hn) :=
 suffices orthonormal 𝕜 (orthonormal_basis _ _ ∘ equiv.symm _),
 by { simp only [fin_orthonormal_basis, basis.coe_reindex], assumption }, -- why doesn't simpa work?
 (orthonormal_basis_orthonormal 𝕜 E).comp _ (equiv.injective _)
 
+section subordinate_orthonormal_basis
+open direct_sum
+variables {n : ℕ} (hn : finrank 𝕜 E = n) {ι : Type*} [fintype ι] [decidable_eq ι]
+  {V : ι → submodule 𝕜 E} (hV : submodule_is_internal V)
+
+/-- Exhibit a bijection between `fin n` and the index set of a certain basis of an `n`-dimensional
+inner product space `E`.  This should not be accessed directly, but only via the subsequent API. -/
+@[irreducible] def direct_sum.submodule_is_internal.sigma_orthonormal_basis_index_equiv :
+  (Σ i, orthonormal_basis_index 𝕜 (V i)) ≃ fin n :=
+let b := hV.collected_basis (λ i, orthonormal_basis 𝕜 (V i)) in
+fintype.equiv_fin_of_card_eq $ (finite_dimensional.finrank_eq_card_basis b).symm.trans hn
+
+/-- An `n`-dimensional `inner_product_space` equipped with a decomposition as an internal direct
+sum has an orthonormal basis indexed by `fin n` and subordinate to that direct sum. -/
+@[irreducible] def direct_sum.submodule_is_internal.subordinate_orthonormal_basis :
+  basis (fin n) 𝕜 E :=
+(hV.collected_basis (λ i, orthonormal_basis 𝕜 (V i))).reindex
+  (hV.sigma_orthonormal_basis_index_equiv hn)
+
+/-- An `n`-dimensional `inner_product_space` equipped with a decomposition as an internal direct
+sum has an orthonormal basis indexed by `fin n` and subordinate to that direct sum. This function
+provides the mapping by which it is subordinate. -/
+def direct_sum.submodule_is_internal.subordinate_orthonormal_basis_index (a : fin n) : ι :=
+((hV.sigma_orthonormal_basis_index_equiv hn).symm a).1
+
+/-- The basis constructed in `orthogonal_family.subordinate_orthonormal_basis` is orthonormal. -/
+lemma direct_sum.submodule_is_internal.subordinate_orthonormal_basis_orthonormal
+  (hV' : orthogonal_family 𝕜 V) :
+  orthonormal 𝕜 (hV.subordinate_orthonormal_basis hn) :=
+begin
+  simp only [direct_sum.submodule_is_internal.subordinate_orthonormal_basis, basis.coe_reindex],
+  have : orthonormal 𝕜 (hV.collected_basis (λ i, orthonormal_basis 𝕜 (V i))) :=
+    hV.collected_basis_orthonormal hV' (λ i, orthonormal_basis_orthonormal 𝕜 (V i)),
+  exact this.comp _ (equiv.injective _),
+end
+
+/-- The basis constructed in `orthogonal_family.subordinate_orthonormal_basis` is subordinate to
+the `orthogonal_family` in question. -/
+lemma direct_sum.submodule_is_internal.subordinate_orthonormal_basis_subordinate (a : fin n) :
+  hV.subordinate_orthonormal_basis hn a ∈ V (hV.subordinate_orthonormal_basis_index hn a) :=
+by simpa only [direct_sum.submodule_is_internal.subordinate_orthonormal_basis, basis.coe_reindex]
+  using hV.collected_basis_mem (λ i, orthonormal_basis 𝕜 (V i))
+    ((hV.sigma_orthonormal_basis_index_equiv hn).symm a)
+
+attribute [irreducible] direct_sum.submodule_is_internal.subordinate_orthonormal_basis_index
+
+end subordinate_orthonormal_basis
+
+end finite_dimensional
+
 end orthonormal_basis

src/data/finsupp/to_dfinsupp.lean

@@ -238,6 +238,21 @@ begin
   exact (finsupp.mem_split_support_iff_nonzero _ _).symm,
 end
 
+@[simp] lemma sigma_finsupp_equiv_dfinsupp_single [has_zero N] (a : Σ i, η i) (n : N) :
+  sigma_finsupp_equiv_dfinsupp (finsupp.single a n)
+    = @dfinsupp.single _ (λ i, η i →₀ N) _ _ a.1 (finsupp.single a.2 n) :=
+begin
+  obtain ⟨i, a⟩ := a,
+  ext j b,
+  by_cases h : i = j,
+  { subst h,
+    simp [split_apply, finsupp.single_apply] },
+  suffices : finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0,
+  { simp [split_apply, dif_neg h, this] },
+  have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h],
+  rw [finsupp.single_apply, if_neg H]
+end
+
 -- Without this Lean fails to find the `add_zero_class` instance on `Π₀ i, (η i →₀ N)`.
 local attribute [-instance] finsupp.has_zero