`beta`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.PartitionFunction
domain: Thermodynamics
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Thermodynamics.PartitionFunction on GitHub at line 37.

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

  34noncomputable def k_B : ℝ := 1.380649e-23
  35
  36/-- Inverse temperature β = 1/(k_B T). -/
  37noncomputable def beta (T : ℝ) (hT : T > 0) : ℝ := 1 / (k_B * T)
  38
  39/-! ## The Classical Partition Function -/
  40
  41/-- A discrete system with energy levels. -/
  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ᵢ). -/
  55noncomputable def partitionFunction (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  56  ∑ i : Fin sys.numLevels, (sys.degeneracy i : ℝ) * exp (-beta T hT * sys.energy i)
  57
  58/-- **THEOREM**: Partition function is always positive. -/
  59theorem partition_function_positive (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) :
  60    partitionFunction sys T hT > 0 := by
  61  unfold partitionFunction
  62  have hne : Nonempty (Fin sys.numLevels) := ⟨⟨0, sys.nonempty⟩⟩
  63  apply Finset.sum_pos
  64  · intro i _
  65    apply mul_pos
  66    · -- degeneracy ≥ 1 > 0
  67      have h := sys.deg_pos i

papers checked against this theorem

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