boseOccupation_eq
plain-language theorem explainer
For dimensionless energy t = E/T > 0, the ensemble-mean occupation of a single bosonic mode equals the Bose–Einstein factor 1/(e^t − 1). Cosmology and statistical-mechanics arguments that need the closed form of ⟨n⟩_B cite this. The proof unfolds the definition, substitutes the geometric partition function, evaluates the arithmetico-geometric series Σ n x^n, and simplifies.
Claim. For every real $t > 0$, the mean bosonic occupation $\langle n \rangle_B(t) := \bigl(\sum_{n=0}^\infty n\, e^{-n t}\bigr)/Z_B(t)$ equals $1/(e^{t}-1)$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from a single-mode grand partition function at μ = 0, rather than taking them as model inputs. The only data are the Gibbs weight w_n = e^{−n t} with t = E/T and the occupancy sets: n ∈ ℕ for bosons, n ∈ {0,1} for fermions.
Mean bosonic occupation is defined as ⟨n⟩_B = (Σ_n n · w_n) / Z_B. The one-quantum weight satisfies boltzmannWeight_pow: w_n = (e^{−t})^n. The Bose partition is the geometric series Z_B(t) = (1 − e^{−t})^{−1} for t > 0 (bosePartition_eq), which needs e^{−t} < 1 (exp_neg_lt_one).
This theorem closes the occupation step of the module ledger: once ⟨n⟩_B is known in closed form, energy kernels become t · ⟨n⟩ and thermodynamic identities follow by differentiation of ln Z.
proof idea
Unfold boseOccupation and rewrite the denominator via bosePartition_eq. Replace each weight by boltzmannWeight_pow so the numerator is Σ n x^n with x = e^{−t}. The hypotheses 0 ≤ x and ‖x‖ < 1 (from exp_pos and exp_neg_lt_one) license Mathlib’s tsum_coe_mul_geometric_of_norm_lt_one, giving x/(1−x)^2. With one_lt_exp and the nonzero denominators e^t − 1 and 1 − e^{−t}, rewrite e^{−t} = 1/e^t and finish by field_simp to 1/(e^t − 1).
why it matters
This is the Bose–Einstein distribution step in the module’s derivation chain from Σ e^{−n E/T} to the plasma kernels. Downstream, boseEnergyKernel_eq_occupation rewrites the energy integrand as t · ⟨n⟩_B; boseLogKernel_hasDerivAt proves grand-canonical consistency d/dt[−ln(1−e^{−t})] = −⟨n⟩_B, so pressure and energy are one input; boseOccupation_pos records positivity; number_integrand_bose identifies the photon number density integrand t²/(e^t−1) with t² · ⟨n⟩_B (integral 2ζ(3)).
In the broader RS cosmology stack this discharges the MODEL status that PhaseSpaceReduction previously assigned to the Bose energy kernel, so the η_B plasma pressure/energy chain starts from the occupancy sum rather than an inserted formula. No forcing-chain landmark (T5–T8) is touched directly; the result is classical statistical mechanics inside the RS formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.