sum_smul_comp_perm_eq_sum_smul_iff

English

Equality under antivary is characterized by antivaryOn for f and g ∘ σ on s.

Русский

Равенство при antivary описывается antivaryOn для f и g ∘ σ на s.

LaTeX

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

Lean4

/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which antivary together, is unchanged by a permutation if and only if `f` and `g ∘ σ` antivary
together. Stated by permuting the entries of `g`. -/
theorem sum_smul_comp_perm_eq_sum_smul_iff (hfg : Antivary f g) :
    ∑ i, f i • g (σ i) = ∑ i, f i • g i ↔ Antivary f (g ∘ σ) := by
  simp [(hfg.antivaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

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