English
Equality case for antivary on s: the two sum expressions are equal iff antivaryOn for f and g∘σ on s holds.
Русский
Равенство для antivary на s: равенство сумм эквивалентно antivaryOn для f и g ∘ σ на s.
LaTeX
$$$$ \sum_i f(i) \cdot g(σ(i)) = \sum_i f(i) \cdot g(i) \iff \text{AntivaryOn}(f, g \circ σ) \, on \, s $$$$
Lean4
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar 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 `g`. -/
theorem sum_smul_comp_perm_eq_sum_smul_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.dual_right.sum_smul_comp_perm_eq_sum_smul_iff hσ).trans monovaryOn_toDual_right
