sum_mul_comp_perm_le_sum_mul — Mathlib

English

MonovaryOn f g on s implies that the sum of f∘σ with g is less or equal to the sum without σ: ∑_{i∈s} f(i)g(σ i) ≤ ∑_{i∈s} f(i)g(i).

Русский

MonovaryOn f g на s даёт неубывание суммы ∑ f(i)g(i) по сравнению с σ-перестановкой.

LaTeX

$$$\displaystyle \text{If } \operatorname{MonovaryOn}(f,g,s) \text{ then } \sum_{i \in s} f(i) \cdot g(σ(i)) \le \sum_{i \in s} f(i) \cdot g(i).$$$

Lean4

/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is maximized when `f` and
`g` monovary together on `s`. Stated by permuting the entries of `g`. -/
theorem sum_mul_comp_perm_le_sum_mul (hfg : MonovaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f i * g (σ i) ≤ ∑ i ∈ s, f i * g i :=
  hfg.sum_smul_comp_perm_le_sum_smul hσ

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