English
Let f : ι → α and g : ι → β be functions on a finite index set s, taking values in ordered structures, and suppose f and g antivary on s. If σ is a permutation with the property that only elements of s move (i.e., {x | σ x ≠ x} ⊆ s), then the pointwise product sum ∑_{i∈s} f(i)·g(i) is strictly decreased by applying σ to g if and only if f and g∘σ do not antivary on s.
Русский
Пусть f:ι→α и g:ι→β — функции, индексируемые по конечному множеству s, где значения лежат в упорядоченных структурах. Если f и g antivary на s и σ — перестановка, которая движет только элементы из s ({x | σ x ≠ x} ⊆ s), то сумма по i∈s f(i)·g(i) строго уменьшается после замены g на g∘σ тогда и только тогда, когда f и g∘σ не antivary на s.
LaTeX
$$$\displaystyle \text{If } \operatorname{AntivaryOn}(f,g,s) \text{ and } \{x \mid σx \neq x\} \subseteq s, \\ \sum_{i \in s} f(i) \cdot g(i) < \sum_{i \in s} f(i) \cdot g(σ(i)) \iff \neg \operatorname{AntivaryOn}(f, g \circ σ, s).$$$
Lean4
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which antivary together on `s`, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not antivary together on `s`. Stated by permuting the entries of `g`. -/
theorem sum_smul_lt_sum_smul_comp_perm_iff (hfg : AntivaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
∑ i ∈ s, f i • g i < ∑ i ∈ s, f i • g (σ i) ↔ ¬AntivaryOn f (g ∘ σ) s := by
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne, eq_comm, hfg.sum_smul_le_sum_smul_comp_perm hσ]
