English
Equality case: if MonovaryOn f g on s and the condition on σ holds, then ∑ f i · g(σ i) = ∑ f i · g i if and only if MonovaryOn f (g ∘ σ) s.
Русский
Равенство: если MonovaryOn f g на s и выполняется условие на σ, то ∑ f(i)g(σ(i)) = ∑ f(i)g(i) тогда и только тогда, когда MonovaryOn f (g ∘ σ) s.
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
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which monovary together on `s`, is unchanged by a permutation if and only if `f` and `g ∘ σ`
monovary together on `s`. Stated by permuting the entries of `g`. -/
theorem sum_mul_comp_perm_eq_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_eq_sum_smul_iff hσ
