Linear functionals bounded below on the nonnegative cone #
Over a linearly ordered field 𝕜, the nonnegative elements of an ordered 𝕜-module are a cone:
they are stable under multiplication by nonnegative scalars. A linear functional that is bounded
below on this cone is therefore nonnegative on it, since a negative value at w would be scaled
below any bound along the ray through w.
Main results #
LinearMap.apply_nonneg_of_forall_le: a linear functional bounded below on the nonnegative elements is nonnegative on them.
theorem
LinearMap.apply_nonneg_of_forall_le
{𝕜 : Type u_1}
{V : Type u_2}
[Field 𝕜]
[LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜]
[AddCommMonoid V]
[Preorder V]
[Module 𝕜 V]
[PosSMulMono 𝕜 V]
(ψ : V →ₗ[𝕜] 𝕜)
{u : 𝕜}
(hψ : ∀ (w : V), 0 ≤ w → u ≤ ψ w)
{w : V}
(hw : 0 ≤ w)
:
A linear functional on an ordered module over a linearly ordered field that is bounded below on the nonnegative elements is nonnegative on them.