English
For MonovaryOn f g on s, the sum ∑ f(i)•g(σ(i)) is strictly less than ∑ f(i)•g(i) exactly when f ∘ σ and g are not monovary on s.
Русский
Для MonovaryOn f g на s сумма ∑ f(i)•g(σ(i)) строго меньше ∑ f(i)•g(i) тогда, когда f∘σ и g не моно-варь на s.
LaTeX
$$$\displaystyle \text{If } \operatorname{MonovaryOn}(f,g,s) \text{ and } \{x | σx \neq x\} \subseteq s, \\ \sum_{i} f(σ(i)) \cdot g(i) < \sum_{i} 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, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together. Stated by permuting the entries of `g`. -/
theorem sum_smul_comp_perm_lt_sum_smul_iff (hfg : Monovary f g) :
∑ i, f i • g (σ i) < ∑ i, f i • g i ↔ ¬Monovary f (g ∘ σ) := by
simp [(hfg.monovaryOn _).sum_smul_comp_perm_lt_sum_smul_iff fun _ _ ↦ mem_univ _]
