English
Let f and g monovary on s. For a permutation σ with {x | σ x ≠ x} ⊆ s, the sum ∑_{i∈s} f(i)·g(i) is strictly decreased when replacing g by g∘σ if and only if f and g∘σ are not monovary on s.
Русский
Пусть f и g моноубывают на s. При перестановке σ с условием {x | σ x ≠ x} ⊆ s, сумма ∑_{i∈s} f(i)·g(i) строго уменьшается при замене g на g∘σ тогда, когда f и g∘σ не моно-варь на s.
LaTeX
$$$\displaystyle \text{If } \operatorname{MonovaryOn}(f,g,s) \text{ and } \{x | σ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{MonovaryOn}(f \circ σ, g, s).$$$
Lean4
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which monovary together on `s`, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not monovary together on `s`. Stated by permuting the entries of `f`. -/
theorem sum_comp_perm_smul_lt_sum_smul_iff (hfg : MonovaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ σ) g s := by
simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, lt_iff_le_and_ne, hfg.sum_comp_perm_smul_le_sum_smul hσ]
