sum_smul_le_sum_smul_comp_perm — Mathlib

English

If f and g antivary on a finite set s, then the sum ∑ f_i·g_i is bounded above by the sum ∑ f_i·g(σ(i)) for any permutation σ with moved points inside s.

Русский

Если f и g антивариантны на конечном множестве s, то сумма ∑ f_i·g_i не превышает сумму ∑ f_i·g(σ(i)) для любой перестановки σ, с переносом элементов в s.

LaTeX

$$$$ \sum_{i \in s} f(i) \cdot g(i) \le \sum_{i \in s} f(i) \cdot g(\sigma(i)) $$$$

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 `g`. -/
theorem sum_smul_le_sum_smul_comp_perm (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_smul_comp_perm_le_sum_smul hσ

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