English
For AntivaryOn f g on s, the strict inequality ∑ f(i)•g(σ(i)) < ∑ f(i)•g(i) holds exactly when ¬Monovary (f ∘ σ) g on s.
Русский
Для AntivaryOn f g на s верно строгое неравенство ∑ f(i)g(σ(i)) < ∑ f(i)g(i) тогда, когда не выполняется Monovary (f∘σ) g на s.
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{MonovaryOn}(f \circ σ, g, s).$$$
Lean4
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which monovary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together. Stated by permuting the entries of `g`. -/
theorem sum_comp_perm_smul_lt_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_lt_sum_smul_iff fun _ _ ↦ mem_univ _]
