FormalConjectures/ErdosProblems/538.lean

GitHub source file

6 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos538.representations The representations m = p * a with p prime and a ∈ A line 34 source

   Source documentation

   The representations m = p * a with p prime and a ∈ A.

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

   Statement uses: Finset, Nat, Prod

   Proof uses: Finset.filter, And, Nat.Prime, Prod.fst, Eq, HMul.hMul, Prod.snd, SProd.sprod, Finset.range, HAdd.hAdd, OfNat.ofNat

   9 instances, coercions and auxiliary constants left out.

   def representations (A : Finset ℕ) (m : ℕ) : Finset (ℕ × ℕ) :=
   …

2. def Erdos538.Admissible A ⊆ {1, …, N} and every m has at most r representations m = p a line 38 source

   Source documentation

   A ⊆ {1, …, N} and every m has at most r representations m = p a.

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

   Statement uses: Nat, Finset

   Proof uses: And, Membership.mem, LE.le, OfNat.ofNat, Finset.card, Prod, Erdos538.representations

   4 instances, coercions and auxiliary constants left out.

   def Admissible (r N : ℕ) (A : Finset ℕ) : Prop :=
   …

3. def Erdos538.reciprocalMass The reciprocal sum ∑_{n ∈ A} 1/n of the problem line 42 source

   Source documentation

   The reciprocal sum ∑_{n ∈ A} 1/n of the problem.

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

   Statement uses: Finset, Nat, Rat

   Proof uses: Finset.sum, HDiv.hDiv, OfNat.ofNat

   6 instances, coercions and auxiliary constants left out.

   def reciprocalMass (A : Finset ℕ) : ℚ := ∑ a ∈ A, (1 : ℚ) / a

4. def Erdos538.maxMass The largest reciprocal sum ∑_{n ∈ A} 1/n over admissible A ⊆ {1, …, N} line 45 source

   Source documentation

   The largest reciprocal sum ∑_{n ∈ A} 1/n over admissible A ⊆ {1, …, N}.

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

   Statement uses: Nat, Real

   Proof uses: SupSet.sSup, Set.image, Finset, Erdos538.reciprocalMass, Set.ofPred, Erdos538.Admissible

   3 instances, coercions and auxiliary constants left out.

   noncomputable def maxMass (r N : ℕ) : ℝ :=
   …

5. theorem Erdos538.erdos_538 Let $r\geq 2$ and suppose that $A\subseteq\{1,\ldots,N\}$ is such that, for any $m$, there are at most $r$ solutions to $m=pa$ where $p$ is prime and $a\in A$ sorry line 59 source

   Source documentation

   Let $r\geq 2$ and suppose that $A\subseteq\{1,\ldots,N\}$ is such that, for any $m$, there are at most $r$ solutions to $m=pa$ where $p$ is prime and $a\in A$. Give the best possible upper bound for $\sum_{n\in A}\frac{1}{n}$.

   Erdős observed that $\sum_{n\in A}\frac{1}{n}\ll r\frac{\log N}{\log\log N}$, and the order Θ_r(log N / loglog N) is known (see erdos_538.matching_order). The best possible upper bound is the asymptotic size of the largest reciprocal sum maxMass r N over admissible A.

   depends on sorry what this means

   Statement uses: Nat, Real, sorryAx, Bool.false, LE.le, OfNat.ofNat, Asymptotics.IsEquivalent, Filter.atTop, Erdos538.maxMass

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_538 :
       let f : ℕ → ℕ → ℝ := answer(sorry)
   …

6. theorem Erdos538.erdos_538.matching_order The reciprocal sum has matching order Θ_r(log N / loglog N): an explicit upper bound for every admissible A, together with a witnessing construction achieving the same order sorry line 71 source

   Source documentation

   The reciprocal sum has matching order Θ_r(log N / loglog N): an explicit upper bound for every admissible A, together with a witnessing construction achieving the same order. This pins the order (up to the one iterated-logarithm factor) but not the best possible upper bound asked for in erdos_538.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, And, Finset, Erdos538.Admissible, Real, HMul.hMul, Real.log, HAdd.hAdd, Erdos538.reciprocalMass, Exists, Nat.log

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

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_538.matching_order (r N : ℕ) (hr : 2 ≤ r) (hN : 2 ≤ N) :
       (∀ A : Finset ℕ, Admissible r N A →
         Real.log (Real.log (N + 1)) * (reciprocalMass A : ℝ) ≤
           2 * r * (1 + Real.log (N * N))) ∧
       (∃ A : Finset ℕ, Admissible r N A ∧
         Real.log (N + 1) ≤
           4 + (8192 * (Nat.log 2 (Nat.log 2 N) + 1) : ℝ) * (reciprocalMass A : ℝ)) := by
   …

   Mentions: Erdos538.Admissible, Erdos538.reciprocalMass