Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 4 research declarations. Search 10,000 more complete Mathlib declarations.
4 results
Clear filtersCanonicalEnsemble.derivWithin_meanEnergy_Beta_eq_neg_variance
Plain-language statement
(∂U/∂β) = -Var(E) for finite systems.
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.entropy_nonneg
Plain-language statement
The entropy of a finite canonical ensemble (Shannon entropy) is non-negative.
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.fluctuation_dissipation_theorem_finite
Plain-language statement
FDT for finite canonical ensembles: C_V = Var(E) / (k_B T²).
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.thermodynamicEntropy_eq_shannonEntropy
Plain-language statement
In the finite, nonempty case the thermodynamic and Shannon entropies coincide. All semi-classical correction factors vanish (dof = 0, phaseSpaceUnit = 1), so the absolute thermodynamic entropy reduces to the discrete Shannon form.
Source project: Physlib
Person-level attribution pending.