English
Roth number is subadditive: rothNumberNat(M+N) ≤ rothNumberNat(M) + rothNumberNat(N).
Русский
Число Рота субаддитивно: rothNumberNat(M+N) ≤ rothNumberNat(M) + rothNumberNat(N).
LaTeX
$$$\\operatorname{rothNumberNat}(M+N) \\le \\operatorname{rothNumberNat}(M) + \\operatorname{rothNumberNat}(N).$$$
Lean4
/-- The Roth number is a subadditive function. Note that by Fekete's lemma this shows that
the limit `rothNumberNat N / N` exists, but Roth's theorem gives the stronger result that this
limit is actually `0`. -/
theorem rothNumberNat_add_le (M N : ℕ) : rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N :=
by
simp_rw [rothNumberNat_def]
rw [range_add_eq_union, ← addRothNumber_map_add_left (range N) M]
exact addRothNumber_union_le _ _
