twoLevel_gt_one

formal source

 154  1 + exp (-beta T hT * epsilon)
 155
 156/-- Two-level partition function is always > 1. -/
 157theorem twoLevel_gt_one (epsilon : ℝ) (T : ℝ) (hT : T > 0) :
 158    twoLevelPartition epsilon T hT > 1 := by
 159  unfold twoLevelPartition
 160  have h : exp (-beta T hT * epsilon) > 0 := exp_pos _
 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! -/