FormalConjectures/ErdosProblems/1190.lean

GitHub source file

6 declarations, 5 contain sorry, 0 declared as axioms

1. def Erdos1190.eps Documented declaration: eps line 44 source

   Source documentation

   $\epsilon_m$ is the supremum of $\sum \frac{1}{n_i}$ over all finite sequences $m<n_1<\cdots<n_k$ for which there exist congruences $a_i\pmod{n_i}$ such that no integer satisfies two such congruences.

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

   Statement uses: Nat, Real

   Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, Int, And, Membership.mem, LT.lt, Ne, Not, Int.ModEq, Eq, Finset.sum, Inv.inv

   9 instances, coercions and auxiliary constants left out.

   noncomputable def eps (m : ℕ) : ℝ :=
   …

2. theorem Erdos1190.erdos_1190 Documented declaration: erdos_1190 sorry line 62 source

   Source documentation

   Let $$\epsilon_m=\max \sum \frac{1}{n_i}$$ where the maximum is taken over all finite sequences $m<n_1<\cdots<n_k$ for which there exist congruences $a_i\pmod{n_i}$ such that no integer satisfies two such congruences.

   Estimate $\epsilon_m$.

   The resolution of [202] by GPT-5.4 Pro implies via the same reduction that $$\epsilon_m=L(m)^{-1+o(1)},$$ where $L(m)=\exp(\sqrt{\log m\log\log m})$.

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, And, HPow.hPow, scaleL, HSub.hSub, Neg.neg, Erdos1190.eps, HAdd.hAdd, Filter.atTop

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

   27 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1190 : ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
       scaleL m ^ (-1 - ε : ℝ) < eps m ∧ eps m < scaleL m ^ (-1 + ε : ℝ) := by
   …

   Mentions: scaleL, Erdos1190.eps

3. theorem Erdos1190.erdos_1190.variants.lt_one Erdős [Er80] seems to credit Mirsky and Newman with the result that $\epsilon_m<1$, but gives no reference sorry line 71 source

   Source documentation

   Erdős [Er80] seems to credit Mirsky and Newman with the result that $\epsilon_m<1$, but gives no reference.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Int, Membership.mem, LT.lt, Ne, Not, Exists, And, Int.ModEq, Real, Finset.sum, Inv.inv

   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_1190.variants.lt_one (m : ℕ) (hm : 1 ≤ m) (S : Finset ℕ) (a : ℕ → ℤ)
       (hS : ∀ n ∈ S, m < n)
       (hdisj : ∀ n ∈ S, ∀ n' ∈ S, n ≠ n' → ¬ ∃ x : ℤ, x ≡ a n [ZMOD n] ∧ x ≡ a n' [ZMOD n']) :
       (∑ n ∈ S, (n : ℝ)⁻¹) < 1 := by
   …

4. theorem Erdos1190.erdos_1190.variants.tendsto_zero He could not even decide whether $\epsilon_m\to 0$ as $m\to \infty$ sorry line 81 source

   Source documentation

   He could not even decide whether $\epsilon_m\to 0$ as $m\to \infty$.

   depends on sorry what this means

   Statement uses: Filter.Tendsto, Nat, Real, Erdos1190.eps, Filter.atTop, nhds, OfNat.ofNat

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

   13 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1190.variants.tendsto_zero : Tendsto eps atTop (𝓝 0) := by
   …

   Mentions: Erdos1190.eps

5. theorem Erdos1190.erdos_1190.variants.lower_bound The work of de la Bretèche, Ford, and Vandehey [BFV13] implies $$L(m)^{-1+o(1)}< \epsilon_m < L(m)^{-\sqrt{3}/2+o(1)},$$ where $L(m)=\exp(\sqrt{\log m\log\log m})$ sorry line 90 source

   Source documentation

   The work of de la Bretèche, Ford, and Vandehey [BFV13] implies $$L(m)^{-1+o(1)}< \epsilon_m < L(m)^{-\sqrt{3}/2+o(1)},$$ where $L(m)=\exp(\sqrt{\log m\log\log m})$. The lower bound is implicit in their construction.

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, HPow.hPow, scaleL, HSub.hSub, Neg.neg, Erdos1190.eps, Filter.atTop

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

   23 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1190.variants.lower_bound : ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
       scaleL m ^ (-1 - ε : ℝ) < eps m := by
   …

   Mentions: scaleL, Erdos1190.eps

6. theorem Erdos1190.erdos_1190.variants.upper_bound The work of de la Bretèche, Ford, and Vandehey [BFV13] implies $$L(m)^{-1+o(1)}< \epsilon_m < L(m)^{-\sqrt{3}/2+o(1)},$$ where $L(m)=\exp(\sqrt{\log m\log\log m})$ sorry line 101 source

   Source documentation

   The work of de la Bretèche, Ford, and Vandehey [BFV13] implies $$L(m)^{-1+o(1)}< \epsilon_m < L(m)^{-\sqrt{3}/2+o(1)},$$ where $L(m)=\exp(\sqrt{\log m\log\log m})$. The upper bound follows immediately from their upper bound as reported in [202] and partial summation.

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Erdos1190.eps, HPow.hPow, scaleL, HAdd.hAdd, Neg.neg, HDiv.hDiv, Real.sqrt, Filter.atTop

   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_1190.variants.upper_bound : ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
       eps m < scaleL m ^ (-(sqrt 3 / 2) + ε : ℝ) := by
   …

   Mentions: Erdos1190.eps, scaleL