Erdős Problem 125

Reference: erdosproblems.com/125

There are four possibilities for the density of $A+B$:

1. $A+B$ has zero upper and lower density (and hence also zero density).
2. $A+B$ has zero lower density, but positive upper density (and hence no density).
3. $A+B$ has positive upper and lower density that are equal (and hence positive density).
4. $A+B$ has positive upper and lower density that are unequal (and hence no density).

theorem Erdos125.erdos_125 : False ↔ ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).HasPosDensity

Case 3: Does $A + B$ have positive upper and lower density that are equal? This is the literal interpretation of "positive density" which was falsified.

theorem Erdos125.erdos_125.variants.positive_lower_density : False ↔ 0 < ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity

Literature question: Does $A + B$ have positive lower density?

This has been falsified.

theorem Erdos125.erdos_125.variants.positive_upper_density : True ↔ 0 < ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).upperDensity

Literature question: Does $A + B$ have positive upper density?

theorem Erdos125.erdos_125.variants.zero_density : True ↔ ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).upperDensity = 0 ∧ ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity = 0

Case 1: Does $A + B$ have zero upper and lower density?

theorem Erdos125.erdos_125.variants.zero_lower_positive_upper_density : True ↔ ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity = 0 ∧ 0 < ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).upperDensity

Case 2: Does $A + B$ have zero lower density, but positive upper density?

theorem Erdos125.erdos_125.variants.positive_unequal_density : True ↔ 0 < ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity ∧ ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity < ({x : ℕ | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).upperDensity

Case 4: Does $A + B$ have positive upper and lower density that are unequal?