English
Equality for AntivaryOn f g on s: sum of products unchanged under permutation iff antivary persists after σ.
Русский
Неравенство сохраняется при перестановке: сумма произведений остаётся неизменной тогда, когда сохранена антивариантность после σ.
LaTeX
$$$\displaystyle \text{If } \operatorname{AntivaryOn}(f,g,s) \text{ then } \sum_{i\in s} f(i) \cdot g(i) = \sum_{i\in s} f(σ(i)) \cdot g(i) \iff \operatorname{AntivaryOn}(f, g, σ).$$$
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_mul_comp_perm_lt_sum_mul_iff (hfg : Monovary f g) :
∑ i, f i * g (σ i) < ∑ i, f i * g i ↔ ¬Monovary f (g ∘ σ) :=
hfg.sum_smul_comp_perm_lt_sum_smul_iff
