FormalConjectures/ErdosProblems/321.lean

GitHub source file

7 declarations, 6 contain sorry, 0 declared as axioms

1. def Erdos321.R Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$ line 38 source

   Source documentation

   Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$.

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

   Statement uses: Nat

   Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, LE.le, Finset.Icc, OfNat.ofNat, Set.InjOn, Rat, Finset.sum, HDiv.hDiv, Finset.powerset, Eq, Finset.card

   15 instances, coercions and auxiliary constants left out.

   noncomputable def R (N : ℕ) : ℕ :=
   …

2. theorem Erdos321.erdos_321 Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$ sorry line 47 source

   Source documentation

   Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$. What is $R(N)$?

   depends on sorry what this means

   Statement uses: Nat, Eq, Erdos321.R, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_321 (N : ℕ) :
       R N = answer(sorry) := by
   …

   Mentions: Erdos321.R

3. theorem Erdos321.erdos_321.variants.isTheta Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$ sorry line 65 source

   Source documentation

   Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$. What is $\Theta(R(N))$?

   depends on sorry what this means

   Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Erdos321.R, sorryAx, Bool.false

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   9 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_321.variants.isTheta :
       (fun N ↦ (R N : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := by
   …

   Mentions: Erdos321.R

4. theorem Erdos321.erdos_321.variants.isBigO Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$ sorry line 73 source

   Source documentation

   Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$. Find the simplest $g(N)$ such that $R(N) = O(g(N))$.

   depends on sorry what this means

   Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos321.R, sorryAx, Bool.false

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   9 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_321.variants.isBigO :
       (fun N ↦ (R N : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := by
   …

   Mentions: Erdos321.R

5. theorem Erdos321.erdos_321.variants.isLittleO Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$ sorry line 81 source

   Source documentation

   Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$. Find the simplest $g(N)$ such that $R(N) = o(g(N))$.

   depends on sorry what this means

   Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos321.R, sorryAx, Bool.false

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   9 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_321.variants.isLittleO :
       (fun N ↦ (R N : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := by
   …

   Mentions: Erdos321.R

6. theorem Erdos321.erdos_321.variants.lower Let $R(N)$ be the maximal such size sorry line 96 source

   Source documentation

   Let $R(N)$ be the maximal such size. Results of Bleicher and Erdős from [BlEr75] and [BlEr76b] imply that $$ \frac{N}{\log N} \prod_{i=3}^{k} \log_i N \le R(N), $$ valid for any $k \ge 4$ with $\log_k N \ge k$ and any $r \ge 1$ with $\log_{2r} N \ge 1$. (In these bounds $\log_i n$ denotes the $i$-fold iterated logarithm.)

   [BlEr75] Bleicher, M. N. and Erdős, P., The number of distinct subsums of $\sum \sb{1}\spN\,1/i$. Math. Comp. (1975), 29-42. [BlEr76b] Bleicher, Michael N. and Erdős, Paul, Denominators of Egyptian fractions. II. Illinois J. Math. (1976), 598-613.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Real, Nat.iterate, Real.log, HMul.hMul, HDiv.hDiv, Finset.prod, Finset.Icc, Erdos321.R

   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_321.variants.lower (N k : ℕ) (hk : 4 ≤ k) (hkN : k ≤ log^[k] N) :
       N / log N * ∏ i ∈ Finset.Icc 3 k, (log^[i] N) ≤ R N := by
   …

   Mentions: Erdos321.R

7. theorem Erdos321.erdos_321.variants.upper Let $R(N)$ be the maximal such size sorry line 115 source

   Source documentation

   Let $R(N)$ be the maximal such size. Results of Bleicher and Erdős from [BlEr75] and [BlEr76b] imply that $$ R(N) \le \frac{1}{\log 2} \log_r N \left( \frac{N}{\log N} \prod_{i=3}^{r} \log_i N \right), $$ valid for any $k \ge 4$ with $\log_k N \ge k$ and any $r \ge 1$ with $\log_{2r} N \ge 1$. (In these bounds $\log_i n$ denotes the $i$-fold iterated logarithm.)

   Since Real.log is defined on all of $\mathbb{R}$, the condition $\log_{2r} N \ge 1$ is formalised as $\log_i N \ge 1$ for all $i \le 2r$, which is equivalent to it for the genuine iterated logarithm and ensures that every intermediate iterate is positive.

   [BlEr75] Bleicher, M. N. and Erdős, P., The number of distinct subsums of $\sum \sb{1}\spN\,1/i$. Math. Comp. (1975), 29-42. [BlEr76b] Bleicher, Michael N. and Erdős, Paul, Denominators of Egyptian fractions. II. Illinois J. Math. (1976), 598-613.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Real, Nat.iterate, Real.log, Erdos321.R, HDiv.hDiv, Finset.prod, Finset.Icc

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

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_321.variants.upper (N r : ℕ) (hr : 1 ≤ r) (hrN : ∀ i ≤ 2 * r, 1 ≤ log^[i] N) :
       R N ≤ 1 / log 2 * log^[r] N * N / log N * ∏ i ∈ Finset.Icc 3 r, (log^[i] N) := by
   …

   Mentions: Erdos321.R