Erdős problem 442
Let , , and Is it true that if is such that then as ?
Sources
FormalConjectures/ErdosProblems/
442.lean
Retained formal statement
Let , , and Is it true that if is such that then as ?
Tao [Ta24b] has shown this is false.
[Ta24b] Tao, T., _Dense sets of natural numbers with unusually large least common multiples_. arXiv:2407.04226 (2024).
Note: the informal and formal statements follow the solution paper https://arxiv.org/pdf/2407.04226
False ↔ ∀ (A : Set ℕ), Filter.Tendsto (fun x => 1 / Erdos442.Real.maxLogOne (Erdos442.Real.maxLogOne x) * ∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) Filter.atTop Filter.atTop → Filter.Tendsto (fun x => 1 / (∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) ^ 2 * ∑ nm ∈ (Erdos442.Set.bddProdUpper A x).toFinset, 1 / ↑(nm.1.lcm nm.2)) Filter.atTop Filter.atTopSolvedStatement only, no proof