Erdős Problem 321

Reference: erdosproblems.com/321

noncomputable def Erdos321.R (N : ℕ) : ℕ

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$.

Equations

• Erdos321.R N = sSup {x : ℕ | ∃ (A : Finset ℕ) (_ : A ⊆ Finset.Icc 1 N) (_ : Set.InjOn (fun (S : Finset ℕ) => ∑ n ∈ S, 1 / ↑n) ↑A.powerset), A.card = x}

theorem Erdos321.erdos_321 (N : ℕ) : R N = sorry

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)$?

theorem Erdos321.erdos_321.variants.isTheta : (fun (N : ℕ) => ↑(R N)) =Θ[Filter.atTop] sorry

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))$?

theorem Erdos321.erdos_321.variants.isBigO : (fun (N : ℕ) => ↑(R N)) =O[Filter.atTop] sorry

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))$.

theorem Erdos321.erdos_321.variants.isLittleO : (fun (N : ℕ) => ↑(R N)) =o[Filter.atTop] sorry

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))$.

theorem Erdos321.erdos_321.variants.lower (N k : ℕ) (hk : 4 ≤ k) (hkN : ↑k ≤ Real.log^[k] ↑N) : ↑N / Real.log ↑N * ∏ i ∈ Finset.Icc 3 k, Real.log^[i] ↑N ≤ ↑(R N)

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.

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

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.)

[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.