English
Under antivariation of f and g, equality in the rearrangement inequality holds precisely when f and g∘σ antivary, i.e., the sums ∑ f_i g_i and ∑ f_i g_{σ(i)} are equal if and only if Antivary f (g ∘ σ).
Русский
При антивариации f и g равенство в перестановочном неравенстве наступает ровно тогда, когда f и g∘σ антивариантны, то есть суммы одинаковы: ∑ f_i g_i = ∑ f_i g_{σ(i)} тогда и только тогда, когда Antivary f (g ∘ σ).
LaTeX
$$$\displaystyle \sum_i f_i g_{\sigma(i)} = \sum_i f_i g_i \iff \text{Antivary}(f, g \circ σ)$$$
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 `g`. -/
theorem sum_mul_eq_sum_mul_comp_perm_iff (hfg : Antivary f g) :
∑ i, f i * g (σ i) = ∑ i, f i * g i ↔ Antivary f (g ∘ σ) :=
hfg.sum_smul_comp_perm_eq_sum_smul_iff
