Skip to content

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 ∑n∈A1/n>K\sum_{n \in A} 1/n > K there exists some S⊆AS \subseteq A such that 1−exp⁡(−(c∗K))<∑n∈S1/n≤11 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

312.lean

Retained formal statement1 of 1

Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with ∑n∈A1/n>K\sum_{n \in A} 1/n > K there exists some S⊆AS \subseteq A such that 1−exp⁡(−(c∗K))<∑n∈S1/n≤11 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1?

FormalConjectures/ErdosProblems/312.leanErdos312.erdos_3129 linesExact file
True ↔  ∃ 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))⁻¹ ≤ 1
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page