Skip to content

Erdős problem 143

Start work

Does this imply that lim inf⁡∣A∩[1,x]∣x=0? \liminf \frac{|A \cap [1,x]|}{x} = 0?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

143.lean

Retained formal statement2 of 2

Or ∑x∈A1xlog⁡x<∞, \sum_{x \in A} \frac{1}{x \log x} < \infty,

FormalConjectures/ErdosProblems/143.leanErdos143.erdos_143.parts.ii1 lineExact file
∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Summable fun x => 1 / (↑x * Real.log ↑x)
OpenStatement only, no proof