English
If f and g antivary, then equality in the rearrangement inequality under permutation of f holds precisely when Antivary (f ∘ σ) g, i.e., ∑ f(σ(i)) g(i) = ∑ f(i) g(i) iff Antivary f (g ∘ σ).
Русский
Если f и g антивариантны, то равенство в неравенстве перестановок при перестановке f наступает тогда и только тогда, когда Antivary (f ∘ σ) g; то есть ∑ f(σ(i)) g(i) = ∑ f(i) g(i) ⇔ Antivary f (g ∘ σ).
LaTeX
$$$\displaystyle \sum_i f(\sigma(i)) g_i = \sum_i f_i g_i \iff \text{Antivary}(f \circ σ, g)$$$
Lean4
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which antivary together, is unchanged by a permutation if and only if `f ∘ σ` and `g` antivary
together. Stated by permuting the entries of `f`. -/
theorem sum_comp_perm_mul_eq_sum_mul_iff (hfg : Antivary f g) :
∑ i, f (σ i) * g i = ∑ i, f i * g i ↔ Antivary (f ∘ σ) g :=
hfg.sum_comp_perm_smul_eq_sum_smul_iff
