English
Equality occurs iff MonovaryOn f g s and the σ-permutation preserves the monovariant relation on s.
Русский
Равенство возникает тогда, когда MonovaryOn f g s выполняется и перестановка σ сохраняет моновариантность на s.
LaTeX
$$$$ \sum_i f(i) \cdot g(σ(i)) = \sum_i f(i) \cdot g(i) \iff \text{MonovaryOn}(f, g) \text{ with } σ $$$$
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 `g`. -/
theorem sum_smul_comp_perm_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_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne, hfg.sum_smul_comp_perm_le_sum_smul hσ]
