Erdős problem 355
Is there a lacunary sequence (so that and there exists some such that for all ) such that contain all rationals in some open interval?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/355.leanTrue ↔ ∃ A, IsLacunary A ∧ ∃ u v, u < v ∧ ∀ (q : ℚ), ↑q ∈ Set.Ioo u v → q ∈ {x | ∃ A', ∃ (_ : ↑A' ⊆ Set.range A), ∑ a ∈ A', 1 / ↑a = x}Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:355 - PLBY Lean proofs
ErdosProblems.Erdos355
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine