sum_comp_perm_smul_eq_sum_smul_iff

English

Equality criterion for MonovaryOn with σ: the two sums are equal iff MonovaryOn f (g ∘ σ) on s.

Русский

Критерий равенства для моновариантности с σ: суммы равны тогда, когда MonovaryOn f (g ∘ σ) на s.

LaTeX

$$$$ \sum_i f(i) \cdot g(σ(i)) = \sum_i f(i) \cdot g(i) \iff \text{MonovaryOn}(f, g \circ σ) \text{ 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_comp_perm_smul_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_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

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