Skip to content

Erdős problem 317

Start work

Is there some constant c>0c>0 such that for every n≥1n\geq 1 there exists some δk∈{−1,0,1}\delta_k\in \{-1,0,1\} for 1≤k≤n1\leq k\leq n with 0<∣∑1≤k≤nδkk∣<c2n?0< \left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert < \frac{c}{2^n}?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

317.lean

Retained formal statement2 of 4

Is there some constant c>0c>0 such that for every n≥1n\geq 1 there exists some δk∈{−1,0,1}\delta_k\in \{-1,0,1\} for 1≤k≤n1\leq k\leq n with 0<∣∑1≤k≤nδkk∣<c2n?0< \left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert < \frac{c}{2^n}?

FormalConjectures/ErdosProblems/317.leanErdos317.erdos_3173 linesExact file
sorry ↔  ∃ c > 0,    ∀ n ≥ 1, ∃ δ, Set.range δ ⊆ {-1, 0, 1} ∧ 0 < |∑ k, ↑(δ k) / (↑↑k + 1)| ∧ |∑ k, ↑(δ k) / (↑↑k + 1)| < c / 2 ^ n
OpenStatement only, no proof