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

averageEnergy

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)

  79noncomputable def averageEnergy (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=

proof body

Definition body.

  80  (∑ i : Fin sys.numLevels,
  81    sys.energy i * (sys.degeneracy i : ℝ) * exp (-beta T hT * sys.energy i)) /
  82  partitionFunction sys T hT
  83
  84/-- Entropy S = k_B(ln Z + β⟨E⟩). -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.