chore(analysis/inner_product_space/basic): golf, add/merge lemmas (#1…

…8928)

- Merge `inner_product_space.of_core.inner_self_nonneg_im` and `inner_product_space.of_core.inner_self_im_zero` into `inner_product_space.of_core.inner_self_im`.
- Rename `inner_product_space.of_core.inner_abs_conj_symm` to `inner_product_space.of_core.abs_inner_symm`.
- Rename `inner_abs_conj_symm` to `abs_inner_symm`.
- Add `inner_product_space.of_core.norm_sq_eq_zero`.
- Merge `inner_self_nonneg_im` and `inner_self_im_zero` into `inner_self_im`.
- Reorder, golf.

src/analysis/inner_product_space/basic.lean

@@ -162,12 +162,9 @@ lemma inner_conj_symm (x y : F) : ⟪y, x⟫† = ⟪x, y⟫ := c.conj_symm x y
 
 lemma inner_self_nonneg {x : F} : 0 ≤ re ⟪x, x⟫ := c.nonneg_re _
 
-lemma inner_self_nonneg_im (x : F) : im ⟪x, x⟫ = 0 :=
+lemma inner_self_im (x : F) : im ⟪x, x⟫ = 0 :=
 by rw [← @of_real_inj 𝕜, im_eq_conj_sub]; simp [inner_conj_symm]
 
-lemma inner_self_im_zero (x : F) : im ⟪x, x⟫ = 0 :=
-inner_self_nonneg_im _
-
 lemma inner_add_left (x y z : F) : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ :=
 c.add_left _ _ _
 
@@ -177,7 +174,7 @@ by rw [←inner_conj_symm, inner_add_left, ring_hom.map_add]; simp only [inner_c
 lemma inner_norm_sq_eq_inner_self (x : F) : (norm_sqF x : 𝕜) = ⟪x, x⟫ :=
 begin
   rw ext_iff,
-  exact ⟨by simp only [of_real_re]; refl, by simp only [inner_self_nonneg_im, of_real_im]⟩
+  exact ⟨by simp only [of_real_re]; refl, by simp only [inner_self_im, of_real_im]⟩
 end
 
 lemma inner_re_symm (x y : F) : re ⟪x, y⟫ = re ⟪y, x⟫ :=
@@ -199,15 +196,19 @@ lemma inner_zero_right (x : F) : ⟪x, 0⟫ = 0 :=
 by rw [←inner_conj_symm, inner_zero_left]; simp only [ring_hom.map_zero]
 
 lemma inner_self_eq_zero {x : F} : ⟪x, x⟫ = 0 ↔ x = 0 :=
-iff.intro (c.definite _) (by { rintro rfl, exact inner_zero_left _ })
+⟨c.definite _, by { rintro rfl, exact inner_zero_left _ }⟩
+
+lemma norm_sq_eq_zero {x : F} : norm_sqF x = 0 ↔ x = 0 :=
+iff.trans (by simp only [norm_sq, ext_iff, map_zero, inner_self_im, eq_self_iff_true, and_true])
+  (@inner_self_eq_zero 𝕜 _ _ _ _ _ x)
 
 lemma inner_self_ne_zero {x : F} : ⟪x, x⟫ ≠ 0 ↔ x ≠ 0 :=
 inner_self_eq_zero.not
 
 lemma inner_self_re_to_K (x : F) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
-by norm_num [ext_iff, inner_self_nonneg_im]
+by norm_num [ext_iff, inner_self_im]
 
-lemma inner_abs_conj_symm (x y : F) : abs ⟪x, y⟫ = abs ⟪y, x⟫ :=
+lemma abs_inner_symm (x y : F) : abs ⟪x, y⟫ = abs ⟪y, x⟫ :=
 by rw [←inner_conj_symm, abs_conj]
 
 lemma inner_neg_left (x y : F) : ⟪-x, y⟫ = -⟪x, y⟫ :=
@@ -259,7 +260,7 @@ begin
       apply hy',
       rw ext_iff,
       exact ⟨by simp only [H, zero_re'],
-             by simp only [inner_self_nonneg_im, add_monoid_hom.map_zero]⟩ },
+             by simp only [inner_self_im, add_monoid_hom.map_zero]⟩ },
     have h₆ : re ⟪y, y⟫ ≠ 0 := ne_of_gt h₅,
     have hmain := calc
       0   ≤ re ⟪x - T • y, x - T • y⟫
@@ -311,7 +312,7 @@ begin
   rw H,
   conv
   begin
-    to_lhs, congr, rw [inner_abs_conj_symm],
+    to_lhs, congr, rw [abs_inner_symm],
   end,
   exact inner_mul_inner_self_le y x,
 end
@@ -332,11 +333,7 @@ add_group_norm.to_normed_add_comm_group
       linarith },
     exact nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this,
   end,
-  eq_zero_of_map_eq_zero' := λ x hx, (inner_self_eq_zero : ⟪x, x⟫ = 0 ↔ x = 0).1 $ begin
-    change sqrt (re ⟪x, x⟫) = 0 at hx,
-    rw [sqrt_eq_zero inner_self_nonneg] at hx,
-    exact ext (by simp [hx]) (by simp [inner_self_im_zero]),
-  end }
+  eq_zero_of_map_eq_zero' := λ x hx, norm_sq_eq_zero.1 $ (sqrt_eq_zero inner_self_nonneg).1 hx }
 
 local attribute [instance] to_normed_add_comm_group
 
@@ -395,11 +392,9 @@ lemma real_inner_comm (x y : F) : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := @inner_conj
 lemma inner_eq_zero_symm {x y : E} : ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0 :=
 ⟨λ h, by simp [←inner_conj_symm, h], λ h, by simp [←inner_conj_symm, h]⟩
 
-@[simp] lemma inner_self_nonneg_im (x : E) : im ⟪x, x⟫ = 0 :=
+@[simp] lemma inner_self_im (x : E) : im ⟪x, x⟫ = 0 :=
 by rw [← @of_real_inj 𝕜, im_eq_conj_sub]; simp
 
-lemma inner_self_im_zero (x : E) : im ⟪x, x⟫ = 0 := inner_self_nonneg_im _
-
 lemma inner_add_left (x y z : E) : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ :=
 inner_product_space.add_left _ _ _
 
@@ -497,47 +492,11 @@ lemma inner_self_nonneg {x : E} : 0 ≤ re ⟪x, x⟫ :=
 by rw [←norm_sq_eq_inner]; exact pow_nonneg (norm_nonneg x) 2
 lemma real_inner_self_nonneg {x : F} : 0 ≤ ⟪x, x⟫_ℝ := @inner_self_nonneg ℝ F _ _ _ x
 
-@[simp] lemma inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0 :=
-begin
-  split,
-  { intro h,
-    have h₁ : re ⟪x, x⟫ = 0 :=
-    by rw is_R_or_C.ext_iff at h; simp only [h.1, zero_re'],
-    rw [←norm_sq_eq_inner x] at h₁,
-    rw [←norm_eq_zero],
-    exact pow_eq_zero h₁ },
-  { rintro rfl,
-    exact inner_zero_left _ }
-end
-
-lemma inner_self_ne_zero {x : E} : ⟪x, x⟫ ≠ 0 ↔ x ≠ 0 :=
-inner_self_eq_zero.not
-
-@[simp] lemma inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 :=
-begin
-  split,
-  { intro h,
-    rw ←@inner_self_eq_zero 𝕜,
-    have H₁ : re ⟪x, x⟫ ≥ 0, exact inner_self_nonneg,
-    have H₂ : re ⟪x, x⟫ = 0, exact le_antisymm h H₁,
-    rw is_R_or_C.ext_iff,
-    exact ⟨by simp [H₂], by simp [inner_self_nonneg_im]⟩ },
-  { rintro rfl,
-    simp only [inner_zero_left, add_monoid_hom.map_zero] }
-end
-
-lemma real_inner_self_nonpos {x : F} : ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0 :=
-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⟫ :=
-is_R_or_C.ext_iff.2 ⟨by simp only [of_real_re], by simp only [inner_self_nonneg_im, of_real_im]⟩
+is_R_or_C.ext_iff.2 ⟨by simp only [of_real_re], by simp only [inner_self_im, of_real_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 only [inner_self_re_to_K] using this },
-  exact_mod_cast (norm_sq_eq_inner x).symm
-end
+by rw [← inner_self_re_to_K, ← norm_sq_eq_inner, of_real_pow]
 
 lemma inner_self_re_abs (x : E) : re ⟪x, x⟫ = abs ⟪x, x⟫ :=
 begin
@@ -549,10 +508,22 @@ end
 lemma inner_self_abs_to_K (x : E) : (absK ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
 by { rw [←inner_self_re_abs], exact inner_self_re_to_K _ }
 
+@[simp] lemma inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0 :=
+by rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, of_real_eq_zero, norm_eq_zero]
+
+lemma inner_self_ne_zero {x : E} : ⟪x, x⟫ ≠ 0 ↔ x ≠ 0 :=
+inner_self_eq_zero.not
+
+@[simp] lemma inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 :=
+by rw [← norm_sq_eq_inner, (sq_nonneg _).le_iff_eq, sq_eq_zero_iff, norm_eq_zero]
+
+lemma real_inner_self_nonpos {x : F} : ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0 :=
+@inner_self_nonpos ℝ F _ _ _ x
+
 lemma real_inner_self_abs (x : F) : absR ⟪x, x⟫_ℝ = ⟪x, x⟫_ℝ :=
 by { have h := @inner_self_abs_to_K ℝ F _ _ _ x, simpa using h }
 
-lemma inner_abs_conj_symm (x y : E) : abs ⟪x, y⟫ = abs ⟪y, x⟫ :=
+lemma abs_inner_symm (x y : E) : abs ⟪x, y⟫ = abs ⟪y, x⟫ :=
 by rw [←inner_conj_symm, abs_conj]
 
 @[simp] lemma inner_neg_left (x y : E) : ⟪-x, y⟫ = -⟪x, y⟫ :=
@@ -564,7 +535,7 @@ by rw [←inner_conj_symm, inner_neg_left]; simp only [ring_hom.map_neg, inner_c
 lemma inner_neg_neg (x y : E) : ⟪-x, -y⟫ = ⟪x, y⟫ := by simp
 
 @[simp] lemma inner_self_conj (x : E) : ⟪x, x⟫† = ⟪x, x⟫ :=
-by rw [is_R_or_C.ext_iff]; exact ⟨by rw [conj_re], by rw [conj_im, inner_self_im_zero, neg_zero]⟩
+by rw [is_R_or_C.ext_iff]; exact ⟨by rw [conj_re], by rw [conj_im, inner_self_im, neg_zero]⟩
 
 lemma inner_sub_left (x y z : E) : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫ :=
 by { simp [sub_eq_add_neg, inner_add_left] }
@@ -637,7 +608,7 @@ begin
       apply hy',
       rw is_R_or_C.ext_iff,
       exact ⟨by simp only [H, zero_re'],
-             by simp only [inner_self_nonneg_im, add_monoid_hom.map_zero]⟩ },
+             by simp only [inner_self_im, add_monoid_hom.map_zero]⟩ },
     have h₆ : re ⟪y, y⟫ ≠ 0 := ne_of_gt h₅,
     have hmain := calc
       0   ≤ re ⟪x - T • y, x - T • y⟫
@@ -668,14 +639,9 @@ end
 
 /-- Cauchy–Schwarz inequality for real inner products. -/
 lemma real_inner_mul_inner_self_le (x y : F) : ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ :=
-begin
-  have h₁ : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [←inner_conj_symm]; refl,
-  have h₂ := @inner_mul_inner_self_le ℝ F _ _ _ x y,
-  dsimp at h₂,
-  have h₃ := abs_mul_abs_self ⟪x, y⟫_ℝ,
-  rw [h₁] at h₂,
-  simpa [h₃] using h₂,
-end
+calc ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ is_R_or_C.abs ⟪x, y⟫_ℝ * is_R_or_C.abs ⟪y, x⟫_ℝ :
+  by { rw [real_inner_comm y, ← is_R_or_C.abs_mul, ← is_R_or_C.norm_eq_abs], exact le_abs_self _ }
+... ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ : @inner_mul_inner_self_le ℝ _ _ _ _ x y
 
 /-- A family of vectors is linearly independent if they are nonzero
 and orthogonal. -/
@@ -1004,17 +970,8 @@ by { have h := @norm_add_mul_self ℝ _ _ _ _ x y, simpa using h }
 
 /-- Expand the square -/
 lemma norm_sub_sq (x y : E) : ‖x - y‖^2 = ‖x‖^2 - 2 * (re ⟪x, y⟫) + ‖y‖^2 :=
-begin
-  repeat {rw [sq, ←@inner_self_eq_norm_mul_norm 𝕜]},
-  rw [inner_sub_sub_self],
-  calc
-    re (⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫)
-        = re ⟪x, x⟫ - re ⟪x, y⟫ - re ⟪y, x⟫ + re ⟪y, y⟫  : by simp only [map_add, map_sub]
-    ... = -re ⟪y, x⟫ - re ⟪x, y⟫ + re ⟪x, x⟫ + re ⟪y, y⟫  : by ring
-    ... = -re (⟪x, y⟫†) - re ⟪x, y⟫ + re ⟪x, x⟫ + re ⟪y, y⟫ : by rw [inner_conj_symm]
-    ... = -re ⟪x, y⟫ - re ⟪x, y⟫ + re ⟪x, x⟫ + re ⟪y, y⟫ : by rw [conj_re]
-    ... = re ⟪x, x⟫ - 2*re ⟪x, y⟫ + re ⟪y, y⟫ : by ring
-end
+by rw [sub_eq_add_neg, @norm_add_sq 𝕜 _ _ _ _ x (-y), norm_neg, inner_neg_right, map_neg, mul_neg,
+  sub_eq_add_neg]
 
 alias norm_sub_sq ← norm_sub_pow_two
 
@@ -1039,7 +996,7 @@ begin
   have : ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) = (re ⟪x, x⟫) * (re ⟪y, y⟫),
     simp only [inner_self_eq_norm_mul_norm], ring,
   rw this,
-  conv_lhs { congr, skip, rw [inner_abs_conj_symm] },
+  conv_lhs { congr, skip, rw [abs_inner_symm] },
   exact inner_mul_inner_self_le _ _
 end
 
@@ -1428,15 +1385,8 @@ end
 norms, has absolute value at most 1. -/
 lemma abs_real_inner_div_norm_mul_norm_le_one (x y : F) : absR (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)) ≤ 1 :=
 begin
-  rw _root_.abs_div,
-  by_cases h : 0 = absR (‖x‖ * ‖y‖),
-  { rw [←h, div_zero],
-    norm_num },
-  { change 0 ≠ absR (‖x‖ * ‖y‖) at h,
-    rw div_le_iff' (lt_of_le_of_ne (ge_iff_le.mp (_root_.abs_nonneg (‖x‖ * ‖y‖))) h),
-    convert abs_real_inner_le_norm x y using 1,
-    rw [_root_.abs_mul, _root_.abs_of_nonneg (norm_nonneg x), _root_.abs_of_nonneg (norm_nonneg y),
-        mul_one] }
+  rw [_root_.abs_div, _root_.abs_mul, abs_norm, abs_norm],
+  exact div_le_one_of_le (abs_real_inner_le_norm x y) (by positivity)
 end
 
 /-- The inner product of a vector with a multiple of itself. -/
@@ -1604,23 +1554,10 @@ a negative multiple of the other. -/
 lemma real_inner_div_norm_mul_norm_eq_neg_one_iff (x y : F) :
   ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r < 0 ∧ y = r • x) :=
 begin
-  split,
-  { intro h,
-    have ha := h,
-    apply_fun absR at ha,
-    norm_num at ha,
-    rcases (abs_real_inner_div_norm_mul_norm_eq_one_iff x y).1 ha with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩,
-    use [hx, r],
-    refine and.intro _ hy,
-    by_contradiction hrpos,
-    rw hy at h,
-    rw real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx
-      (lt_of_le_of_ne (le_of_not_lt hrpos) hr.symm) at h,
-    norm_num at h },
-  { intro h,
-    rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩,
-    rw hy,
-    exact real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul hx hr }
+  rw [← neg_eq_iff_eq_neg, ← neg_div, ← inner_neg_right, ← norm_neg y,
+    real_inner_div_norm_mul_norm_eq_one_iff, (@neg_surjective ℝ _).exists],
+  refine iff.rfl.and (exists_congr $ λ r, _),
+  rw [neg_pos, neg_smul, neg_inj]
 end
 
 /-- If the inner product of two vectors is equal to the product of their norms (i.e.,
@@ -1722,14 +1659,11 @@ linear_map.mk_continuous₂ (innerₛₗ 𝕜) 1
 begin
   refine le_antisymm ((innerSL 𝕜 x).op_norm_le_bound (norm_nonneg _)
     (λ y, norm_inner_le_norm _ _)) _,
-  cases eq_or_lt_of_le (norm_nonneg x) with h h,
-  { have : x = 0 := norm_eq_zero.mp (eq.symm h),
-    simp [this] },
-  { refine (mul_le_mul_right h).mp _,
-    calc ‖x‖ * ‖x‖ = ‖x‖ ^ 2 : by ring
-    ... = re ⟪x, x⟫ : norm_sq_eq_inner _
-    ... ≤ abs ⟪x, x⟫ : re_le_abs _
-    ... = ‖⟪x, x⟫‖ : by rw [←is_R_or_C.norm_eq_abs]
+  rcases eq_or_ne x 0 with (rfl | h),
+  { simp },
+  { refine (mul_le_mul_right (norm_pos_iff.2 h)).mp _,
+    calc ‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ : by rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow,
+      norm_of_real, norm_norm]
     ... ≤ ‖innerSL 𝕜 x‖ * ‖x‖ : (innerSL 𝕜 x).le_op_norm _ }
 end