DiscreteSystem

formal source

  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
  68      exact Nat.cast_pos.mpr (Nat.lt_of_lt_of_le Nat.zero_lt_one h)
  69    · exact exp_pos _
  70  · exact @Finset.univ_nonempty (Fin sys.numLevels) _ hne
  71
  72/-! ## Thermodynamic Quantities from Z -/