sum_smul_le_sum_comp_perm_smul — Mathlib

English

Further antisymmetric rearrangement inequality: sum of smuls is minimized under antivary on s when comparing to a permuted version.

Русский

Дополнительное несимметричное неравенство перестановки: сумма скалярных произведений минимальна при антивариантности на s по отношению к перестановке.

LaTeX

$$$$ \sum_i f(i) \cdot g(i) \le \sum_i f(i) \cdot g(σ(i)) $$$$

Lean4

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

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