FormalConjectures/ErdosProblems/400.lean

GitHub source file

5 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos400.g For any $k\geq 2$ let $g_k(n)$ denote the maximum value of $(a_1+\cdots+a_k)-n$ where $a_1,\ldots,a_k$ are integers such that $a_1!\cdots a_k! \mid n!$ line 37 source

   Source documentation

   For any $k\geq 2$ let $g_k(n)$ denote the maximum value of $(a_1+\cdots+a_k)-n$ where $a_1,\ldots,a_k$ are integers such that $a_1!\cdots a_k! \mid n!$.

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

   Statement uses: Nat

   Proof uses: SupSet.sSup, Set.ofPred, Exists, Fin, Dvd.dvd, Finset.prod, Finset.univ, Nat.factorial, Eq, HSub.hSub, Finset.sum

   7 instances, coercions and auxiliary constants left out.

   noncomputable def g (k n : ℕ) : ℕ :=
   …

2. theorem Erdos400.erdos_400.parts.i Can one show that $\sum_{n\leq x}g_k(n) \sim c_k x\log x$ for some constant $c_k$? sorry line 44 source

   Source documentation

   Can one show that $\sum_{n\leq x}g_k(n) \sim c_k x\log x$ for some constant $c_k$?

   depends on sorry what this means

   Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Exists, Real, Asymptotics.IsEquivalent, Filter.atTop, Finset.sum, Finset.Icc, Erdos400.g, HMul.hMul, Real.log

   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_400.parts.i :
       answer(sorry) ↔ ∀ᵉ (k ≥ 2), ∃ c : ℝ,
         (fun x : ℕ ↦ (∑ n ∈ Icc 1 x, (g k n : ℝ))) ~[atTop]
         (fun x : ℕ ↦ c * x * Real.log x) := by
   …

   Mentions: c, Erdos400.g

3. theorem Erdos400.erdos_400.parts.ii Is it true that there is a constant $c_k$ such that for almost all $n < x$ we have $g_k(n)=c_k\log x+o(\log x)$? sorry line 55 source

   Source documentation

   Is it true that there is a constant $c_k$ such that for almost all $n < x$ we have $g_k(n)=c_k\log x+o(\log x)$?

   depends on sorry what this means

   Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Exists, Real, GT.gt, Filter.Tendsto, HDiv.hDiv, Finset.card, Finset.filter, LE.le, abs, HSub.hSub, Erdos400.g, HMul.hMul, Real.log, Finset.Icc, Filter.atTop and 1 more

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

   50 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_400.parts.ii :
       answer(sorry) ↔ ∀ᵉ (k ≥ 2), ∃ c : ℝ, ∀ ε > 0,
         Tendsto (fun x : ℕ ↦
           (((Icc 1 x).filter (fun n ↦
             |(g k n : ℝ) - c * Real.log x| ≤ ε * Real.log x)).card : ℝ) / x)
           atTop (𝓝 1) := by
   …

   Mentions: c, Erdos400.g

4. theorem Erdos400.erdos_400.variants.upper_bound Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown sorry line 68 source

   Source documentation

   Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown.

   depends on sorry what this means

   Statement uses: Nat, GE.ge, OfNat.ofNat, Asymptotics.IsBigO, Real, Filter.atTop, Erdos400.g, Real.log

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

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_400.variants.upper_bound (k : ℕ) (hk : k ≥ 2) :
       (fun n : ℕ ↦ (g k n : ℝ)) ≪ (fun n : ℕ ↦ Real.log (n : ℝ)) := by
   …

   Mentions: Erdos400.g

5. theorem Erdos400.erdos_400.variants.g_pos For $k \ge 2$, $g_k(n) > 0$ line 75 source

   Source documentation

   For $k \ge 2$, $g_k(n) > 0$. We show this by choosing $a = (n, 1, 0, \ldots, 0)$.

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

   Statement uses: Nat, GE.ge, OfNat.ofNat, LT.lt, Erdos400.g

   Proof uses: Eq, HAdd.hAdd, Exists, Exists.intro, HSub.hSub, Decidable.byContradiction, Not, id, Fin, ite, rfl, Finset.prod, Finset.univ, Nat.factorial, Eq.mpr, HMul.hMul, Fin.succ, congrArg, Fin.prod_univ_succ, congrFun' and 49 more

   63 instances, coercions and auxiliary constants left out.

   Tactic trace: 23 steps

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

   theorem erdos_400.variants.g_pos (k n : ℕ) (h: k ≥ 2) : 0 < g k n := by
   …

   Mentions: Erdos400.g