exp_neg_lt_one
plain-language theorem explainer
For every positive real t, the Boltzmann factor e^{-t} is strictly less than one. Bose partition, positivity, occupation, and log-kernel derivative proofs cite it to justify the geometric-series radius and denominator signs. The proof is a one-line wrapper of Mathlib's exp_lt_one_iff plus linarith.
Claim. For every real number $t>0$, one has $e^{-t}<1$.
background
The StatisticsKernels module rebuilds the Bose and Fermi pressure and energy kernels from a single-mode grand partition function at vanishing chemical potential. The only inputs are Gibbs weights $e^{-n t}$ with dimensionless $t=E/T$, unrestricted occupancy $n\in\mathbb{N}$ for bosons, and $n\in{0,1}$ for fermions.
For bosons the mode partition is the geometric series $Z_B=\sum_{n=0}^\infty x^n$ with ratio $x=e^{-t}$. Mathlib's geometric tsum requires $0\le x<1$. Positivity of the exponential is standard; the strict upper bound $x<1$ is exactly this lemma. The same bound keeps $1-e^{-t}>0$, so the closed form $(1-e^{-t})^{-1}$ is positive and the log-pressure kernel is well-defined.
proof idea
One-line wrapper. Apply the Mathlib equivalence Real.exp_lt_one_iff in the reverse direction: $e^u<1$ iff $u<0$. Instantiate at $u=-t$ and discharge $-t<0$ from the hypothesis $t>0$ by linarith.
why it matters
Without $e^{-t}<1$ the Bose geometric series does not converge in Mathlib, so the closed form $Z_B=(1-e^{-t})^{-1}$ is unavailable. Downstream, bosePartition_eq feeds the bound straight into tsum_geometric_of_lt_one; bosePartition_pos uses it to prove the inverse is positive; boseOccupation_eq needs the same radius to evaluate $\langle n\rangle_B=1/(e^t-1)$; and boseLogKernel_hasDerivAt differentiates through $1-e^{-t}$ under that strict inequality.
Those identities are the module's bridge from $\sum e^{-nE/T}$ to the pressure kernel $-\ln(1-e^{-t})$ and energy kernel $t/(e^t-1)$, which then enter the plasma pressure and energy capstones of the $\eta_B$ cosmology chain. The lemma is elementary analysis, but it is the gate that turns the Bose occupancy set into the standard kernels rather than leaving them as MODEL definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.