Erdős Problem 442

Reference: erdosproblems.com/442

noncomputable def Erdos442.Real.maxLogOne (x : ℝ) : ℝ

The function $\operatorname{Log} x := \max\{log x, 1\}$.

Equations

• Erdos442.Real.maxLogOne x = max (Real.log x) 1

@[reducible, inline]

abbrev Erdos442.Set.bddProdUpper (A : Set ℕ) (x : ℝ) : Set (ℕ × ℕ)

If A be a set of natural numbers and let x be real, then A.bddProdUpper x is the finite upper-triangular set of pairs of elements of A that are ≤ x. Specifically, it is the set {(n, m) | n ∈ A, n ≤ x, m ∈ A, m ≤ x, n < m}

Equations

• Erdos442.Set.bddProdUpper A x = {y : ℕ × ℕ | y ∈ A.interIcc 1 ⌊x⌋₊ ×ˢ A.interIcc 1 ⌊x⌋₊ ∧ y.1 < y.2}

noncomputable instance Erdos442.Set.instFintypeElemProdNatBddProdUpper (A : Set ℕ) (x : ℝ) : Fintype ↑(bddProdUpper A x)

Equations

• Erdos442.Set.instFintypeElemProdNatBddProdUpper A x = ⋯.fintype

theorem Erdos442.erdos_442 : (∀ (A : Set ℕ), Filter.Tendsto (fun (x : ℝ) => 1 / Real.maxLogOne (Real.maxLogOne x) * ∑ n ∈ (A.interIcc 1 ⌊x⌋₊).toFinset, 1 / ↑n) Filter.atTop Filter.atTop → Filter.Tendsto (fun (x : ℝ) => 1 / (∑ n ∈ (A.interIcc 1 ⌊x⌋₊).toFinset, 1 / ↑n) ^ 2 * ∑ nm ∈ (Set.bddProdUpper A x).toFinset, 1 / ↑(nm.1.lcm nm.2)) Filter.atTop Filter.atTop) ↔ True

Let $\operatorname{Log} x := \max\{\log x, 1\}$, $\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x)$, and $\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)).$ Is it true that if $A\subseteq\mathbb{N}$ is such that $$ \frac{1}{\operatorname{Log}_2 x} \sum_{n\in A: n\leq x} \frac{1}{n}\to\infty $$ then $$ \left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2 \sum_{n, m \in A: n < m \leq x} \frac{1}{\operatorname{lcm}(n, m)}\to\infty $$ as $x\to\infty$?

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

theorem Erdos442.erdos_442.variants.tao : ∃ (A : Set ℕ) (f : ℝ → ℝ) (C : ℝ) (_ : 0 < C) (_ : f =o[Filter.atTop] 1), ∀ (x : ℝ), ∑ n ∈ (A.interIcc 1 ⌊x⌋₊).toFinset, 1 / ↑n = Real.exp ((1 / 2 + f x) * √(Real.maxLogOne (Real.maxLogOne x)) * Real.maxLogOne (Real.maxLogOne (Real.maxLogOne x))) ∧ |∑ nm ∈ (A.interIcc 1 ⌊x⌋₊ ×ˢ A.interIcc 1 ⌊x⌋₊).toFinset, 1 / ↑(nm.1.lcm nm.2)| ≤ C * (∑ n ∈ (A.interIcc 1 ⌊x⌋₊).toFinset, 1 / ↑n) ^ 2

Tao resolved erdos_442 in the negative in Theorem 1 of https://arxiv.org/pdf/2407.04226. The following is a formalisation of that theorem with $C_0 = 1$.

Let $\operatorname{Log} x := \max\{\log x, 1\}$, $\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x)$, and $\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)).$ There exists a set $A$ of natural numbers such that $$ \sum_{n\in A: n\leq x} \frac{1}{n} = \exp\left(\left(\left(\frac{1}{2} + o(1)\right)\operatorname{Log}_2^{1/2}x \operatorname{Log}_3x\right)\right) $$ and $$ \sum_{n, m\in A: n, m\leq x} \frac{1}{\operatorname{lcm}(n, m)}\ll\left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2 $$