sum_smul_comp_perm_eq_sum_smul_iff

English

Equality occurs if and only if MonovaryOn f g s holds when composed with σ on s.

Русский

Равенство достигается тогда, когда MonovaryOn f g s выполняется после композиции с σ на s.

LaTeX

$$$$ \sum_i f(i) \cdot g(σ(i)) = \sum_i f(i) \cdot g(i) \iff \text{MonovaryOn}(f, g) \circ σ \; on \, s $$$$

Lean4

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

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