English
If f and g antivary, then the strict inequality ∑ f_i g_i < ∑ f_{σ(i)} g_i holds precisely when ¬Antivary (f ∘ σ) g, i.e., the sum with f permuted strictly exceeds the original only if f and g ∘ σ are not antivary.
Русский
Если f и g антивариантны, то строгое неравенство ∑ f_i g_i < ∑ f_{σ(i)} g_i выполняется ровно тогда, когда ¬Antivary (f ∘ σ) g; иначе сумма нестрого больше.
LaTeX
$$$\displaystyle \sum_i f_i g_i < \sum_i f_{\sigma(i)} g_i \iff \neg \text{Antivary}(f \circ σ, g)$$$
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 `f`. -/
theorem sum_mul_lt_sum_comp_perm_mul_iff (hfg : Antivary f g) :
∑ i, f i * g i < ∑ i, f (σ i) * g i ↔ ¬Antivary (f ∘ σ) g :=
hfg.sum_smul_lt_sum_comp_perm_smul_iff
