English
Equality case: sum ∑ f_i·g(σ(i)) equals ∑ f_i·g(i) if and only if antivary on f and g∘σ.
Русский
Равенство: сумма ∑ f_i·g(σ(i)) равна ∑ f_i·g(i) тогда и только если f и g ∘ σ антивариантны на s.
LaTeX
$$$$ \sum_{i\in s} f(i) \cdot g(\sigma(i)) = \sum_{i\in s} f(i) \cdot g(i) \iff \text{AntivaryOn}(f, g \circ \sigma, s) $$$$
Lean4
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is maximized when
`f` and `g` monovary together on `s`. Stated by permuting the entries of `f`. -/
theorem sum_comp_perm_smul_le_sum_smul (hfg : MonovaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i :=
by
convert hfg.sum_smul_comp_perm_le_sum_smul (show {x | σ⁻¹ x ≠ x} ⊆ s by simp only [set_support_inv_eq, hσ]) using 1
exact σ.sum_comp' s (fun i j ↦ f i • g j) hσ
