[Merged by Bors] - feat(analysis/normed_space/inner_product): existence of orthonormal basis

src/algebra/group_power/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import algebra.ordered_ring
+import algebra.ordered_field
 import deprecated.group
 
 /-!
@@ -612,6 +612,19 @@ pow_bit0_pos h 1
 
 end linear_ordered_ring
 
+/- this lemma would work for `ordered_integral_domain`, if that typeclass existed -/
+@[simp] lemma eq_of_pow_two_eq_pow_two [linear_ordered_field R] {a b : R}
+  (ha : 0 ≤ a) (hb : 0 ≤ b) :
+  a ^ 2 = b ^ 2 ↔ a = b :=
+begin
+  refine ⟨_, congr_arg _⟩,
+  intros h,
+  refine (eq_or_eq_neg_of_pow_two_eq_pow_two _ _ h).elim id _,
+  rintros rfl,
+  rw le_antisymm (neg_nonneg.mp ha) hb,
+  exact neg_zero
+end
+
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]
 

src/analysis/normed_space/inner_product.lean

@@ -448,6 +448,17 @@ lemma inner_sum {ι : Type*} (s : finset ι) (f : ι → E) (x : E) :
   ⟪x, ∑ i in s, f i⟫ = ∑ i in s, ⟪x, f i⟫ :=
 sesq_form.map_sum_left (sesq_form_of_inner) _ _ _
 
+/-- An inner product with a sum on the left, `finsupp` version. -/
+lemma finsupp.sum_inner {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
+  ⟪l.sum (λ (i : ι) (a : 𝕜), a • v i), x⟫
+  = l.sum (λ (i : ι) (a : 𝕜), (is_R_or_C.conj a) • ⟪v i, x⟫) :=
+by { convert sum_inner l.support (λ a, l a • v a) x, simp [inner_smul_left, finsupp.sum] }
+
+/-- An inner product with a sum on the right, `finsupp` version. -/
+lemma finsupp.inner_sum {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
+  ⟪x, l.sum (λ (i : ι) (a : 𝕜), a • v i)⟫ = l.sum (λ (i : ι) (a : 𝕜), a • ⟪x, v i⟫) :=
+by { convert inner_sum l.support (λ a, l a • v a) x, simp [inner_smul_right, finsupp.sum] }
+
 @[simp] lemma inner_zero_left {x : E} : ⟪0, x⟫ = 0 :=
 by rw [← zero_smul 𝕜 (0:E), inner_smul_left, ring_hom.map_zero, zero_mul]
 
@@ -495,6 +506,13 @@ by { have h := @inner_self_nonpos ℝ F _ _ x, simpa using h }
 @[simp] lemma inner_self_re_to_K {x : E} : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
 by rw is_R_or_C.ext_iff; exact ⟨by simp, by simp [inner_self_nonneg_im]⟩
 
+lemma inner_self_eq_norm_sq_to_K (x : E) : ⟪x, x⟫ = (∥x∥ ^ 2 : 𝕜) :=
+begin
+  suffices : (is_R_or_C.re ⟪x, x⟫ : 𝕜) = ∥x∥ ^ 2,
+  { simpa [inner_self_re_to_K] using this },
+  exact_mod_cast (norm_sq_eq_inner x).symm
+end
+
 lemma inner_self_re_abs {x : E} : re ⟪x, x⟫ = abs ⟪x, x⟫ :=
 begin
   have H : ⟪x, x⟫ = (re ⟪x, x⟫ : 𝕜) + im ⟪x, x⟫ * I,
@@ -642,6 +660,66 @@ end
 
 end basic_properties
 
+section orthonormal_sets
+variables {ι : Type*} (𝕜)
+
+include 𝕜
+
+/-- An orthonormal set of vectors in an `inner_product_space` -/
+def orthonormal (v : ι → E) : Prop :=
+(∀ i, ∥v i∥ = 1) ∧ (∀ {i j}, i ≠ j → ⟪v i, v j⟫ = 0)
+
+omit 𝕜
+
+variables {𝕜}
+
+/-- `if ... then ... else` characterization of a set of vectors being orthonormal.  (Inner product
+equals Kronecker delta.) -/
+lemma orthonormal_iff_ite {v : ι → E} :
+  orthonormal 𝕜 v ↔ ∀ i j, ⟪v i, v j⟫ = if i = j then (1:𝕜) else (0:𝕜) :=
+begin
+  split,
+  { intros hv i j,
+    split_ifs,
+    { simp [h, inner_self_eq_norm_sq_to_K, hv.1] },
+    { exact hv.2 h } },
+  { intros h,
+    split,
+    { intros i,
+      have h' : ∥v i∥ ^ 2 = 1 ^ 2 := by simp [norm_sq_eq_inner, h i i],
+      have h₁ : 0 ≤ ∥v i∥ := norm_nonneg _,
+      have h₂ : (0:ℝ) ≤ 1 := by norm_num,
+      rwa eq_of_pow_two_eq_pow_two h₁ h₂ at h' },
+    { intros i j hij,
+      simpa [hij] using h i j } }
+end
+
+/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
+vectors picks out the coefficient of that vector. -/
+lemma inner_finsupp_orthonormal {v : ι → E} (he : orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
+  ⟪v i, finsupp.total ι E 𝕜 v l⟫ = l i :=
+by simp [finsupp.total_apply, finsupp.inner_sum, orthonormal_iff_ite.mp he]
+
+/-- An orthonormal set is linearly independent. -/
+lemma linear_independent_of_orthonormal {v : ι → E} (he : orthonormal 𝕜 v) :
+  linear_independent 𝕜 v :=
+begin
+  rw linear_independent_iff,
+  intros l hl,
+  ext i,
+  have key : ⟪v i, finsupp.total ι E 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw hl,
+  simpa [inner_finsupp_orthonormal he] using key
+end
+
+open finite_dimensional
+
+lemma is_basis_of_orthonormal_of_card_eq_findim [fintype ι] [nonempty ι] {v : ι → E}
+  (hv : orthonormal 𝕜 v) (card_eq : fintype.card ι = findim 𝕜 E) :
+  is_basis 𝕜 v :=
+is_basis_of_linear_independent_of_card_eq_findim (linear_independent_of_orthonormal hv) card_eq
+
+end orthonormal_sets
+
 section norm
 
 lemma norm_eq_sqrt_inner (x : E) : ∥x∥ = sqrt (re ⟪x, x⟫) :=
@@ -1170,6 +1248,21 @@ space use `euclidean_space 𝕜 (fin n)`. -/
 def euclidean_space (𝕜 : Type*) [is_R_or_C 𝕜]
   (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), 𝕜)
 
+/-! ### Inner product space structure on subspaces -/
+
+/-- Induced inner product on a submodule. -/
+instance submodule.inner_product_space (W : submodule 𝕜 E) : inner_product_space 𝕜 W :=
+{ inner             := λ x y, ⟪(x:E), (y:E)⟫,
+  conj_sym          := λ _ _, inner_conj_sym _ _ ,
+  nonneg_im         := λ _, inner_self_nonneg_im,
+  norm_sq_eq_inner  := λ _, norm_sq_eq_inner _,
+  add_left          := λ _ _ _ , inner_add_left,
+  smul_left         := λ _ _ _, inner_smul_left,
+  ..submodule.normed_space W }
+
+/-- 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
+
 section is_R_or_C_to_real
 
 variables {G : Type*}
@@ -1425,6 +1518,13 @@ instance : finite_dimensional 𝕜 (euclidean_space 𝕜 ι) := by apply_instanc
 lemma findim_euclidean_space_fin {n : ℕ} :
   finite_dimensional.findim 𝕜 (euclidean_space 𝕜 (fin n)) = n := by simp
 
+/-- A basis on `ι` for a finite-dimensional space induces a continuous linear equivalence 
+with `euclidean_space 𝕜 ι`.  If the basis is orthonormal in an inner product space, this continuous 
+linear equivalence is an isometry, but we don't prove that here. -/
+def is_basis.equiv_fun_euclidean [finite_dimensional 𝕜 E] {v : ι → E} (h : is_basis 𝕜 v) :
+  E ≃L[𝕜] (euclidean_space 𝕜 ι) :=
+h.equiv_fun.to_continuous_linear_equiv
+
 end pi_Lp
 
 
@@ -2216,3 +2316,75 @@ begin
   exact nat.add_sub_cancel' (nat.succ_le_iff.mpr findim_pos)
 end
 end orthogonal
+
+section orthonormal_basis
+
+/-! ### Existence of an orthonormal basis for a finite-dimensional inner product space -/
+
+variables (𝕜 E)
+
+open finite_dimensional
+
+/-- A finite-dimensional `inner_product_space` has an orthonormal set whose cardinality is the
+dimension. -/
+theorem exists_max_orthonormal [finite_dimensional 𝕜 E] :
+  ∃ (v : fin (findim 𝕜 E) → E), orthonormal 𝕜 v :=
+begin
+  tactic.unfreeze_local_instances,
+  -- prove this by induction on the dimension
+  induction hk : findim 𝕜 E with k IH generalizing E,
+  { -- base case trivial
+    use λ i, 0,
+    have h₀ : fin 0 → fin 0 → false := fin.elim0,
+    simpa [orthonormal_iff_ite] using h₀ },
+  -- in the inductive step, the `inner_product_space` must contain a nonzero vector
+  obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0,
+  { rw [← @findim_pos_iff_exists_ne_zero 𝕜, hk],
+    exact k.succ_pos },
+  -- normalize it
+  let e := (∥x∥⁻¹ : 𝕜) • x,
+  have he : ∥e∥ = 1 := by simp [e, norm_smul_inv_norm hx],
+  -- by the inductive hypothesis, find an orthonormal basis for its orthogonal complement
+  obtain ⟨w, hw₁, hw₂⟩ : ∃ w : fin k → (𝕜 ∙ e)ᗮ, orthonormal 𝕜 w,
+  { have he' : e ≠ 0,
+    { rw [← norm_pos_iff, he],
+      norm_num },
+    apply IH,
+    simp [findim_orthogonal_span_singleton he', hk] },
+  -- put these together to provide a candidate orthonormal basis `v` for the whole space
+  let v : fin (k + 1) → E := λ i, if h : i ≠ 0 then coe (w (i.pred h)) else e,
+  refine ⟨v, _, _⟩,
+  { -- show that the elements of `v` have unit length
+    intro i,
+    by_cases h : i = 0,
+    { simp [v, h, he] },
+    { simpa [v, h] using hw₁ (i.pred h) } },
+  { -- show that the elements of `v` are orthogonal
+    have h_end : ∀ (j : fin k.succ), 0 ≠ j → ⟪v 0, v j⟫ = 0,
+    { intros j hj,
+      suffices : ⟪e, w (j.pred hj.symm)⟫ = 0,
+      { simpa [v, hj.symm] using this },
+      apply inner_right_of_mem_orthogonal_singleton,
+      exact (w (j.pred hj.symm)).2 },
+    intro i,
+    by_cases hi : i = 0,
+    { rw hi,
+      exact h_end },
+    intros j inej,
+    by_cases hj : j = 0,
+    { rw [hj, inner_eq_zero_sym],
+      apply h_end _ (ne.symm hi) },
+    have : ⟪w (i.pred hi), w (j.pred hj)⟫ = 0 := by simp [inej, hw₂],
+    simpa [v, hi, hj] using this }
+end
+
+/-- A finite-dimensional `inner_product_space` has an orthonormal basis. -/
+lemma is_basis_max_orthonormal [nontrivial E] [finite_dimensional 𝕜 E] :
+  ∃ (v : fin (findim 𝕜 E) → E), orthonormal 𝕜 v ∧ is_basis 𝕜 v :=
+begin
+  let v := classical.some (exists_max_orthonormal 𝕜 E),
+  let hv := classical.some_spec (exists_max_orthonormal 𝕜 E),
+  exact ⟨v, hv, is_basis_of_orthonormal_of_card_eq_findim hv (by simp)⟩
+end
+
+end orthonormal_basis

src/data/complex/is_R_or_C.lean

@@ -750,3 +750,24 @@ by simp [is_R_or_C.abs, complex.abs]
 end cleanup_lemmas
 
 end is_R_or_C
+
+section normalization
+variables {K : Type*} [is_R_or_C K]
+variables {E : Type*} [normed_group E] [normed_space K E]
+
+open is_R_or_C
+
+/- Note: one might think the following lemma belongs in `analysis.normed_space.basic`.  But it
+can't be placed there, because that file is an import of `data.complex.is_R_or_C`! -/
+
+/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to unit length. -/
+@[simp] lemma norm_smul_inv_norm {x : E} (hx : x ≠ 0) : ∥(∥x∥⁻¹ : K) • x∥ = 1 :=
+begin
+  have h : ∥(∥x∥ : K)∥ = ∥x∥,
+  { rw norm_eq_abs,
+    exact abs_of_nonneg (norm_nonneg _) },
+  have : ∥x∥ ≠ 0 := by simp [hx],
+  field_simp [norm_smul, h]
+end
+
+end normalization

src/data/finsupp/basic.lean

@@ -595,12 +595,20 @@ lemma prod_ite_eq (f : α →₀ M) (a : α) (b : α → M → N) :
   f.prod (λ x v, ite (a = x) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 :=
 by { dsimp [finsupp.prod], rw f.support.prod_ite_eq, }
 
+@[simp] lemma sum_ite_self_eq {N : Type*} [add_comm_monoid N] (f : α →₀ N) (a : α) :
+  f.sum (λ x v, ite (a = x) v 0) = f a :=
+by { convert f.sum_ite_eq a (λ x, id), simp [ite_eq_right_iff.2 eq.symm] }
+
 /-- A restatement of `prod_ite_eq` with the equality test reversed. -/
 @[simp, to_additive "A restatement of `sum_ite_eq` with the equality test reversed."]
 lemma prod_ite_eq' (f : α →₀ M) (a : α) (b : α → M → N) :
   f.prod (λ x v, ite (x = a) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 :=
 by { dsimp [finsupp.prod], rw f.support.prod_ite_eq', }
 
+@[simp] lemma sum_ite_self_eq' {N : Type*} [add_comm_monoid N] (f : α →₀ N) (a : α) :
+  f.sum (λ x v, ite (x = a) v 0) = f a :=
+by { convert f.sum_ite_eq' a (λ x, id), simp [ite_eq_right_iff.2 eq.symm] }
+
 @[simp] lemma prod_pow [fintype α] (f : α →₀ ℕ) (g : α → N) :
   f.prod (λ a b, g a ^ b) = ∏ a, g a ^ (f a) :=
 f.prod_fintype _ $ λ a, pow_zero _

src/linear_algebra/finite_dimensional.lean

@@ -312,6 +312,17 @@ iff.trans (by { rw ← findim_eq_dim, norm_cast }) (@dim_pos_iff_nontrivial K V
 lemma findim_pos [finite_dimensional K V] [h : nontrivial V] : 0 < findim K V :=
 findim_pos_iff.mpr h
 
+/-- `has_zero` instance for `fin k` where `k` is the dimension of a nontrivial finite-dimensional
+vector space.  This is primarily useful so that `nonempty` can be deduced, by typeclass inference.
+-/
+noncomputable instance has_zero_findim [nontrivial V] [finite_dimensional K V] :
+  has_zero (fin (findim K V)) :=
+begin
+  cases h : findim K V,
+  exact false.elim (ne_of_gt findim_pos h),
+  apply_instance
+end
+
 section
 open_locale big_operators
 open finset