feat(analysis/inner_product/pi_L2): a finite orthonormal family is a …

…basis of its span (#15481)

We actually prove this for finite sub-families of a generic orthonormal basis because this is easier to use in practice

src/analysis/inner_product_space/basic.lean

@@ -1207,14 +1207,18 @@ def linear_equiv.isometry_of_inner (f : E ≃ₗ[𝕜] E') (h : ∀ x y, ⟪f x,
   (f.isometry_of_inner h).to_linear_equiv = f := rfl
 
 /-- A linear isometry preserves the property of being orthonormal. -/
-lemma orthonormal.comp_linear_isometry {v : ι → E} (hv : orthonormal 𝕜 v) (f : E →ₗᵢ[𝕜] E') :
-  orthonormal 𝕜 (f ∘ v) :=
+lemma linear_isometry.orthonormal_comp_iff {v : ι → E} (f : E →ₗᵢ[𝕜] E') :
+  orthonormal 𝕜 (f ∘ v) ↔ orthonormal 𝕜 v :=
 begin
   classical,
-  simp_rw [orthonormal_iff_ite, linear_isometry.inner_map_map, ←orthonormal_iff_ite],
-  exact hv
+  simp_rw [orthonormal_iff_ite, linear_isometry.inner_map_map]
 end
 
+/-- A linear isometry preserves the property of being orthonormal. -/
+lemma orthonormal.comp_linear_isometry {v : ι → E} (hv : orthonormal 𝕜 v) (f : E →ₗᵢ[𝕜] E') :
+  orthonormal 𝕜 (f ∘ v) :=
+by rwa f.orthonormal_comp_iff
+
 /-- A linear isometric equivalence preserves the property of being orthonormal. -/
 lemma orthonormal.comp_linear_isometry_equiv {v : ι → E} (hv : orthonormal 𝕜 v) (f : E ≃ₗᵢ[𝕜] E') :
   orthonormal 𝕜 (f ∘ v) :=
@@ -1820,6 +1824,17 @@ 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
 
+lemma orthonormal.cod_restrict {ι : Type*} {v : ι → E} (hv : orthonormal 𝕜 v)
+  (s : submodule 𝕜 E) (hvs : ∀ i, v i ∈ s) :
+  @orthonormal 𝕜 s _ _ ι (set.cod_restrict v s hvs) :=
+s.subtypeₗᵢ.orthonormal_comp_iff.mp hv
+
+lemma orthonormal_span {ι : Type*} {v : ι → E} (hv : orthonormal 𝕜 v) :
+  @orthonormal 𝕜 (submodule.span 𝕜 (set.range v)) _ _ ι
+    (λ i : ι, ⟨v i, submodule.subset_span (set.mem_range_self i)⟩) :=
+hv.cod_restrict (submodule.span 𝕜 (set.range v))
+  (λ i, submodule.subset_span (set.mem_range_self i))
+
 /-! ### Families of mutually-orthogonal subspaces of an inner product space -/
 
 section orthogonal_family

src/analysis/inner_product_space/pi_L2.lean

@@ -50,7 +50,7 @@ For consequences in infinite dimension (Hilbert bases, etc.), see the file
 
 -/
 
-open real set filter is_R_or_C
+open real set filter is_R_or_C submodule
 open_locale big_operators uniformity topological_space nnreal ennreal complex_conjugate direct_sum
 
 noncomputable theory
@@ -338,6 +338,16 @@ begin
   refl,
 end
 
+/-- Mapping an orthonormal basis along a `linear_isometry_equiv`. -/
+protected def map {G : Type*} [inner_product_space 𝕜 G] (b : orthonormal_basis ι 𝕜 E)
+  (L : E ≃ₗᵢ[𝕜] G) :
+  orthonormal_basis ι 𝕜 G :=
+{ repr := L.symm.trans b.repr }
+
+@[simp] protected lemma map_apply {G : Type*} [inner_product_space 𝕜 G]
+  (b : orthonormal_basis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) (i : ι) :
+  b.map L i = L (b i) := rfl
+
 /-- A basis that is orthonormal is an orthonormal basis. -/
 def _root_.basis.to_orthonormal_basis (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) :
   orthonormal_basis ι 𝕜 E :=
@@ -385,6 +395,32 @@ protected lemma coe_mk (hon : orthonormal 𝕜 v) (hsp: submodule.span 𝕜 (set
   ⇑(orthonormal_basis.mk hon hsp) = v :=
 by classical; rw [orthonormal_basis.mk, _root_.basis.coe_to_orthonormal_basis, basis.coe_mk]
 
+/-- Any finite subset of a orthonormal family is an `orthonormal_basis` for its span. -/
+protected def span {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') :
+  orthonormal_basis s 𝕜 (span 𝕜 (s.image v' : set E)) :=
+let
+  e₀' : basis s 𝕜 _ := basis.span (h.linear_independent.comp (coe : s → ι') subtype.coe_injective),
+  e₀ : orthonormal_basis s 𝕜 _ := orthonormal_basis.mk
+    begin
+      convert orthonormal_span (h.comp (coe : s → ι') subtype.coe_injective),
+      ext,
+      simp [e₀', basis.span_apply],
+    end e₀'.span_eq,
+  φ : span 𝕜 (s.image v' : set E) ≃ₗᵢ[𝕜] span 𝕜 (range (v' ∘ (coe : s → ι'))) :=
+    linear_isometry_equiv.of_eq _ _
+    begin
+      rw [finset.coe_image, image_eq_range],
+      refl
+    end
+in
+e₀.map φ.symm
+
+@[simp] protected lemma span_apply {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') (i : s) :
+  (orthonormal_basis.span h s i : E) = v' i :=
+by simp only [orthonormal_basis.span, basis.span_apply, linear_isometry_equiv.of_eq_symm,
+              orthonormal_basis.map_apply, orthonormal_basis.coe_mk,
+              linear_isometry_equiv.coe_of_eq_apply]
+
 open submodule
 
 /-- A finite orthonormal family of vectors whose span has trivial orthogonal complement is an

src/linear_algebra/basis.lean

@@ -970,6 +970,9 @@ begin
   rwa h_x_eq_y
 end
 
+protected lemma span_apply (i : ι) : (basis.span hli i : M) = v i :=
+congr_arg (coe : span R (range v) → M) $ basis.mk_apply (linear_independent_span hli) _ i
+
 end span
 
 lemma group_smul_span_eq_top