Does there exist a constant `c > 0` such that, for any `K > 1`, whenever `A` is a sufficiently large
finite multiset of integers with $\sum_{n \in A} 1/n > K$ there exists some $S \subseteq A$ such that
$1 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1$?
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_312 :
answer(sorry) ↔
∃ (c : ℝ), 0 < c ∧
∀ (K : ℝ), 1 < K →
∃ (N₀ : ℕ),
∀ (n : ℕ) (a : Fin n → ℕ),
(n ≥ N₀ ∧ (∑ i : Fin n, (a i : ℝ)⁻¹) > K) →
∃ (S : Finset (Fin n)),
1 - Real.exp (-(c * K)) < (∑ i ∈ S, (a i : ℝ)⁻¹) ∧
∑ i ∈ S, (a i : ℝ)⁻¹ ≤ 1
