`EnergyLevel`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.BoltzmannDistribution
domain: Thermodynamics
line: 54 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Thermodynamics.BoltzmannDistribution on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  51/-! ## Energy Levels and States -/
  52
  53/-- An energy level with degeneracy. -/
  54structure EnergyLevel where
  55  /-- Energy value (in natural units). -/
  56  energy : ℝ
  57  /-- Degeneracy (number of microstates). -/
  58  degeneracy : ℕ
  59  /-- Degeneracy is positive. -/
  60  deg_pos : degeneracy > 0
  61
  62/-- A system is a collection of energy levels. -/
  63structure System where
  64  /-- The energy levels. -/
  65  levels : List EnergyLevel
  66  /-- Non-empty. -/
  67  nonempty : levels.length > 0
  68
  69/-! ## The Partition Function -/
  70
  71/-- The Boltzmann factor for an energy level at inverse temperature β. -/
  72noncomputable def boltzmannFactor (level : EnergyLevel) (beta : ℝ) : ℝ :=
  73  level.degeneracy * Real.exp (-beta * level.energy)
  74
  75/-- The partition function Z = Σ g_i exp(-β E_i). -/
  76noncomputable def partitionFunction (sys : System) (beta : ℝ) : ℝ :=
  77  (sys.levels.map (fun l => boltzmannFactor l beta)).sum
  78
  79/-- Helper: Boltzmann factor is positive. -/
  80lemma boltzmannFactor_pos (level : EnergyLevel) (beta : ℝ) :
  81    boltzmannFactor level beta > 0 := by
  82  unfold boltzmannFactor
  83  apply mul_pos
  84  · exact Nat.cast_pos.mpr level.deg_pos

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.