sum_smul_le_sum_comp_perm_smul — Mathlib

English

Permutation equality implies antivarying relation with the composed map: ∑ f_i·g(σ(i)) = ∑ f_i·g(i) iff AntivaryOn f (g ∘ σ).

Русский

Равенство по перестановке эквивалентно антивариантности: сумма равна тогда, когда f и g ∘ σ антивариантны.

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 σ, s) $$$$

Lean4

/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is minimized when
`f` and `g` antivary together on `s`. Stated by permuting the entries of `f`. -/
theorem sum_smul_le_sum_comp_perm_smul (hfg : AntivaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f (σ i) • g i :=
  hfg.dual_right.sum_comp_perm_smul_le_sum_smul hσ

Похожие утверждения