sum_comp_perm_smul_eq_sum_smul_iff

English

Equality iff antiviral relation between f and g after composing with σ on s.

Русский

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

LaTeX

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

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 `f`. -/
theorem sum_comp_perm_smul_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_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

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