pith. machine review for the scientific record. sign in
def definition def or abbrev

harmonicOscillatorPartition

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)

 177noncomputable def harmonicOscillatorPartition (omega : ℝ) (T : ℝ) (hT : T > 0)
 178    (hω : omega > 0) : ℝ :=

proof body

Definition body.

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

depends on (17)

Lean names referenced from this declaration's body.