Dot product of two vectors

This file contains some results on the map Matrix.dotProduct, which maps two vectors v w : n → R to the sum of the entrywise products v i * w i.

Main results

• Matrix.dotProduct_stdBasis_one: the dot product of v with the ith standard basis vector is v i
• Matrix.dotProduct_eq_zero_iff: if v's' dot product with all w is zero, then v is zero

Tags

matrix, reindex

@[simp]

theorem Matrix.dotProduct_stdBasis_eq_mul {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] [DecidableEq n] (v : n → R) (c : R) (i : n) : Matrix.dotProduct v ((LinearMap.stdBasis R (fun (x : n) => R) i) c) = v i * c

theorem Matrix.dotProduct_stdBasis_one {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] [DecidableEq n] (v : n → R) (i : n) : Matrix.dotProduct v ((LinearMap.stdBasis R (fun (x : n) => R) i) 1) = v i

theorem Matrix.dotProduct_eq {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] (v : n → R) (w : n → R) (h : ∀ (u : n → R), Matrix.dotProduct v u = Matrix.dotProduct w u) : v = w

theorem Matrix.dotProduct_eq_iff {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] {v : n → R} {w : n → R} : (∀ (u : n → R), Matrix.dotProduct v u = Matrix.dotProduct w u) ↔ v = w

theorem Matrix.dotProduct_eq_zero {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] (v : n → R) (h : ∀ (w : n → R), Matrix.dotProduct v w = 0) : v = 0

theorem Matrix.dotProduct_eq_zero_iff {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] {v : n → R} : (∀ (w : n → R), Matrix.dotProduct v w = 0) ↔ v = 0

theorem Matrix.dotProduct_nonneg_of_nonneg {n : Type u_2} {R : Type u_4} [OrderedSemiring R] [Fintype n] {v : n → R} {w : n → R} (hv : 0 ≤ v) (hw : 0 ≤ w) : 0 ≤ Matrix.dotProduct v w

theorem Matrix.dotProduct_le_dotProduct_of_nonneg_right {n : Type u_2} {R : Type u_4} [OrderedSemiring R] [Fintype n] {u : n → R} {v : n → R} {w : n → R} (huv : u ≤ v) (hw : 0 ≤ w) : Matrix.dotProduct u w ≤ Matrix.dotProduct v w

theorem Matrix.dotProduct_le_dotProduct_of_nonneg_left {n : Type u_2} {R : Type u_4} [OrderedSemiring R] [Fintype n] {u : n → R} {v : n → R} {w : n → R} (huv : u ≤ v) (hw : 0 ≤ w) : Matrix.dotProduct w u ≤ Matrix.dotProduct w v

@[simp]

theorem Matrix.dotProduct_self_eq_zero {n : Type u_2} {R : Type u_4} [Fintype n] [LinearOrderedRing R] {v : n → R} : Matrix.dotProduct v v = 0 ↔ v = 0

@[simp]

theorem Matrix.dotProduct_star_self_eq_zero {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R} : Matrix.dotProduct (star v) v = 0 ↔ v = 0

Note that this applies to ℂ via Complex.strictOrderedCommRing.

@[simp]

theorem Matrix.dotProduct_self_star_eq_zero {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R} : Matrix.dotProduct v (star v) = 0 ↔ v = 0

Note that this applies to ℂ via Complex.strictOrderedCommRing.

@[simp]

theorem Matrix.conjTranspose_mul_self_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype m] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {A : Matrix m n R} : A.conjTranspose * A = 0 ↔ A = 0

@[simp]

theorem Matrix.self_mul_conjTranspose_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {A : Matrix m n R} : A * A.conjTranspose = 0 ↔ A = 0

theorem Matrix.conjTranspose_mul_self_mul_eq_zero {m : Type u_1} {n : Type u_2} {p : Type u_3} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (B : Matrix n p R) : A.conjTranspose * A * B = 0 ↔ A * B = 0

theorem Matrix.self_mul_conjTranspose_mul_eq_zero {m : Type u_1} {n : Type u_2} {p : Type u_3} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (B : Matrix m p R) : A * A.conjTranspose * B = 0 ↔ A.conjTranspose * B = 0

theorem Matrix.mul_self_mul_conjTranspose_eq_zero {m : Type u_1} {n : Type u_2} {p : Type u_3} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (B : Matrix p m R) : B * (A * A.conjTranspose) = 0 ↔ B * A = 0

theorem Matrix.mul_conjTranspose_mul_self_eq_zero {m : Type u_1} {n : Type u_2} {p : Type u_3} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (B : Matrix p n R) : B * (A.conjTranspose * A) = 0 ↔ B * A.conjTranspose = 0

theorem Matrix.conjTranspose_mul_self_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (v : n → R) : (A.conjTranspose * A).mulVec v = 0 ↔ A.mulVec v = 0

theorem Matrix.self_mul_conjTranspose_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (v : m → R) : (A * A.conjTranspose).mulVec v = 0 ↔ A.conjTranspose.mulVec v = 0

theorem Matrix.vecMul_conjTranspose_mul_self_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (v : n → R) : Matrix.vecMul v (A.conjTranspose * A) = 0 ↔ Matrix.vecMul v A.conjTranspose = 0

theorem Matrix.vecMul_self_mul_conjTranspose_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype m] [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (v : m → R) : Matrix.vecMul v (A * A.conjTranspose) = 0 ↔ Matrix.vecMul v A = 0