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

DiscreteSystem

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)

  42structure DiscreteSystem where
  43  /-- Number of energy levels -/
  44  numLevels : ℕ
  45  /-- Energy of each level -/
  46  energy : Fin numLevels → ℝ
  47  /-- Degeneracy of each level (must be positive) -/
  48  degeneracy : Fin numLevels → ℕ
  49  /-- At least one level -/
  50  nonempty : numLevels > 0
  51  /-- Each level has degeneracy ≥ 1 -/
  52  deg_pos : ∀ i, degeneracy i ≥ 1
  53
  54/-- The canonical partition function Z = Σᵢ gᵢ exp(-βEᵢ). -/

used by (6)

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

depends on (16)

Lean names referenced from this declaration's body.