Comparing two choices under two linear penalties #
Suppose that the choice (a₀, d₀) is at least as good as (a₁, d₁) for the objective
a + s * d, and (a₁, d₁) is at least as good as (a₀, d₀) for the objective a + t * d, with
a smaller penalty 0 ≤ t < s. Then d₀ ≤ d₁ and a₁ ≤ a₀: lowering the penalty on d can only
increase d and decrease a. This is the exchange argument behind the monotonicity of minimizers
of a linearly penalized objective in the penalty, for instance of resolvent steps in the time step.
Main results #
TauCeti.le_and_le_of_add_mul_le_add_mul: the comparison above.
theorem
TauCeti.le_and_le_of_add_mul_le_add_mul
{R : Type u_1}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{a₀ a₁ d₀ d₁ s t : R}
(ht : 0 ≤ t)
(hts : t < s)
(h₀ : a₀ + s * d₀ ≤ a₁ + s * d₁)
(h₁ : a₁ + t * d₁ ≤ a₀ + t * d₀)
:
Exchange argument for two linear penalties. If a₀ + s d₀ ≤ a₁ + s d₁ and
a₁ + t d₁ ≤ a₀ + t d₀ with 0 ≤ t < s, then d₀ ≤ d₁ and a₁ ≤ a₀.