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