English
For f,g monotone on a finite set s, the sum with f_i·g_i after permuting g by σ is equal to the original sum iff g is rearranged compatibly with σ in a monovariant way on s.
Русский
Для функций f,g монотонных на конечном множестве s сумма после перестановки g остаётся равной исходной сумме тогда и только если g перестраивается совместимо с σ в монотонном отношении на s.
LaTeX
$$$$ \sum_{i \in s} f(i) \; g(\sigma(i)) = \sum_{i \in s} f(i) \; g(i) \quad \Longleftrightarrow \; \text{MonovaryOn}(f, g \circ \sigma, s) $$$$
Lean4
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is maximized when
`f` and `g` monovary together on `s`. Stated by permuting the entries of `g`. -/
theorem sum_smul_comp_perm_le_sum_smul (hfg : MonovaryOn f g s) (hσ : {x | σ x ≠ x} ⊆ s) :
∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i := by
classical
revert hσ σ hfg
apply
Finset.induction_on_max_value (fun i ↦ toLex (g i, f i)) (p := fun t ↦
∀ {σ : Perm ι}, MonovaryOn f g t → {x | σ x ≠ x} ⊆ t → ∑ i ∈ t, f i • g (σ i) ≤ ∑ i ∈ t, f i • g i) s
· simp only [le_rfl, Finset.sum_empty, imp_true_iff]
intro a s has hamax hind σ hfg hσ
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
have hτs : {x | τ x ≠ x} ⊆ s := by
intro x hx
simp only [τ, Ne, Set.mem_setOf_eq, Equiv.swap_comp_apply] at hx
split_ifs at hx with h₁ h₂
· obtain rfl | hax := eq_or_ne x a
· contradiction
· exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
· exact (hx <| σ.injective h₂.symm).elim
· exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
specialize hind (hfg.subset <| subset_insert _ _) hτs
simp_rw [sum_insert has]
grw [← hind]
obtain hσa | hσa := eq_or_ne a (σ a)
· rw [hτ, ← hσa, swap_self, trans_refl]
have h1s : σ⁻¹ a ∈ s := by
rw [Ne, ← inv_eq_iff_eq] at hσa
refine mem_of_mem_insert_of_ne (hσ fun h ↦ hσa ?_) hσa
rwa [apply_inv_self, eq_comm] at h
simp only [← s.sum_erase_add _ h1s, add_comm]
rw [← add_assoc, ← add_assoc]
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_inv_self]
refine add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le
· specialize hamax (σ⁻¹ a) h1s
rw [Prod.Lex.toLex_le_toLex] at hamax
rcases hamax with hamax | hamax
· exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
· exact hamax.2
· specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
rw [Prod.Lex.toLex_le_toLex] at hamax
rcases hamax with hamax | hamax
· exact hamax.le
· exact hamax.1.le
· rw [mem_erase, Ne, eq_inv_iff_eq] at hx
rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
rintro rfl
exact has hx.2
