English
For any Multiset s of α and n ∈ ℕ, the element (sum s)^(|s| n + 1) lies in the span of the set { x^(n+1) | x ∈ s }.
Русский
Для любого мультимножества s над α и натурального n, (sum s)^(|s| n + 1) принадлежит span{ x^(n+1) | x ∈ s }.
LaTeX
$$$\\big(\\sum_{x \\in s} x\\big)^{|s|\\,n + 1} \\in \\operatorname{span}\\{ x^{n+1} \\mid x \\in s \\}$$$
Lean4
theorem pow_multiset_sum_mem_span_pow [DecidableEq α] (s : Multiset α) (n : ℕ) :
s.sum ^ (Multiset.card s * n + 1) ∈ span ((s.map fun (x : α) ↦ x ^ (n + 1)).toFinset : Set α) :=
by
induction s using Multiset.induction_on with
| empty => simp
| cons a s hs => ?_
simp only [Finset.coe_insert, Multiset.map_cons, Multiset.toFinset_cons, Multiset.sum_cons, Multiset.card_cons,
add_pow]
refine Submodule.sum_mem _ ?_
intro c _hc
rw [mem_span_insert]
by_cases h : n + 1 ≤ c
· refine
⟨a ^ (c - (n + 1)) * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) * ((Multiset.card s + 1) * n + 1).choose c, 0,
Submodule.zero_mem _, ?_⟩
rw [mul_comm _ (a ^ (n + 1))]
simp_rw [← mul_assoc]
rw [← pow_add, add_zero, add_tsub_cancel_of_le h]
· use 0
simp_rw [zero_mul, zero_add]
refine ⟨_, ?_, rfl⟩
replace h : c ≤ n := Nat.lt_succ_iff.mp (not_le.mp h)
have : (Multiset.card s + 1) * n + 1 - c = Multiset.card s * n + 1 + (n - c) := by
rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]
rw [this, pow_add]
simp_rw [mul_assoc, mul_comm (s.sum ^ (Multiset.card s * n + 1)), ← mul_assoc]
exact mul_mem_left _ _ hs
