Strict monotonicity of the dot product #
Mathlib proves that w ⬝ᵥ u ≤ w ⬝ᵥ v when u ≤ v pointwise and w is nonnegative
(dotProduct_le_dotProduct_of_nonneg_left). This file adds the strict version, in which the
inequality is strict as soon as u lies strictly below v at a coordinate where w is positive.
A weighted sum therefore respects a Pareto improvement on any positively weighted coordinate.
Main results #
dotProduct_lt_dotProduct_of_nonneg_left,dotProduct_lt_dotProduct_of_nonneg_right: the strict monotonicity of the dot product in either argument.
theorem
dotProduct_lt_dotProduct_of_nonneg_left
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{u v w : n → R}
(huv : u ≤ v)
(hw : 0 ≤ w)
(h : ∃ (i : n), 0 < w i ∧ u i < v i)
:
w ⬝ᵥ u < w ⬝ᵥ v
The dot product with a nonnegative vector w is strictly monotone in the other argument
when the increase is strict at a coordinate where w is positive.
theorem
dotProduct_lt_dotProduct_of_nonneg_right
{n : Type u_1}
{R : Type u_2}
[Fintype n]
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{u v w : n → R}
(huv : u ≤ v)
(hw : 0 ≤ w)
(h : ∃ (i : n), 0 < w i ∧ u i < v i)
:
u ⬝ᵥ w < v ⬝ᵥ w
The dot product with a nonnegative vector w on the right is strictly monotone in the left
argument when the increase is strict at a coordinate where w is positive.