feat: star self dot product eq zero and kernel lemmas apply to matric…

…es not just vectors (#6587)

This generalizes two results about vectors to matrices:
* `dotProduct_star_self_eq_zero` to `conjTranspose_mul_self_eq_zero` 
* `dotProduct_self_star_eq_zero` to `self_mul_conjTranspose_eq_zero`

It also adds lemmas linking the kernel (under left-multiplication, right-multiplication, `vecMul`, and `mulVec`) of $A$, $A^HA$, and $AA^H$.

Some of these lemmas are used in the SVD decomposition theorem of R or C matrices #6042 




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Matrix/Rank.lean

@@ -218,16 +218,7 @@ variable [Fintype m] [Field R] [PartialOrder R] [StarOrderedRing R]
 theorem ker_mulVecLin_conjTranspose_mul_self (A : Matrix m n R) :
     LinearMap.ker (Aᴴ * A).mulVecLin = LinearMap.ker (mulVecLin A) := by
   ext x
-  simp only [LinearMap.mem_ker, mulVecLin_apply, ← mulVec_mulVec]
-  constructor
-  · intro h
-    replace h := congr_arg (dotProduct (star x)) h
-    haveI : NoZeroDivisors R := inferInstance
-    rwa [dotProduct_mulVec, dotProduct_zero, vecMul_conjTranspose, star_star,
-      -- Porting note: couldn't find `NoZeroDivisors R` instance.
-      @dotProduct_star_self_eq_zero R _ _ _ _ _ ‹_›] at h
-  · intro h
-    rw [h, mulVec_zero]
+  simp only [LinearMap.mem_ker, mulVecLin_apply, conjTranspose_mul_self_mulVec_eq_zero]
 #align matrix.ker_mul_vec_lin_conj_transpose_mul_self Matrix.ker_mulVecLin_conjTranspose_mul_self
 
 theorem rank_conjTranspose_mul_self (A : Matrix m n R) : (Aᴴ * A).rank = A.rank := by

Mathlib/LinearAlgebra/Matrix/DotProduct.lean

@@ -29,9 +29,7 @@ matrix, reindex
 -/
 
 
-universe v w
-
-variable {R : Type v} {n : Type w}
+variable {m n p R : Type*}
 
 namespace Matrix
 
@@ -74,30 +72,84 @@ end Semiring
 
 section Self
 
-variable [Fintype n]
+variable [Fintype m] [Fintype n] [Fintype p]
 
 @[simp]
 theorem dotProduct_self_eq_zero [LinearOrderedRing R] {v : n → R} : dotProduct v v = 0 ↔ v = 0 :=
   (Finset.sum_eq_zero_iff_of_nonneg fun i _ => mul_self_nonneg (v i)).trans <| by
     simp [Function.funext_iff]
 #align matrix.dot_product_self_eq_zero Matrix.dotProduct_self_eq_zero
 
+section StarOrderedRing
+
+variable [PartialOrder R] [NonUnitalRing R] [StarOrderedRing R] [NoZeroDivisors R]
+
 /-- Note that this applies to `ℂ` via `Complex.strictOrderedCommRing`. -/
 @[simp]
-theorem dotProduct_star_self_eq_zero [PartialOrder R] [NonUnitalRing R] [StarOrderedRing R]
-    [NoZeroDivisors R] {v : n → R} : dotProduct (star v) v = 0 ↔ v = 0 :=
+theorem dotProduct_star_self_eq_zero {v : n → R} : dotProduct (star v) v = 0 ↔ v = 0 :=
   (Finset.sum_eq_zero_iff_of_nonneg fun i _ => (@star_mul_self_nonneg _ _ _ _ (v i) : _)).trans <|
     by simp [Function.funext_iff, mul_eq_zero]
 #align matrix.dot_product_star_self_eq_zero Matrix.dotProduct_star_self_eq_zero
 
 /-- Note that this applies to `ℂ` via `Complex.strictOrderedCommRing`. -/
 @[simp]
-theorem dotProduct_self_star_eq_zero [PartialOrder R] [NonUnitalRing R] [StarOrderedRing R]
-    [NoZeroDivisors R] {v : n → R} : dotProduct v (star v) = 0 ↔ v = 0 :=
+theorem dotProduct_self_star_eq_zero {v : n → R} : dotProduct v (star v) = 0 ↔ v = 0 :=
   (Finset.sum_eq_zero_iff_of_nonneg fun i _ => (@star_mul_self_nonneg' _ _ _ _ (v i) : _)).trans <|
     by simp [Function.funext_iff, mul_eq_zero]
 #align matrix.dot_product_self_star_eq_zero Matrix.dotProduct_self_star_eq_zero
 
+@[simp]
+lemma conjTranspose_mul_self_eq_zero {A : Matrix m n R} : Aᴴ * A = 0 ↔ A = 0 :=
+  ⟨fun h => Matrix.ext fun i j =>
+    (congr_fun <| dotProduct_star_self_eq_zero.1 <| Matrix.ext_iff.2 h j j) i,
+  fun h => h ▸ Matrix.mul_zero _⟩
+
+@[simp]
+lemma self_mul_conjTranspose_eq_zero {A : Matrix m n R} : A * Aᴴ = 0 ↔ A = 0 :=
+  ⟨fun h => Matrix.ext fun i j =>
+    (congr_fun <| dotProduct_self_star_eq_zero.1 <| Matrix.ext_iff.2 h i i) j,
+  fun h => h ▸ Matrix.zero_mul _⟩
+
+lemma conjTranspose_mul_self_mul_eq_zero (A : Matrix m n R) (B : Matrix n p R) :
+    (Aᴴ * A) * B = 0 ↔ A * B = 0 := by
+  refine ⟨fun h => ?_, fun h => by simp only [Matrix.mul_assoc, h, Matrix.mul_zero]⟩
+  apply_fun (Bᴴ * ·) at h
+  rwa [Matrix.mul_zero, Matrix.mul_assoc, ← Matrix.mul_assoc, ← conjTranspose_mul,
+    conjTranspose_mul_self_eq_zero] at h
+
+lemma self_mul_conjTranspose_mul_eq_zero (A : Matrix m n R) (B : Matrix m p R) :
+    (A * Aᴴ) * B = 0 ↔ Aᴴ * B = 0 := by
+  simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mul_eq_zero Aᴴ _
+
+lemma mul_self_mul_conjTranspose_eq_zero (A : Matrix m n R) (B : Matrix p m R) :
+    B * (A * Aᴴ) = 0 ↔ B * A = 0 := by
+  rw [← conjTranspose_eq_zero, conjTranspose_mul, conjTranspose_mul, conjTranspose_conjTranspose,
+    self_mul_conjTranspose_mul_eq_zero, ← conjTranspose_mul, conjTranspose_eq_zero]
+
+lemma mul_conjTranspose_mul_self_eq_zero (A : Matrix m n R) (B : Matrix p n R) :
+    B * (Aᴴ * A) = 0 ↔ B * Aᴴ = 0 := by
+  simpa only [conjTranspose_conjTranspose] using mul_self_mul_conjTranspose_eq_zero Aᴴ _
+
+lemma conjTranspose_mul_self_mulVec_eq_zero (A : Matrix m n R) (v : n → R) :
+    (Aᴴ * A).mulVec v = 0 ↔ A.mulVec v = 0 := by
+  simpa only [← Matrix.col_mulVec, col_eq_zero] using
+    conjTranspose_mul_self_mul_eq_zero A (col v)
+
+lemma self_mul_conjTranspose_mulVec_eq_zero (A : Matrix m n R) (v : m → R) :
+    (A * Aᴴ).mulVec v = 0 ↔ Aᴴ.mulVec v = 0 := by
+  simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mulVec_eq_zero Aᴴ _
+
+lemma vecMul_conjTranspose_mul_self_eq_zero (A : Matrix m n R) (v : n → R) :
+    vecMul v (Aᴴ * A) = 0 ↔ vecMul v Aᴴ = 0 := by
+  simpa only [← Matrix.row_vecMul, row_eq_zero] using
+    mul_conjTranspose_mul_self_eq_zero A (row v)
+
+lemma vecMul_self_mul_conjTranspose_eq_zero (A : Matrix m n R) (v : m → R) :
+    vecMul v (A * Aᴴ) = 0 ↔ vecMul v A = 0 := by
+  simpa only [conjTranspose_conjTranspose] using vecMul_conjTranspose_mul_self_eq_zero Aᴴ _
+
+end StarOrderedRing
+
 end Self
 
 end Matrix