Matrix.dotProduct inequalities (#9652)

Author: madvorak

Mathlib/LinearAlgebra/Matrix/DotProduct.lean

@@ -70,6 +70,23 @@ theorem dotProduct_eq_zero_iff {v : n → R} : (∀ w, dotProduct v w = 0) ↔ v
 
 end Semiring
 
+section OrderedSemiring
+
+variable [OrderedSemiring R] [Fintype n]
+
+lemma dotProduct_nonneg_of_nonneg {v w : n → R} (hv : 0 ≤ v) (hw : 0 ≤ w) : 0 ≤ dotProduct v w :=
+  Finset.sum_nonneg (fun i _ => mul_nonneg (hv i) (hw i))
+
+lemma dotProduct_le_dotProduct_of_nonneg_right {u v w : n → R} (huv : u ≤ v) (hw : 0 ≤ w) :
+    dotProduct u w ≤ dotProduct v w :=
+  Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_right (huv i) (hw i))
+
+lemma dotProduct_le_dotProduct_of_nonneg_left {u v w : n → R} (huv : u ≤ v) (hw : 0 ≤ w) :
+    dotProduct w u ≤ dotProduct w v :=
+  Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_left (huv i) (hw i))
+
+end OrderedSemiring
+
 section Self
 
 variable [Fintype m] [Fintype n] [Fintype p]