averageEnergy

formal source

 196/-! ## Thermodynamic Quantities from Partition Function -/
 197
 198/-- Average energy ⟨E⟩ = -∂(ln Z)/∂β. -/
 199noncomputable def averageEnergy (sys : System) (beta : ℝ) : ℝ :=
 200  (sys.levels.map (fun l => l.energy * boltzmannFactor l beta)).sum / partitionFunction sys beta
 201
 202/-- Entropy S = kβ⟨E⟩ + k ln Z. -/
 203noncomputable def entropy (sys : System) (beta : ℝ) : ℝ :=
 204  beta * averageEnergy sys beta + Real.log (partitionFunction sys beta)
 205
 206/-- Free energy F = -kT ln Z = ⟨E⟩ - TS. -/
 207noncomputable def freeEnergy (sys : System) (beta : ℝ) : ℝ :=
 208  -temperature beta * Real.log (partitionFunction sys beta)
 209
 210/-- **THEOREM**: Free energy identity F = ⟨E⟩ - TS. -/
 211theorem free_energy_identity (sys : System) (beta : ℝ) (hb : beta > 0) :
 212    freeEnergy sys beta = averageEnergy sys beta - temperature beta * entropy sys beta := by
 213  -- F = -T ln Z
 214  -- S = β⟨E⟩ + ln Z
 215  -- ⟨E⟩ - T*S = ⟨E⟩ - (1/β)(β⟨E⟩ + ln Z) = ⟨E⟩ - ⟨E⟩ - (1/β) ln Z = -(1/β) ln Z = F
 216  unfold freeEnergy entropy temperature averageEnergy
 217  have hb' : beta ≠ 0 := hb.ne'
 218  field_simp
 219  ring
 220
 221/-! ## The Boltzmann Distribution from Maximum Entropy -/
 222
 223/-- **THEOREM (Entropy Positivity)**: The entropy of any system at positive
 224    temperature is non-negative when Z ≥ 1. This is a consequence of the
 225    Boltzmann definition S = β⟨E⟩ + ln Z and the non-negativity of ln Z. -/
 226theorem entropy_nonneg_of_Z_ge_one (sys : System) (beta : ℝ) (hb : beta > 0)
 227    (hE : 0 ≤ averageEnergy sys beta)
 228    (hZ : 1 ≤ partitionFunction sys beta) :
 229    0 ≤ entropy sys beta := by