Skip to content

Erdős problem 321

What is the largest A⊆{1,…,N}A\subseteq\{1,\dots,N\} such that all subset sums ∑n∈S1/n\sum_{n\in S}1/n (over S⊆AS\subseteq A) are distinct?

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

321.lean

Retained formal statement6 of 6

Let R(N)R(N) be the maximal such size. Results of Bleicher and Erdős from [BlEr75] and [BlEr76b] imply that R(N)≤1log⁡2log⁡rN(Nlog⁡N∏i=3rlog⁡iN), 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≥4k \ge 4 with log⁡kN≥k\log_k N \ge k and any r≥1r \ge 1 with log⁡2rN≥1\log_{2r} N \ge 1. (In these bounds log⁡in\log_i n denotes the ii-fold iterated logarithm.)

[BlEr75] Bleicher, M. N. and Erdős, P., _The number of distinct subsums of Unparsed notation: \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.

FormalConjectures/ErdosProblems/321.leanErdos321.erdos_321.variants.upper4 linesExact file
∀ (N r : ℕ),  1 ≤ r →    1 ≤ Real.log^[2 * r] ↑N →      ↑(Erdos321.R N) ≤ 1 / Real.log 2 * Real.log^[r] ↑N * ↑N / Real.log ↑N * ∏ i ∈ Finset.Icc 3 r, Real.log^[i] ↑N
SolvedStatement only, no proofformal statement reference