boseLog_series
plain-language theorem explainer
For every real t>0 the Mercator series ∑_{n≥0} e^{-t(n+1)}/(n+1) sums to −log(1−e^{−t}). Cosmology and statistical-mechanics proofs that expand the Bose logarithmic entropy kernel cite it. The argument checks |e^{−t}|<1 and invokes Mathlib’s power-series form of −log(1−x), then reindexes by a ring identity.
Claim. For every real $t>0$, the series $\sum_{n=0}^{\infty} \frac{(e^{-t})^{n+1}}{n+1}$ converges (in the sense of `HasSum`) to $-\log(1-e^{-t})$.
background
The module derives the radiation identity $s=(4/3)\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than assuming the thermodynamic 4/3 factor. For Bose–Einstein statistics the entropy integrand splits pointwise as
$$\sigma_B(x)=\frac{x^3}{e^x-1}+x^2\bigl(-\log(1-e^{-x})\bigr).$$
The second summand is the Bose logarithmic kernel. Its Mellin transform at $s=3$ is needed to evaluate $\int_0^\infty\sigma_B$ and match it to $(4/3)$ times the energy integral $\int x^3/(e^x-1)$.
The classical Mercator expansion $-\log(1-z)=\sum_{n\ge0}z^{n+1}/(n+1)$ for $|z|<1$ supplies the series representation of that kernel once $z=e^{-t}$ with $t>0$.
proof idea
First prove $|e^{-t}|<1$: positivity of the exponential gives the absolute value, and $t>0$ forces $e^{-t}<1$ via Real.exp_lt_one_iff and linarith. Then apply Mathlib’s Real.hasSum_pow_div_log_of_abs_lt_one at that radius bound, which yields
$$\mathrm{HasSum}\bigl(n\mapsto z^{n+1}/(n+1),;-\log(1-z)\bigr)$$
for $z=e^{-t}$. A one-line congr_fun with ring aligns the summand indexing with the stated formula.
why it matters
This lemma is the series engine behind hasSum_mellin_boseLog, the Mellin/Dirichlet identity for the Bose logarithmic kernel at $s=3$. That identity feeds the evaluation of $\int\sigma_B$ and therefore the proved equalities
$$\int_0^\infty\sigma_B=\frac{4\pi^4}{45}=\frac43\int_0^\infty\frac{x^3}{e^x-1},$$
together with the entropy coefficient $2\pi^2/45$ that appears in $s_\gamma=(2\pi^2/45)gT^3$. In the broader $\eta_B$ chain it closes the statistical-mechanics step that previously treated the 4/3 factor as an external thermodynamic input. The Fermi twin (fermiLog_series) plays the analogous role for the 7/8 weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.