Erdős Problem 316

Reference: erdosproblems.com/316

theorem Erdos316.erdos_316 : (∀ (A : Finset ℕ), 0 ∉ A → 1 ∉ A → ∑ n ∈ A, 1 / ↑n < 2 → ∃ (A₁ : Finset ℕ) (A₂ : Finset ℕ), Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧ ∑ n ∈ A₁, 1 / ↑n < 1 ∧ ∑ n ∈ A₂, 1 / ↑n < 1) ↔ False

Is it true that if $A \subseteq \mathbb{N}\setminus\{1\}$ is a finite set with $\sum_{n \in A} \frac{1}{n} < 2$ then there is a partition $A=A_1 \sqcup A_2$ such that $\sum_{n \in A_i} \frac{1}{n} < 1$ for $i=1,2$?

This is not true in general, as shown by Sándor [Sa97].

[Sa97] S'{A}ndor, Csaba, On a problem of Erdős. J. Number Theory (1997), 203-210.

theorem Erdos316.erdos_316.variants.multiset : ∃ (A : Multiset ℕ), 0 ∉ A ∧ 1 ∉ A ∧ (Multiset.map (fun (x : ℚ) => 1 / x) do let a ← A pure ↑a).sum < 2 ∧ ∀ (A₁ A₂ : Multiset ℕ), A = A₁ + A₂ → 1 ≤ (Multiset.map (fun (x : ℚ) => 1 / x) do let a ← A₁ pure ↑a).sum ∨ 1 ≤ (Multiset.map (fun (x : ℚ) => 1 / x) do let a ← A₂ pure ↑a).sum

It is not true if A is a multiset (easier)

theorem Erdos316.erdos_316.variants.generalized (n : ℕ) (hn : 2 ≤ n) : ∃ (A : Finset ℕ), A.Nonempty ∧ 0 ∉ A ∧ 1 ∉ A ∧ ∑ k ∈ A, 1 / ↑k < ↑n ∧ ∀ (P : Finpartition A), P.parts.card = n → ∃ p ∈ P.parts, 1 ≤ ∑ n ∈ p, 1 / ↑n

More generally, Sándor shows that for any $n \ge 2$ there exists a finite set $A \subseteq \mathbb{N}\setminus\{1\}$ with $\sum_{k \in A} \frac{1}{k} < n$, and no partition into $n$ parts each of which has $\sum_{n \in A_i} \frac{1}{n} < 1$.