English
In a finitely colored commutative monoid M, for any finite subset S, there exists a positive scalar a and elements b,c with a>0 such that for all s in S, C(a•s + b) = c.
Русский
В конечно раскрашиваемом коммутативном моноиде M для любого конечного подмножества S существует положительный коэффициент a и элементы b,c такие, что для всех s∈S выполняется C(a•s + b) = c.
LaTeX
$$$\\exists a>0,\\ exists b:\\ M,\\ exists c:\\ κ,\\ ∀ s:\\ Finset\\ M, s∈S → C(a\\cdot s + b) = c.$$$
Lean4
/-- A generalization of Van der Waerden's theorem: if `M` is a finitely colored commutative
monoid, and `S` is a finite subset, then there exists a monochromatic homothetic copy of `S`. -/
theorem exists_mono_homothetic_copy {M κ : Type*} [AddCommMonoid M] (S : Finset M) [Finite κ] (C : M → κ) :
∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c := by
classical
obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ
specialize hι fun v => C <| ∑ i, v i
obtain ⟨l, c, hl⟩ := hι
set s : Finset ι := {i | l.idxFun i = none} with hs
refine ⟨#s, Finset.card_pos.mpr ⟨l.proper.choose, ?_⟩, ∑ i ∈ sᶜ, ((l.idxFun i).map ?_).getD 0, c, ?_⟩
· rw [hs, Finset.mem_filter]
exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩
· exact fun m => m
intro x xs
rw [← hl ⟨x, xs⟩]
clear hl; congr
rw [← Finset.sum_add_sum_compl s]
congr 1
· rw [← Finset.sum_const]
apply Finset.sum_congr rfl
intro i hi
rw [hs, Finset.mem_filter] at hi
rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
· apply Finset.sum_congr rfl
intro i hi
rw [hs, Finset.compl_filter, Finset.mem_filter] at hi
obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
simp [← hy, Option.map_some, Option.getD]
