sum_mul_comp_perm_le_sum_mul — Mathlib

English

Strict inequality for MonovaryOn with equality under sum_mul_eq_sum_mul_iff: ∑ f(σ i)·g i < ∑ f i · g i iff not MonovaryOn (f ∘ σ) g s.

Русский

Строгое неравенство для MonovaryOn: если сумма меньше, то не выполняется MonovaryOn (f ∘ σ) g s.

LaTeX

$$$\displaystyle \text{If } \operatorname{MonovaryOn}(f,g,s) \text{ then } \sum_{i\in s} f(σ(i)) \cdot g(i) < \sum_{i\in s} f(i) \cdot g(i) \iff \neg \operatorname{MonovaryOn}(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 `g`. -/
theorem sum_mul_comp_perm_le_sum_mul (hfg : Monovary f g) : ∑ i, f i * g (σ i) ≤ ∑ i, f i * g i :=
  hfg.sum_smul_comp_perm_le_sum_smul

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