sum_smul_le_sum_smul_comp_perm — Mathlib

English

Equality case: sum ∑ f_i·g(σ(i)) equals ∑ f_i·g(i) iff antivary on f and g∘σ; equivalently, MonovaryOn f (g ∘ σ) ⇔ equality.

Русский

Равенство имеет место тогда и только тогда, когда f и g ∘ σ антивариантны.

LaTeX

$$$$ \sum_{i} f(i) \cdot g(\sigma(i)) = \sum_{i} f(i) \cdot g(i) \iff \text{AntivaryOn}(f, g \circ σ) $$$$

Lean4

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

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