integrableOn_boseLog
plain-language theorem explainer
The Bose logarithmic kernel $t^2(-\log(1-e^{-t}))$ is Lebesgue-integrable on $(0,\infty)$. Cosmology proofs that split the Bose entropy integrand into an energy piece plus this log piece cite it to justify the set integral. The argument is pure contradiction: non-integrability would force the integral to $0$, contradicting the already-proved value $\pi^4/45$.
Claim. The map $t \mapsto t^{2}\bigl(-\log(1-e^{-t})\bigr)$ is integrable on the open ray $(0,\infty)$.
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. Pointwise, the Bose entropy integrand splits as $$\sigma_B(t)=\frac{t^3}{e^t-1}+t^2\bigl(-\log(1-e^{-t})\bigr).$$ The second summand is the Bose logarithmic kernel treated here.
Upstream, boseLog_integral_value already evaluates the improper integral to $\pi^4/45$ via a Mellin-transform route (series expansion of $-\log(1-e^{-t})$, termwise Gamma factors, and $\zeta(4)=\pi^4/90$). Integrability is the missing analytic hypothesis needed before that value can be used inside set-integral rewrites of $\int\sigma_B$.
proof idea
Proof by contradiction. Assume the kernel is not integrable on Ioi 0. Mathlib's integral_undef then forces the Lebesgue integral over that set to equal $0$. Rewrite that equality with boseLog_integral_value, obtaining $0=\pi^4/45$. A one-line positivity check gives $0<\pi^4/45$, and linarith closes the contradiction. No direct majorant or comparison test is built; the known nonzero value is the only input.
why it matters
Downstream parent is bose_entropy_integral_value, which assembles
$$\int_0^\infty\sigma_B=4\pi^4/45$$
by integrating the pointwise split and adding the Bose energy integral $\pi^4/15$ to this log integral $\pi^4/45$. That identity is the Bose half of the module's main claim: entropy equals $(4/3)$ times energy density over temperature, with the $4/3$ emerging from the functional rather than being inserted by hand. The same pattern (integrability via nonzero evaluated integral) is mirrored for the Fermi log kernel. In the broader $\eta_B$ chain this closes the statistical-mechanics step that earlier entropy-per-photon and number-density modules had treated as an external thermodynamic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.