partitionFunction

formal source

  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 -/
  73
  74/-- The Helmholtz free energy F = -k_B T ln Z. -/
  75noncomputable def freeEnergy (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  76  -k_B * T * log (partitionFunction sys T hT)
  77
  78/-- Average energy ⟨E⟩ = -∂ln Z/∂β = Σᵢ Eᵢ Pᵢ. -/
  79noncomputable def averageEnergy (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  80  (∑ i : Fin sys.numLevels,
  81    sys.energy i * (sys.degeneracy i : ℝ) * exp (-beta T hT * sys.energy i)) /
  82  partitionFunction sys T hT
  83
  84/-- Entropy S = k_B(ln Z + β⟨E⟩). -/
  85noncomputable def entropy (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=