English
Equality for AntivaryOn: ∑ f i · g i = ∑ f i · g(σ i) iff AntivaryOn f (g ∘ σ) s.
Русский
Равенство для AntivaryOn: сумма равна тогда и только тогда, когда AntivaryOn f (g ∘ σ) s.
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 \circ σ, s).$$$
Lean4
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which antivary together on `s`, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not antivary together on `s`. Stated by permuting the entries of `f`. -/
theorem sum_mul_lt_sum_comp_perm_mul_iff (hfg : AntivaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
∑ i ∈ s, f i * g i < ∑ i ∈ s, f (σ i) * g i ↔ ¬AntivaryOn (f ∘ σ) g s :=
hfg.sum_smul_lt_sum_comp_perm_smul_iff hσ
