therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 44 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

44 results

Clear filters
Project-declaredLean 4.32.0

Differential Entropy eq k B beta mean Energy add k B log math Z

CanonicalEnsemble.differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ

Plain-language statement

General identity: S_diff = kB β ⟨E⟩ + kB log Z_math. This connects the differential entropy to the mean energy and the mathematical partition function. Integrability of log (probability …) follows from the pointwise formula.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Helmholtz Free Energy eq mean Energy sub temp mul thermodynamic Entropy

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.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Log phys eq log math sub const on Ioi

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...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Mean Energy eq neg deriv log math Z of beta

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.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record