Erdős Problem 1049

References:

• erdosproblems.com/1049
• [Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.) (1948), 63-66.

theorem Erdos1049.erdos_1049 : sorry ↔ ∀ t > 1, Irrational (∑' (n : ℕ+), 1 / (↑t ^ ↑n - 1))

Let $t>1$ be a rational number. Is $\sum_{n=1}^\infty\frac{1}{t^n-1}=\sum_{n=1}^\infty \frac{\tau(n)}{t^n}$ irrational, where $\tau(n)$ counts the divisors of $n$?

A conjecture of Chowla.

theorem Erdos1049.erdos_1049.variants.geq_2_integer (t : ℤ) : t ≥ 2 → Irrational (∑' (n : ℕ+), 1 / (↑t ^ ↑n - 1))

Erdős [Er48] proved that this is true if $t\geq 2$ is an integer.

theorem Erdos1049.lambert_series_eq_num_divisor_sum (t : ℚ) : ∑' (n : ℕ+), 1 / (↑t ^ ↑n - 1) = ∑' (n : ℕ+), ↑(↑n).divisors.card / ↑t ^ ↑n

The classical Lambert series identity: $\sum_{n=1}^\infty \frac{1}{t^n - 1} = \sum_{n=1}^\infty \frac{\tau(n)}{t^n}$, where $\tau(n)$ counts the divisors of $n$.