sum_mul_le_sum_mul_comp_perm — Mathlib

English

AntivaryOn f g on s implies a symmetric equivalence between the sum with σ and the sum without, in terms of antivary on f∘σ and g.

Русский

AntivaryOn f g на s эквивалентно симметрии между суммой с σ и без σ через antivary на f∘σ и g.

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 minimized when `f` and
`g` antivary together on `s`. Stated by permuting the entries of `g`. -/
theorem sum_mul_le_sum_mul_comp_perm (hfg : AntivaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, f i * g (σ i) :=
  hfg.sum_smul_le_sum_smul_comp_perm hσ

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