English
If f and g antivary, then the strict decrease ∑ f_i g_i < ∑ f_i g_{σ(i)} occurs precisely when f and g ∘ σ do not antivary; equivalently, the strict inequality holds if and only if ¬Antivary f (g ∘ σ).
Русский
Если f и g антивариантны, то строгая разность ∑ f_i g_i < ∑ f_i g_{σ(i)} наступает тогда, когда f и g ∘ σ не антивариантны; то есть неравенство строгой, если и только если ¬Antivary f (g ∘ σ).
LaTeX
$$$\displaystyle \sum_i f_i g_i < \sum_i f_i g_{\sigma(i)} \iff \neg \text{Antivary}(f, g \circ σ)$$$
Lean4
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which antivary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not antivary together. Stated by permuting the entries of `g`. -/
theorem sum_mul_lt_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_lt_sum_smul_comp_perm_iff
