FormalConjectures/ErdosProblems/145.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 145

Reference: erdosproblems.com/145

Imports (1)
  1. abbrev Erdos145.s Let $s_1 < s_2 < \cdots$ be the sequence of squarefree numbers line 34 source

    Source documentation

    Let $s_1 < s_2 < \cdots$ be the sequence of squarefree numbers.

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

    Statement uses: Nat

    Proof uses: Nat.nth, Squarefree

    1 instances, coercions and auxiliary constants left out.

    noncomputable abbrev s (n : ℕ) : ℕ := Nat.nth Squarefree n
  2. abbrev Erdos145.A Let $A(x)$ denote the set of indices $n$ for which $s_n \leq x$ line 37 source

    Source documentation

    Let $A(x)$ denote the set of indices $n$ for which $s_n \leq x$.

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

    Statement uses: Real, Finset, Nat

    Proof uses: Finset.preimage, Finset.Icc, OfNat.ofNat, Nat.floor, Erdos145.s

    10 instances, coercions and auxiliary constants left out.

    noncomputable abbrev A (x : ℝ) : Finset ℕ :=
…
  3. theorem Erdos145.erdos_145 Let $s_1 < s_2 < \cdots$ be the sequence of squarefree numbers sorry line 49 source

    Source documentation

    Let $s_1 < s_2 < \cdots$ be the sequence of squarefree numbers. Is it true that, for any $\alpha\geq 0$, $$ \lim_{x\to\infty} \frac{1}{x}\sum_{s_n\leq x}(s_{n+1}-s_n)^\alpha $$ exists?

    depends on sorry what this means

    Statement uses: Iff, True, Real, GE.ge, OfNat.ofNat, Exists, Filter.Tendsto, HMul.hMul, HDiv.hDiv, Finset.sum, Nat, Erdos145.A, HPow.hPow, HSub.hSub, Erdos145.s, HAdd.hAdd, Filter.atTop, nhds

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

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_145 :
    answer(sorry) ↔ ∀ α ≥ (0 : ℝ), ∃ β : ℝ,
      atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β) := by
…

    Mentions: Erdos145.A, Erdos145.s

  4. theorem Erdos145.erdos_145.variants.le_two Erdős [Er51] proved this for all $0\leq \alpha\leq 2$ sorry line 61 source

    Source documentation

    Erdős [Er51] proved this for all $0\leq \alpha\leq 2$.

    [Er51] Erdös, P., Some problems and results in elementary number theory. Publ. Math. Debrecen (1951), 103-109.

    depends on sorry what this means

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, Nat, Exists, Filter.Tendsto, HMul.hMul, HDiv.hDiv, Finset.sum, Erdos145.A, HPow.hPow, HSub.hSub, Erdos145.s, HAdd.hAdd, Filter.atTop, nhds

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

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_145.variants.le_two {α : ℝ} (hα : α ∈ Set.Icc 0 2) :
    ∃ β : ℝ,
      atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β) := by
…

    Mentions: Erdos145.A, Erdos145.s

  5. theorem Erdos145.erdos_145.variants.le_three Hooley [Ho73] extended this to all $0 \leq \alpha\leq 3$ sorry line 72 source

    Source documentation

    Hooley [Ho73] extended this to all $0 \leq \alpha\leq 3$.

    [Ho73] Hooley, Christopher, On the intervals between consecutive terms of sequences. Proc. Symp. Pure Math, vol. 24, pp. 129-140. 1973.

    depends on sorry what this means

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, Nat, Exists, Filter.Tendsto, HMul.hMul, HDiv.hDiv, Finset.sum, Erdos145.A, HPow.hPow, HSub.hSub, Erdos145.s, HAdd.hAdd, Filter.atTop, nhds

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

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_145.variants.le_three {α : ℝ} (hα : α ∈ Set.Icc 0 3) :
    ∃ β : ℝ,
      atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β) := by
…

    Mentions: Erdos145.A, Erdos145.s

  6. theorem Erdos145.erdos_145.variants.lt_eleven_thirds Greaves, Harman, and Huxley showed (in Chapter 11 of [GHH97]) that this is true for $0 \leq \alpha < 11/3$ sorry line 85 source

    Source documentation

    Greaves, Harman, and Huxley showed (in Chapter 11 of [GHH97]) that this is true for $0 \leq \alpha < 11/3$.

    [GHH97] Greaves, G. R. H. and Harman, G. and Huxley, M. N., Sieve Methods, Exponential Sums, and their Applications in Number Theory. (1997).

    depends on sorry what this means

    Statement uses: Real, Membership.mem, Set, Set.Ico, OfNat.ofNat, HDiv.hDiv, Nat, Exists, Filter.Tendsto, HMul.hMul, Finset.sum, Erdos145.A, HPow.hPow, HSub.hSub, Erdos145.s, HAdd.hAdd, Filter.atTop, nhds

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

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_145.variants.lt_eleven_thirds {α : ℝ} (hα : α ∈ Set.Ico 0 (11 / 3)) :
    ∃ β : ℝ,
      atTop.Tendsto (fun x : ℝ ↦ 1 / x * ∑ n ∈ A x, (s (n + 1) - s n : ℝ) ^ α) (𝓝 β) := by
…

    Mentions: Erdos145.A, Erdos145.s