sum_smul_comp_perm_le_sum_smul — Mathlib

English

If f and g are monovariant on s, then the sum of smul-products with a fixed permutation σ is bounded by the sum without permutation: sum_{i} f_i·g_{σ(i)} ≤ sum_i f_i·g_i.

Русский

Если f и g моновариантны на s, то сумма произведений с перестановкой σ не превышает исходную сумму.

LaTeX

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

Lean4

/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is maximized when
`f` and `g` monovary together. Stated by permuting the entries of `g`. -/
theorem sum_smul_comp_perm_le_sum_smul (hfg : Monovary f g) : ∑ i, f i • g (σ i) ≤ ∑ i, f i • g i :=
  (hfg.monovaryOn _).sum_smul_comp_perm_le_sum_smul fun _ _ ↦ mem_univ _

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