/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/importFormalConjecturesUtil
[Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.)
(1948), 63-66.
namespaceErdos1049openArithmeticFunctionFilter
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$?
Substitute r := t⁻¹ so ‖r‖ < 1, then apply Mathlib's series identity
tsum_pow_div_one_sub_eq_tsum_sigma at k = 0:
$$\sum_{n \ge 1} \frac{r^n}{1 - r^n} = \sum_{n \ge 1} \sigma_0(n) \cdot r^n.$$
After clearing denominators, both sides match the Lambert identity:
LHS becomes 1/(t^n - 1) and RHS becomes τ(n) / t^n.
Both tsums equal 0 in this regime, but for different reasons in each
sub-case. We split on t ∈ {1, 0, -1} and the generic |t| < 1, t ≠ 0
remainder, and use the same key non-summability lemma below to handle
the cases where the series diverges.
t = 1: every LHS term is 1 / (1 - 1) = 0 (Lean convention), so the
LHS sum is trivially 0. RHS is Σ τ(n), non-summable.
t = 0: every RHS term is τ(n) / 0 = 0 (Lean convention), so the RHS
sum is trivially 0. LHS is Σ (-1), non-summable.
t = -1: alternating; LHS vanishes at even n but odd n give terms
of magnitude 1/2, an infinite set. RHS terms have magnitude τ(n) ≥ 1.
|t| < 1, t ≠ 0: standard; bounded denominator gives lower-bounded
reciprocal on LHS, and |t^n| ≤ 1 plus τ(n) ≥ 1 gives the RHS bound.
In every case, Lean's tsum_eq_zero_of_not_summable collapses the non-
summable side to 0, matching the 0 on the other side.