feat(analysis/inner_product_space/basic) : inner_map_self_eq_zero (#…

…12065)

The main result here is:  If ⟪T x, x⟫_C = 0 for all x, then T = 0.
The proof uses a polarization identity.  Note that this is false
with R in place of C.  I am confident that my use of ring_nf is
not optimal, but I hope to learn from the cleanup process!

Co-authored-by: Daniel Packer



Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>

src/analysis/inner_product_space/basic.lean

@@ -1066,6 +1066,42 @@ begin
   simp only [sq, ← mul_div_right_comm, ← add_div]
 end
 
+section complex
+
+variables {V : Type*}
+[inner_product_space ℂ V]
+/--
+A complex polarization identity, with a linear map
+-/
+lemma inner_map_polarization (T : V →ₗ[ℂ] V) (x y : V):
+  ⟪ T y, x ⟫_ℂ = (⟪T (x + y) , x + y⟫_ℂ - ⟪T (x - y) , x - y⟫_ℂ +
+    complex.I * ⟪T (x + complex.I • y) , x + complex.I • y⟫_ℂ -
+    complex.I * ⟪T (x - complex.I • y), x - complex.I • y ⟫_ℂ) / 4 :=
+begin
+  simp only [map_add, map_sub, inner_add_left, inner_add_right, linear_map.map_smul,
+             inner_smul_left, inner_smul_right, complex.conj_I, ←pow_two, complex.I_sq,
+             inner_sub_left, inner_sub_right, mul_add, ←mul_assoc, mul_neg, neg_neg,
+             sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub],
+  ring,
+end
+
+/--
+If `⟪T x, x⟫_ℂ = 0` for all x, then T = 0.
+-/
+lemma inner_map_self_eq_zero (T : V →ₗ[ℂ] V) :
+  (∀ (x : V), ⟪T x, x⟫_ℂ = 0) ↔ T = 0 :=
+begin
+  split,
+  { intro hT,
+    ext x,
+    simp only [linear_map.zero_apply, ← inner_self_eq_zero, inner_map_polarization, hT],
+    norm_num },
+  { rintro rfl x,
+    simp only [linear_map.zero_apply, inner_zero_left] }
+end
+
+end complex
+
 section
 
 variables {ι : Type*} {ι' : Type*} {ι'' : Type*}