pith. machine review for the scientific record. sign in
theorem proved term proof

twoLevel_at_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 164theorem twoLevel_at_zero (T : ℝ) (hT : T > 0) :
 165    twoLevelPartition 0 T hT = 2 := by

proof body

Term-mode proof.

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

depends on (9)

Lean names referenced from this declaration's body.