sum_mul_le_sum_comp_perm_mul — Mathlib

English

If f and g antivary, then the sum with g fixed and f permuted does not exceed the original sum: ∑ f_i g_i ≤ ∑ f_{σ(i)} g_i.

Русский

Если f и g антивариантны, то сумма, где g фиксирована, а f переставлена по σ, не превышает исходную сумму: ∑ f_i g_i ≤ ∑ f_{σ(i)} g_i.

LaTeX

$$$\displaystyle \sum_i f_i g_i \le \sum_i f_{\sigma(i)} g_i$$$

Lean4

/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is minimized when `f` and
`g` antivary together. Stated by permuting the entries of `f`. -/
theorem sum_mul_le_sum_comp_perm_mul (hfg : Antivary f g) : ∑ i, f i * g i ≤ ∑ i, f (σ i) * g i :=
  hfg.sum_smul_le_sum_comp_perm_smul

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