erdos_442.variants.tao

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 $$

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.