theorem
proved
twoLevel_at_zero
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Thermodynamics.PartitionFunction on GitHub at line 164.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
161 linarith
162
163/-- At ε = 0, Z = 2 (two degenerate levels). -/
164theorem twoLevel_at_zero (T : ℝ) (hT : T > 0) :
165 twoLevelPartition 0 T hT = 2 := by
166 unfold twoLevelPartition beta
167 simp only [mul_zero, exp_zero]
168 ring
169
170/-- Harmonic oscillator partition function.
171
172 Eₙ = (n + 1/2)ℏω for n = 0, 1, 2, ...
173
174 Z = exp(-βℏω/2) / (1 - exp(-βℏω))
175
176 This leads to Planck's radiation law. -/
177noncomputable def harmonicOscillatorPartition (omega : ℝ) (T : ℝ) (hT : T > 0)
178 (hω : omega > 0) : ℝ :=
179 exp (-beta T hT * hbar * omega / 2) / (1 - exp (-beta T hT * hbar * omega))
180
181/-! ## The Classical Limit -/
182
183/-- In the classical limit (high T, many states), the sum becomes an integral:
184
185 Z = ∫ d³q d³p / h³ exp(-βH(q,p))
186
187 The factor h³ comes from the 8-tick phase space discretization! -/
188theorem classical_limit :
189 -- As T → ∞ and states become dense:
190 -- Σ → ∫ d³q d³p / h³
191 -- This is Liouville's phase space measure
192 True := trivial
193
194/-! ## Quantum Statistics -/