English
Equality case for MonovaryOn with σ: sum with σ equals sum without σ iff f and g monovary after σ.
Русский
Условие равенства для MonovaryOn: сумма с σ равна сумме без σ тогда, когда f и g моно-варь после применения σ.
LaTeX
$$$\displaystyle \text{If } \operatorname{MonovaryOn}(f,g,s) \text{ then } \sum_{i\in s} f(σ(i)) \cdot g(i) = \sum_{i\in s} f(i) \cdot g(i) \iff \operatorname{MonovaryOn}(f, g, s).$$$
Lean4
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which monovary together, is unchanged by a permutation if and only if `f` and `g ∘ σ` monovary
together. Stated by permuting the entries of `g`. -/
theorem sum_mul_comp_perm_eq_sum_mul_iff (hfg : Monovary f g) :
∑ i, f i * g (σ i) = ∑ i, f i * g i ↔ Monovary f (g ∘ σ) :=
hfg.sum_smul_comp_perm_eq_sum_smul_iff
