Documentation

Mathlib.LinearAlgebra.Matrix.DotProduct

Dot product of two vectors #

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

Main results #

Tags #

matrix

source
@[simp, deprecated Matrix.dotProduct_single]
theorem 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) :
v ⬝ᵥ (LinearMap.stdBasis R (fun (x : n) => R) i) c = v i * c
source
@[deprecated Matrix.dotProduct_single_one]
theorem dotProduct_stdBasis_one {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] [DecidableEq n] (v : n → R) (i : n) :
v ⬝ᵥ (LinearMap.stdBasis R (fun (x : n) => R) i) 1 = v i
source
theorem dotProduct_eq {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] (v w : n → R) (h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u) :
v = w
source
@[deprecated dotProduct_eq]
theorem Matrix.dotProduct_eq {n : Type u_2} {R : Type u_4} [Semiring R] [Fintype n] (v w : n → R) (h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u) :
v = w

Alias of dotProduct_eq.

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

Alias of dotProduct_eq_iff.

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

Alias of dotProduct_eq_zero.

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

Alias of dotProduct_eq_zero_iff.

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

Alias of dotProduct_nonneg_of_nonneg.

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

Alias of dotProduct_le_dotProduct_of_nonneg_right.

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

Alias of dotProduct_le_dotProduct_of_nonneg_left.

source
@[simp]
theorem dotProduct_self_eq_zero {n : Type u_2} {R : Type u_4} [Fintype n] [LinearOrderedRing R] {v : n → R} :
v ⬝ᵥ v = 0 ↔ v = 0
source
@[deprecated dotProduct_self_eq_zero]
theorem Matrix.dotProduct_self_eq_zero {n : Type u_2} {R : Type u_4} [Fintype n] [LinearOrderedRing R] {v : n → R} :
v ⬝ᵥ v = 0 ↔ v = 0

Alias of dotProduct_self_eq_zero.

source
@[simp]
theorem dotProduct_star_self_nonneg {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] (v : n → R) :
0 ≤ star v ⬝ᵥ v

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[deprecated dotProduct_star_self_nonneg]
theorem Matrix.dotProduct_star_self_nonneg {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] (v : n → R) :
0 ≤ star v ⬝ᵥ v

Alias of dotProduct_star_self_nonneg.

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[simp]
theorem dotProduct_self_star_nonneg {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] (v : n → R) :
0 ≤ v ⬝ᵥ star v

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[deprecated dotProduct_self_star_nonneg]
theorem Matrix.dotProduct_self_star_nonneg {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] (v : n → R) :
0 ≤ v ⬝ᵥ star v

Alias of dotProduct_self_star_nonneg.

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[simp]
theorem 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} :
star v ⬝ᵥ v = 0 ↔ v = 0

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[deprecated dotProduct_star_self_eq_zero]
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} :
star v ⬝ᵥ v = 0 ↔ v = 0

Alias of dotProduct_star_self_eq_zero.

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[simp]
theorem 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} :
v ⬝ᵥ star v = 0 ↔ v = 0

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[deprecated dotProduct_self_star_eq_zero]
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} :
v ⬝ᵥ star v = 0 ↔ v = 0

Alias of dotProduct_self_star_eq_zero.

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[simp]
theorem Matrix.conjTranspose_mul_self_eq_zero {m : Type u_1} {R : Type u_4} [Fintype m] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {n : Type u_5} {A : Matrix m n R} :
A.conjTranspose * A = 0 ↔ A = 0
source
@[simp]
theorem Matrix.self_mul_conjTranspose_eq_zero {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {m : Type u_5} {A : Matrix m n R} :
A * A.conjTranspose = 0 ↔ A = 0
source
theorem Matrix.conjTranspose_mul_self_mul_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] {p : Type u_5} (A : Matrix m n R) (B : Matrix n p R) :
A.conjTranspose * A * B = 0 ↔ A * B = 0
source
theorem Matrix.self_mul_conjTranspose_mul_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] {p : Type u_5} (A : Matrix m n R) (B : Matrix m p R) :
A * A.conjTranspose * B = 0 ↔ A.conjTranspose * B = 0
source
theorem Matrix.mul_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] {p : Type u_5} (A : Matrix m n R) (B : Matrix p m R) :
B * (A * A.conjTranspose) = 0 ↔ B * A = 0
source
theorem Matrix.mul_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] {p : Type u_5} (A : Matrix m n R) (B : Matrix p n R) :
B * (A.conjTranspose * A) = 0 ↔ B * A.conjTranspose = 0
source
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
source
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
source
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
source
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
source
@[simp]
theorem Matrix.dotProduct_star_self_pos_iff {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R} :
0 < star v ⬝ᵥ v ↔ v ≠ 0

Note that this applies to ℂ via RCLike.toStarOrderedRing.

source
@[simp]
theorem Matrix.dotProduct_self_star_pos_iff {n : Type u_2} {R : Type u_4} [Fintype n] [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R} :
0 < v ⬝ᵥ star v ↔ v ≠ 0

Note that this applies to ℂ via RCLike.toStarOrderedRing.