sum_comp_perm_mul_le_sum_mul — Mathlib

English

Equality for AntivaryOn f g on s: sum of products unchanged by permutation iff f ∘ σ and g are antivary on s.

Русский

Условие равенства: сумма произведений не изменяется при перестановке тогда, когда f∘σ и g остаются антивариантными на s.

LaTeX

$$$\displaystyle \text{If } \operatorname{AntivaryOn}(f,g,s) \text{ then } \sum_{i\in s} f(i) \cdot g(i) = \sum_{i\in s} f(σ(i)) \cdot g(i) \iff \operatorname{AntivaryOn}(f \circ σ, g, s).$$$

Lean4

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

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