English
Let f and g be sequences indexed by a finite set I, taking values in a totally ordered semiring. If f and g antivary (i.e., they move in opposite directions in a suitable sense), then for every permutation σ of I, the sum of pointwise products is minimized by antivarying g, that is, ∑_{i∈I} f(i) g(i) ≤ ∑_{i∈I} f(i) g(σ(i)).
Русский
Пусть f и g — последовательности, индексируемые конечным множеством I, значения в полностью упорядоченной полугруппе; если f и g антивариантны (движутся в противоположных направлениях), то для любой перестановки σ выполняется неравенство ∑_{i∈I} f(i) g(i) ≤ ∑_{i∈I} f(i) g(σ(i)).
LaTeX
$$$\displaystyle \sum_i f_i g_i \le \sum_i f_i g_{\sigma(i)}$$$
Lean4
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is minimized when `f` and
`g` antivary together. Stated by permuting the entries of `g`. -/
theorem sum_mul_le_sum_mul_comp_perm (hfg : Antivary f g) : ∑ i, f i * g i ≤ ∑ i, f i * g (σ i) :=
hfg.sum_smul_le_sum_smul_comp_perm
