`partitionFunction`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.BoltzmannDistribution
domain: Thermodynamics
line: 76 · 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 76.

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

  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
  85  · exact exp_pos _
  86
  87/-- Helper: sum of positive list is nonneg -/
  88lemma list_sum_nonneg_of_pos {l : List ℝ} (h : ∀ x ∈ l, 0 < x) : 0 ≤ l.sum := by
  89  induction l with
  90  | nil => simp
  91  | cons head tail ih =>
  92    simp only [List.sum_cons]
  93    have h1 : 0 < head := h head (by simp)
  94    have h2 : 0 ≤ tail.sum := ih fun x hx => h x (by simp [hx])
  95    linarith
  96
  97/-- **THEOREM**: The partition function is positive for positive temperatures. -/
  98theorem partition_positive (sys : System) (beta : ℝ) (hb : beta > 0) :
  99    partitionFunction sys beta > 0 := by
 100  unfold partitionFunction
 101  -- The partition function is a sum of positive terms
 102  have hne : 0 < sys.levels.length := sys.nonempty
 103  -- Get the first element
 104  have hex : ∃ head tail, sys.levels = head :: tail := by
 105    cases heq : sys.levels with
 106    | nil => simp [heq] at hne

papers checked against this theorem

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