Skip to content

Erdős problem 312

Start work

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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/312.lean

Formal Conjectures

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

Continue

Start a contributionBrowse the source filesOpen the collection entry