FormalConjectures/ErdosProblems/442.lean

GitHub source file

6 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos442.Real.maxLogOne The function $\operatorname{Log} x := \max\{log x, 1\}$ line 38 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Real

   Proof uses: Max.max, Real.log, OfNat.ofNat

   3 instances, coercions and auxiliary constants left out.

   noncomputable def Real.maxLogOne (x : ℝ) := max x.log 1
   …

2. abbrev Erdos442.Set.bddProdUpper 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 line 51 source

   Source documentation

   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}

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Set, Nat, Real, Prod

   Proof uses: Set.ofPred, And, Membership.mem, SProd.sprod, Inter.inter, Set.Icc, OfNat.ofNat, Nat.floor, LT.lt, Prod.fst, Prod.snd

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   abbrev bddProdUpper : Set (ℕ × ℕ) :=
   …

3. instance Erdos442.Set.(instance at line 54) line 54 source
4. instance Erdos442.Set.(instance at line 57) line 57 source
5. theorem Erdos442.erdos_442 sorry line 88 source

   depends on sorry what this means

   Statement uses: Iff, False, Set, Nat, Filter.Tendsto, Real, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Erdos442.Real.maxLogOne, Finset.sum, Set.toFinset, Inter.inter, Set.Icc, Nat.floor, Filter.atTop, HPow.hPow, Prod, Erdos442.Set.bddProdUpper, Nat.lcm and 2 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   52 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

6. theorem Erdos442.erdos_442.variants.tao Tao resolved erdos_442 in the negative in Theorem 1 of https://arxiv.org/pdf/2407.04226 sorry line 113 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Exists, Set, Nat, Real, LT.lt, OfNat.ofNat, Asymptotics.IsLittleO, Filter.atTop, Filter.Eventually, And, Eq, Finset.sum, Set.toFinset, Inter.inter, Set.Icc, Nat.floor, HDiv.hDiv, Real.exp, HMul.hMul, HAdd.hAdd and 10 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   80 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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