Erdős problem 337
Let be an additive basis (of any finite order) such that . Is it true that
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/337.leanFalse ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasis → ((fun N => ↑(A ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => ↑N) → Filter.Tendsto (fun N => ↑((A + A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop Filter.atTopProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:337 - PLBY Lean proofs
ErdosProblems.Erdos337
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine