Skip to content

Erdős problem 260

Start work

Let a1<a2<⋯a_1 < a_2 < \cdots be an increasing sequence such that ann→∞\frac{a_n}{n} \to \infty. Is the sum ∑n∞an2an\sum_{n}^{\infty} \frac{a_n}{2^{a_n}} irrational?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

260.lean

Retained formal statement1 of 1

Let a1<a2<⋯a_1 < a_2 < \cdots be an increasing sequence such that ann→∞\frac{a_n}{n} \to \infty. Is the sum ∑n∞an2an\sum_{n}^{\infty} \frac{a_n}{2^{a_n}} irrational?

FormalConjectures/ErdosProblems/260.leanErdos260.erdos_2605 linesExact file
sorry ↔  ∀ (a : ℕ → ℤ) (s : ℝ),    StrictMono a →      Filter.Tendsto (fun n => ↑(a n) / ↑n) Filter.atTop Filter.atTop →        HasSum (fun n => ↑(a n) / 2 ^ a n) s → Irrational s
OpenStatement only, no proof