English
Equality for MonovaryOn: ∑ f (σ i) * g i = ∑ f i * g i iff MonovaryOn (f ∘ σ) g s.
Русский
Равенство для MonovaryOn: сумма равна тогда и только тогда, когда MonovaryOn (f ∘ σ) g s.
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 \circ σ, g, s).$$$
Lean4
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which antivary together on `s`, is unchanged by a permutation if and only if `f ∘ σ` and `g`
antivary together on `s`. Stated by permuting the entries of `f`. -/
theorem sum_comp_perm_mul_eq_sum_mul_iff (hfg : AntivaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
∑ i ∈ s, f (σ i) * g i = ∑ i ∈ s, f i * g i ↔ AntivaryOn (f ∘ σ) g s :=
hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ
