expectedEnergy
plain-language theorem explainer
expectedEnergy defines the average energy under the Boltzmann distribution at inverse temperature β as a direct sum. Discrete statistical mechanics derivations cite it when establishing thermodynamic identities from the partition function. The definition is introduced by one-line summation over boltzmannProb times state energies with no auxiliary lemmas.
Claim. The expected energy is the average $E$ under the Boltzmann distribution: $E_β = ∑_i p_i E_i$ where $p_i = exp(-β E_i)/Z$ and $Z = ∑_i exp(-β E_i)$ is the partition function.
background
The HelmholtzReal module supplies real proofs for Helmholtz free energy on finite discrete index sets ι. The partition function Z and Boltzmann probabilities are defined in the same module; boltzmannEntropy is the corresponding Shannon entropy. Upstream results include entropy as total defect from InitialCondition.entropy and discrete spectral structures from SpectralEmergence.of that supply the finite index set.
proof idea
One-line definition that directly unfolds the sum of boltzmannProb E β i multiplied by E i. No tactics or upstream lemmas are invoked beyond the already-established boltzmannProb in the module.
why it matters
This supplies the energy term required by F_eq_E_minus_TS to prove helmholtzF E β = expectedEnergy E β - (1/β) * boltzmannEntropy E β and by HelmholtzRealCert to certify the discrete thermodynamic relations. It grounds the real version of free-energy minimization used in vfe_at_boltzmann_eq_helmholtzF, consistent with the module's use of the Gibbs inequality on the simplex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.