English
The function n ↦ Roth-number for {1,...,n} is little-o of n; in other words, rothNumberNat(n) grows slower than n, i.e., rothNumberNat(n)/n → 0 as n → ∞.
Русский
Функция rotnNumberNat(n) растет медленнее чем n, то есть rothNumberNat(n)/n → 0 при n → ∞.
LaTeX
$$IsLittleO atTop (fun N ↦ (rothNumberNat N : ℝ)) (fun N ↦ (N : ℝ)).$$
Lean4
/-- **Roth's theorem** for `ℕ` as an asymptotic statement.
The maximum density of a 3AP-free set in `{1, ..., n}` goes to zero as `n` tends to infinity. -/
theorem rothNumberNat_isLittleO_id : IsLittleO atTop (fun N ↦ (rothNumberNat N : ℝ)) (fun N ↦ (N : ℝ)) :=
by
simp only [isLittleO_iff, eventually_atTop, RCLike.norm_natCast]
refine fun ε hε ↦ ⟨cornersTheoremBound (ε / 3), fun n hn ↦ ?_⟩
obtain ⟨A, hs₁, hs₂, hs₃⟩ := rothNumberNat_spec n
rw [← hs₂, ← not_lt]
exact fun hδn ↦ roth_3ap_theorem_nat ε hε hn _ hs₁ hδn.le hs₃
