English
Let Antivary f g on ι. Then ∑ f i • g i < ∑ f i • g(σ i) is equivalent to ¬Antivary (f ∘ σ) g.
Русский
Пусть Antivary f g на ι. Тогда ∑ f(i)•g(i) < ∑ f(i)•g(σ(i)) эквивалентно ¬Antivary (f ∘ σ) g.
LaTeX
$$$\displaystyle \text{If } \operatorname{Antivary}(f,g) \text{ then } \sum_{i} f(i) \cdot g(i) < \sum_{i} f(i) \cdot g(σ(i)) \iff \neg \operatorname{Antivary}(f \circ σ, g).$$$
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 `g`. -/
theorem sum_smul_lt_sum_smul_comp_perm_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_smul_comp_perm_iff fun _ _ ↦ mem_univ _]
