Skip to content

Erdős problem 1145

Start work

Let A={1≤a1<a2<⋯ }A=\{1\leq a_1 < a_2 < \cdots\} and B={1≤b1<b2<⋯ }B=\{1\leq b_1 < b_2 < \cdots\} be sets of integers with an/bn→1a_n/b_n\to 1.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1145.lean

Retained formal statement2 of 2

A stronger form of [erdosproblems.com/28].

FormalConjectures/ErdosProblems/1145.leanErdos1145.erdos_1145.test_implies_erdos_282 linesExact file
Erdos1145.Erdos1145Prop →  ∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤
TestStatement only, no proof