FormalConjectures/ErdosProblems/489.lean

GitHub source file

4 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos489.sievedSet The set of positive integers not divisible by any element of A line 34 source

   Source documentation

   The set of positive integers not divisible by any element of A.

   no axioms what this means

   Statement uses: Set, Nat

   Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Membership.mem, Not, Dvd.dvd

   4 instances, coercions and auxiliary constants left out.

   def sievedSet (A : Set ℕ) : Set ℕ := {n : ℕ | 0 < n ∧ ∀ a ∈ A, ¬(a ∣ n)}

2. def Erdos489.GapSumSq The squared-gap sum ∑_{b_i < x} (b_{i+1} - b_i)², where b_i enumerates the positive integers not divisible by any element of A line 38 source

   Source documentation

   The squared-gap sum ∑_{b_i < x} (b_{i+1} - b_i)², where b_i enumerates the positive integers not divisible by any element of A.

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

   Statement uses: Set, Nat, Real

   Proof uses: Nat.nth, Membership.mem, Erdos489.sievedSet, Finset.sum, Finset.Iio, Nat.count, Classical.propDecidable, HPow.hPow, HSub.hSub, HAdd.hAdd, OfNat.ofNat

   17 instances, coercions and auxiliary constants left out.

   noncomputable def GapSumSq (A : Set ℕ) (x : ℕ) : ℝ :=
   …

3. theorem Erdos489.erdos_489 Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$ sorry line 58 source

   Source documentation

   Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$. Let $B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}$. If $B=\{b_1 < b_2 < \cdots\}$ then is it true that $$\lim_{x \to \infty} \frac{1}{x}\sum_{b_i < x}(b_{i+1}-b_i)^2$$ exists (and is finite)?

   For example, when $A=\{p^2: p\textrm{ prime}\}$ then $B$ is the set of squarefree numbers, and the existence of this limit was proved by Erdős.

   See also [208].

   depends on sorry what this means

   Statement uses: Iff, True, Set, Nat, Asymptotics.IsLittleO, Real, Filter.atTop, Finset.card, Finset.filter, Membership.mem, Classical.propDecidable, Finset.Icc, OfNat.ofNat, Real.sqrt, Set.Infinite, Erdos489.sievedSet, Exists, Filter.Tendsto, HDiv.hDiv, Erdos489.GapSumSq and 1 more

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

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_489 : answer(True) ↔
       ∀ (A : Set ℕ),
         (fun x : ℕ => (((Finset.Icc 1 x).filter (· ∈ A)).card : ℝ)) =o[atTop]
           (fun x : ℕ => (x : ℝ).sqrt) →
         (sievedSet A).Infinite →
         ∃ L : ℝ, Tendsto (fun x : ℕ => GapSumSq A x / (x : ℝ)) atTop (𝓝 L) := by
   …

   Mentions: Erdos489.sievedSet, Erdos489.GapSumSq

4. theorem Erdos489.erdos_489.variants.squarefree When $A = \{p^2 : p \textrm{ prime}\}$, $B$ is the set of squarefree numbers, and the existence of this limit was proved by Erdős sorry line 69 source

   Source documentation

   When $A = \{p^2 : p \textrm{ prime}\}$, $B$ is the set of squarefree numbers, and the existence of this limit was proved by Erdős. This is the $\alpha = 2$ case of Erdős Problem 145.

   depends on sorry what this means

   Statement uses: Exists, Real, Filter.Tendsto, Nat, HDiv.hDiv, Erdos489.GapSumSq, Set.ofPred, And, Nat.Prime, Eq, HPow.hPow, OfNat.ofNat, Filter.atTop, nhds

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

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_489.variants.squarefree :
       ∃ L : ℝ, Tendsto
         (fun x : ℕ => GapSumSq {n | ∃ p, Nat.Prime p ∧ n = p ^ 2} x / (x : ℝ))
         atTop (𝓝 L) := by
   …

   Mentions: Erdos489.GapSumSq