Erdős problem 312
Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with there exists some such that ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/312.leanTrue ↔ ∃ c, 0 < c ∧ ∀ (K : ℝ), 1 < K → ∃ N₀, ∀ (n : ℕ) (a : Fin n → ℕ), n ≥ N₀ ∧ ∑ i, (↑(a i))⁻¹ > K → ∃ S, 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1OpenStatement only, no proof