English
For Antivary f g on s, the equivalence ∑ f i • g i < ∑ f i • g(σ i) ⇔ ¬Antivary (f ∘ σ) g holds.
Русский
Для Antivary f g на s верна эквивалентность ∑ f i • g i < ∑ f i • g(σ i) ⇔ ¬Antivary (f ∘ σ) g.
LaTeX
$$$\displaystyle \text{If } \operatorname{AntivaryOn}(f,g,s) \text{ then } \sum_{i} f(i) \cdot g(i) < \sum_{i} f(i) \cdot g(σ(i)) \iff \neg \operatorname{AntivaryOn}(f \circ σ, g, s).$$$
Lean4
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which antivary together, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not antivary together. Stated by permuting the entries of `f`. -/
theorem sum_smul_lt_sum_comp_perm_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_lt_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]
