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 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersCanonicalEnsemble.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.
CanonicalEnsemble.meanEnergy_eq_neg_deriv_log_mathZ_of_beta
Plain-language statement
The mean energy is the negative derivative of the logarithm of the (mathematical) partition function with respect to β = 1/(kB T). see: Tong (§1.3.2, §1.3.3), L&L (§31, implicitly, and §36) Here the derivative is a derivWithin over Set.Ioi 0 since β > 0.
Source project: Physlib
Person-level attribution pending.