English
Equality case for antivary rearrangements: sum with f i smul g i equals sum with f i smul g (σ i) iff antivary holds for f and g ∘ σ on s.
Русский
Равенство в случае antivary: сумма с f_i smul g_i равна сумме с f_i smul g(σ_i), если antivary выполняется для f и g ∘ σ на s.
LaTeX
$$$$ \sum_i f(i) \cdot g(i) = \sum_i f(i) \cdot g(σ(i)) \iff \text{Antivary}(f, g) \text{ on } s $$$$
Lean4
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which monovary together on `s`, is unchanged by a permutation if and only if `f` and `g ∘ σ`
monovary together on `s`. Stated by permuting the entries of `g`. -/
theorem sum_smul_comp_perm_eq_sum_smul_iff (hfg : MonovaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ σ) s := by
classical
refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm ?_⟩
· rw [MonovaryOn] at h
push_neg at h
obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
set τ : Perm ι := (Equiv.swap x y).trans σ
have hτs : {x | τ x ≠ x} ⊆ s :=
by
refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
obtain rfl | hxy := eq_or_ne x y
· cases lt_irrefl _ hfxy
simp only [τ, ← s.sum_erase_add _ hx, ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩), add_assoc,
Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le (smul_add_smul_lt_smul_add_smul hfxy hgxy)
simp_rw [mem_erase] at hz
rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
· convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1
simp_rw [Function.comp_apply, apply_inv_self]
