FormalConjectures/ErdosProblems/450.lean

GitHub source file

7 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos450.HasMediumDivisor m has a divisor strictly between n and 2n line 31 source

   Source documentation

   m has a divisor strictly between n and 2n.

   no axioms what this means

   Statement uses: Nat

   Proof uses: Exists, And, LT.lt, HMul.hMul, OfNat.ofNat, Dvd.dvd

   5 instances, coercions and auxiliary constants left out.

   def HasMediumDivisor (n m : ℕ) : Prop := ∃ d : ℕ, n < d ∧ d < 2 * n ∧ d ∣ m
   …

2. def Erdos450.localCount The number of integers strictly between x and x + y with a divisor in (n, 2n) line 36 source

   Source documentation

   The number of integers strictly between x and x + y with a divisor in (n, 2n).

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

   Statement uses: Nat

   Proof uses: Finset.card, Finset.filter, Erdos450.HasMediumDivisor, Classical.propDecidable, Finset.Ioo, HAdd.hAdd

   4 instances, coercions and auxiliary constants left out.

   noncomputable def localCount (n x y : ℕ) : ℕ :=
   …

3. def Erdos450.UniformlySparse Every window (x, x+y) has at most ε y integers with a divisor in (n, 2n) line 40 source

   Source documentation

   Every window (x, x+y) has at most ε y integers with a divisor in (n, 2n).

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

   Statement uses: Real, Nat

   Proof uses: LE.le, Erdos450.localCount, HMul.hMul

   5 instances, coercions and auxiliary constants left out.

   def UniformlySparse (ε : ℝ) (n y : ℕ) : Prop := ∀ x : ℕ, (localCount n x y : ℝ) ≤ ε * (y : ℝ)

   Mentions: Erdos450.localCount

4. def Erdos450.IsSufficientScale Y ε n is a sufficient window length: for every ε > 0, all large n, and every y ≥ Y ε n, the window is ε-sparse line 44 source

   Source documentation

   Y ε n is a sufficient window length: for every ε > 0, all large n, and every y ≥ Y ε n, the window is ε-sparse.

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

   Statement uses: Real, Nat

   Proof uses: LT.lt, OfNat.ofNat, Exists, LE.le, Erdos450.UniformlySparse

   4 instances, coercions and auxiliary constants left out.

   def IsSufficientScale (Y : ℝ → ℕ → ℕ) : Prop :=
   …

5. def Erdos450.windowThreshold The least window length y₀ such that every window (x, x+y) with y ≥ y₀ is ε-sparse, or ⊤ if no such y₀ exists line 49 source

   Source documentation

   The least window length y₀ such that every window (x, x+y) with y ≥ y₀ is ε-sparse, or ⊤ if no such y₀ exists.

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

   Statement uses: Real, Nat, ENat

   Proof uses: iInf, Subtype, GE.ge, Erdos450.UniformlySparse

   11 instances, coercions and auxiliary constants left out.

   noncomputable def windowThreshold (ε : ℝ) (n : ℕ) : ℕ∞ :=
   …

6. theorem Erdos450.erdos_450 How large must $y=y(\epsilon,n)$ be such that the number of integers in $(x,x+y)$ with a divisor in $(n,2n)$ is at most $\epsilon y$? sorry line 62 source

   Source documentation

   How large must $y=y(\epsilon,n)$ be such that the number of integers in $(x,x+y)$ with a divisor in $(n,2n)$ is at most $\epsilon y$?

   The bound is required for every $x$ and every window length at least $y$, and $y(\epsilon,n)$ is the least such threshold (or $\infty$ if there is none). A linear scale $y \le C(\epsilon) n$ is known to suffice for fixed $\epsilon$ and all large $n$ (see erdos_450.linear_scale_suffices).

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Nat, Eq, ENat, Erdos450.windowThreshold, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   8 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_450 (ε : ℝ) (hε : 0 < ε) (n : ℕ) : windowThreshold ε n = answer(sorry) := by
   …

   Mentions: Erdos450.windowThreshold

7. theorem Erdos450.erdos_450.linear_scale_suffices A translate-uniform linear scale suffices: there is a sufficient window length Y with Y ε n ≤ C(ε) · n sorry line 71 source

   Source documentation

   A translate-uniform linear scale suffices: there is a sufficient window length Y with Y ε n ≤ C(ε) · n. This is an upper bound on the optimal scale, not the exact threshold asked for in erdos_450.

   depends on sorry what this means

   Statement uses: Exists, Real, Nat, And, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, Erdos450.IsSufficientScale

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

   17 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_450.linear_scale_suffices :
       ∃ Y : ℝ → ℕ → ℕ,
         (∀ ε : ℝ, 0 < ε → ∃ C : ℝ, ∀ n : ℕ, (Y ε n : ℝ) ≤ C * n) ∧ IsSufficientScale Y := by
   …

   Mentions: Erdos450.IsSufficientScale