twoLevelPartition

formal source

 150    Z = 1 + exp(-βε)
 151
 152    This is the basis for the Ising model, spin systems, etc. -/
 153noncomputable def twoLevelPartition (epsilon : ℝ) (T : ℝ) (hT : T > 0) : ℝ :=
 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: