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 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
CanonicalEnsemble.energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq
Plain-language statement
The identity Var(E) = ⟨E²⟩ - ⟨E⟩².
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.heatCapacity_eq_deriv_meanEnergyBeta
Plain-language statement
Relates C_V = dU/dT to dU/dβ. C_V = dU/dβ * (-1/(kB T²)).
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy
Project documentation
The Helmholtz free energy F is related to the mean energy U and the absolute thermodynamic entropy S by the identity F = U - TS. This theorem shows that the statistically-defined quantities in this framework correctly satisfy this principle of thermodynamics.
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.log_phys_eq_log_math_sub_const_on_Ioi
Plain-language statement
Helper: equality (on Set.Ioi 0) between the β–parametrized logarithm of the physical partition function and the β–parametrized logarithm of the mathematical partition function up to the (β–independent) semiclassical correction. This is used only to identify derivatives (the correction drops). We add the hypothesis h_fin giving finiteness of the Bolt...
Source project: Physlib
Person-level attribution pending.