English
Equality case of AntivaryOn sum_mul_eq_sum_mul_comp_perm_iff: ∑ f i * g(σ i) = ∑ f i * g i iff AntivaryOn f (g ∘ σ) s.
Русский
Условие равенства: сумма произведений остаётся равной тогда и только тогда, когда AntivaryOn f (g ∘ σ) s.
LaTeX
$$$\displaystyle \text{If } \operatorname{AntivaryOn}(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{AntivaryOn}(f, g \circ σ, 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_comp_perm_mul_eq_sum_mul_iff (hfg : Monovary f g) :
∑ i, f (σ i) * g i = ∑ i, f i * g i ↔ Monovary (f ∘ σ) g :=
hfg.sum_comp_perm_smul_eq_sum_smul_iff
