Skip to content

Erdős problem 741

Start work

Let A⊆NA\subseteq \mathbb{N} be such that A+AA+A has positive density in the literal sense that its natural density exists and is positive. Can one always decompose A=A1⊔A2A=A_1\sqcup A_2 such that A1+A1A_1+A_1 and A2+A2A_2+A_2 both have positive density in this sense?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

741.lean

Retained formal statement4 of 4

Let A⊆NA\subseteq \mathbb{N} be such that A+AA+A has positive lower density. Can one always decompose A=A1⊔A2A=A_1\sqcup A_2 such that A1+A1A_1+A_1 and A2+A2A_2+A_2 both have positive lower density?

FormalConjectures/ErdosProblems/741.leanErdos741.erdos_741.variants.lower4 linesExact file
True ↔  ∀ (A : Set ℕ),    0 < (A + A).lowerDensity →      ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).lowerDensity ∧ 0 < (A₂ + A₂).lowerDensity
OpenStatement only, no proof