English
Strict inequality for MonovaryOn f g: ∑ f(i)·g(σ(i)) < ∑ f(i)·g(i) iff not Monovary (f ∘ σ) g.
Русский
Строгое неравенство для MonovaryOn: ∑ f(i)·g(σ(i)) < ∑ f(i)·g(i) тогда и только тогда, когда не выполняется Monovary (f ∘ σ) g.
LaTeX
$$$\displaystyle \text{If } \operatorname{MonovaryOn}(f,g,s) \text{ then } \sum_{i} f(i) \cdot g(σ(i)) < \sum_{i} f(i) \cdot g(i) \iff \neg \operatorname{MonovaryOn}(f \circ σ, g, s).$$$
Lean4
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which monovary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together. Stated by permuting the entries of `g`. -/
theorem sum_comp_perm_mul_lt_sum_mul_iff (hfg : Monovary f g) :
∑ i, f (σ i) * g i < ∑ i, f i * g i ↔ ¬Monovary (f ∘ σ) g :=
hfg.sum_comp_perm_smul_lt_sum_smul_iff
