English
Equality case for MonovaryOn with regards to sum of products under a permutation: sum of f(i)·g(σ(i)) equals sum of f(i)·g(i) iff MonovaryOn f g with the permuted second argument.
Русский
Условия равенства для MonovaryOn по сумме произведений при перестановке: сумма f(i)·g(σ(i)) равна сумме f(i)·g(i) тогда и только тогда, когда MonovaryOn f g с переставленным вторым аргументом выполняется.
LaTeX
$$$\displaystyle \text{If } \operatorname{MonovaryOn}(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 \operatorname{MonovaryOn}(f, g \circ σ, 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 `g`. -/
theorem sum_mul_comp_perm_lt_sum_mul_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 :=
hfg.sum_smul_comp_perm_lt_sum_smul_iff hσ
