Erdős Problem 442

Reference: erdosproblems.com/442

def Real.maxLogOne (x : ℝ) : ℝ

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

Equations

• x.maxLogOne = Real.log x ⊔ 1

def Set.instFintypeElemNatInterIccOfNatFloorReal_formalConjectures (A : Set ℕ) (x : ℝ) : Fintype ↑(A ∩ Icc 1 ⌊x⌋₊)

Equations

• A.instFintypeElemNatInterIccOfNatFloorReal_formalConjectures x = ⋯.fintype

theorem erdos_442 : (∀ (A : Set ℕ), Filter.Tendsto (fun (x : ℝ) => 1 / x.maxLogOne.maxLogOne * ∑ n ∈ Set.bdd✝ A x, 1 / ↑n) Filter.atTop Filter.atTop → Filter.Tendsto (fun (x : ℝ) => 1 / (∑ n ∈ Set.bdd✝ A x, 1 / ↑n) ^ 2 * ∑ nm ∈ Set.bddProdUpper✝ A x, 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 erdos_442.variants.tao : ∃ (A : Set ℕ) (f : ℝ → ℝ) (C : ℝ) (_ : 0 < C) (_ : Filter.Tendsto f Filter.atTop (nhds 0)), ∀ (x : ℝ), ∑ n ∈ Set.bdd✝ A x, 1 / ↑n = Real.exp ((1 / 2 + f x) * √x.maxLogOne.maxLogOne * x.maxLogOne.maxLogOne.maxLogOne) ∧ |∑ nm ∈ Set.bdd✝ A x ×ˢ Set.bdd✝ A x, 1 / ↑(nm.1.lcm nm.2)| ≤ C * (∑ n ∈ Set.bdd✝ A x, 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 $$