English
Equality case for antivary on σ: sum f(i) smul g(σ i) equals sum f(i) smul g(i) iff antivary on f and g with σ.
Русский
Равенство для antivary при σ: сумма равна только в том случае, когда antivary на f и g с σ.
LaTeX
$$$$ \sum_i f(i) \cdot g(σ(i)) = \sum_i f(i) \cdot g(i) \iff \text{AntivaryOn}(f, g) \text{ with } σ $$$$
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 `f`. -/
theorem sum_comp_perm_smul_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_comp_perm_smul_eq_sum_smul_iff hσ).trans monovaryOn_toDual_right
