Standalone Lean project
Community physics definitions, theorems, calculations, notation, tactics, and quantum-information developments.
Flagship declarations
adiabatic_relation_log
Plain-language statement
Adiabatic relation in logarithmic form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then c * log (Ua/Ub) + log (Va/Vb) = 0.
Source project: Physlib
Person-level attribution pending.
adiabatic_relation_UaUbVaVb
Plain-language statement
Adiabatic relation in product form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then (Ua/Ub)^c * (Va/Vb) = 1.
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.derivWithin_meanEnergy_Beta_eq_neg_variance
Plain-language statement
(∂U/∂β) = -Var(E) for finite systems.
Source project: Physlib
Person-level attribution pending.
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.
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.differentialEntropy_nonneg_of_prob_le_one
Plain-language statement
General entropy non-negativity under a pointwise upper bound probability ≤ 1. This assumption holds automatically in the finite/counting case (since sums bound each term), but can fail in general (continuous) settings; hence we separate it as a hypothesis. Finite case: see CanonicalEnsemble.entropy_nonneg in Finite.
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq
Plain-language statement
The identity Var(E) = ⟨E²⟩ - ⟨E⟩².
Source project: Physlib
Person-level attribution pending.
Project index
Showing 8 of 585 additional declarations. Use project search for the complete index.
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.
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.
CanonicalEnsemble.meanEnergy_eq_ratio_of_integrals
Plain-language statement
The mean energy can be expressed as a ratio of integrals.
Source project: Physlib
Person-level attribution pending.
CanonicalEnsemble.thermodynamicEntropy_eq_differentialEntropy_sub_correction
Plain-language statement
Fundamental relation between thermodynamic and differential entropy: S_thermo = S_diff - kB * dof * log h.
Source project: Physlib
Person-level attribution pending.