FormalConjectures/ErdosProblems/697.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

5 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 697

Reference:

Imports (1)
Imported by 1 file
  1. theorem Erdos697.density_exists For each $m$ and $\alpha$, the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < \exp (m ^ \alpha)$ exists sorry line 39 source

    Source documentation

    For each $m$ and $\alpha$, the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < \exp (m ^ \alpha)$ exists.

    depends on sorry what this means

    Statement uses: Nat, Real, Exists, Set.HasDensity, Set.ofPred, And, Nat.ModEq, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Real.exp, HPow.hPow, Dvd.dvd, Set.univ

    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 density_exists (m : ℕ) (α : ℝ) : ∃ δ, HasDensity
    {n : ℕ | ∃ d, d ≡ 1 [MOD m] ∧ (d : ℝ) ∈ Set.Ioo 1 (exp (m ^ α)) ∧ d ∣ n} δ := by
…

    Mentions: Erdos697.δ

  2. def Erdos697.δ For each $m$ and $\alpha$, $\delta (m, \alpha)$ is the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < exp (m ^ \alpha)$ exists line 45 source

    Source documentation

    For each $m$ and $\alpha$, $\delta (m, \alpha)$ is the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < exp (m ^ \alpha)$ exists.

    depends on sorry what this means

    Statement uses: Nat, Real

    Proof uses: Exists.choose, Set.HasDensity, Set.ofPred, Exists, And, Nat.ModEq, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Real.exp, HPow.hPow, Dvd.dvd, Set.univ, Erdos697.density_exists

    14 instances, coercions and auxiliary constants left out.

    noncomputable def δ (m : ℕ) (α : ℝ) : ℝ := (density_exists m α).choose
…

    Mentions: Erdos697.density_exists

  3. theorem Erdos697.erdos_697.variants.delta_lt $\delta < \frac{m ^ \alpha + 1}{m}$ sorry line 52 source

    Source documentation

    $\delta < \frac{m ^ \alpha + 1}{m}$. This shows that $lim_{m\rightarrow\infty} \delta (m, \alpha) = 0$ for $\alpha < 1$. At $m = 0$, both sides are 0, so the strict bound requires $m > 0$. #TODO: prove this theorem.

    depends on sorry what this means

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Erdos697.δ, HDiv.hDiv, HAdd.hAdd, HPow.hPow

    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_697.variants.delta_lt (m : ℕ) (α : ℝ) (hm : 0 < m) : δ m α < (m ^ α + 1) / m := by
…

    Mentions: Erdos697.δ

  4. theorem Erdos697.erdos_697.parts.i Let $\beta = \frac{1}{\log 2}$ sorry line 58 source

    Source documentation

    Let $\beta = \frac{1}{\log 2}$. Then $lim_{m\rightarrow\infty} \delta (m, \alpha) = 0$ if $\alpha < \beta$. This is proved in [Ha92].

    depends on sorry what this means

    Statement uses: Real, LT.lt, HDiv.hDiv, OfNat.ofNat, Real.log, Nat, Filter.Tendsto, Erdos697.δ, Filter.atTop, nhds

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

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_697.parts.i {α : ℝ} (hα : α < 1 / log (2 : ℝ)) : Tendsto (δ · α) atTop (𝓝 0) := by
…

    Mentions: Erdos697.δ

  5. theorem Erdos697.erdos_697.parts.ii $lim_{m\rightarrow\infty} \delta (m, \alpha) = 1$ if $\beta < \alpha$ sorry line 64 source

    Source documentation

    $lim_{m\rightarrow\infty} \delta (m, \alpha) = 1$ if $\beta < \alpha$. This is proved in [Ha92].

    depends on sorry what this means

    Statement uses: Real, LT.lt, HDiv.hDiv, OfNat.ofNat, Real.log, Nat, Filter.Tendsto, Erdos697.δ, Filter.atTop, nhds

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

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_697.parts.ii {α : ℝ} (hα : 1 / log (2 : ℝ) < α) : Tendsto (δ · α) atTop (𝓝 1) := by
…

    Mentions: Erdos697.δ