sum_comp_perm_smul_le_sum_smul — Mathlib

English

Equality condition for sum when f,g monovary on s and σ is a permutation: equality holds iff (f ∘ σ) monovaries with g.

Русский

Условие равенства суммы при моновариантности и перестановке: равенство, если и только если f∘σ моновариантно с g.

LaTeX

$$$$ \sum_i f(i) \cdot g(σ(i)) = \sum_i f(i) \cdot g(i) \iff \text{Monovary}(f, g\circ σ) $$$$

Lean4

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

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