partitionFunction

formal source

  36variable {ι : Type*} [Fintype ι] [Nonempty ι]
  37
  38/-- Partition function for a discrete energy level set. -/
  39def partitionFunction (E : ι → ℝ) (β : ℝ) : ℝ :=
  40  ∑ i, Real.exp (-β * E i)
  41
  42theorem partitionFunction_pos (E : ι → ℝ) (β : ℝ) :
  43    0 < partitionFunction E β := by
  44  unfold partitionFunction
  45  apply Finset.sum_pos
  46  · intro i _
  47    exact Real.exp_pos _
  48  · exact Finset.univ_nonempty
  49
  50/-- Boltzmann probability for level `i`. -/
  51def boltzmannProb (E : ι → ℝ) (β : ℝ) (i : ι) : ℝ :=
  52  Real.exp (-β * E i) / partitionFunction E β
  53
  54theorem boltzmannProb_pos (E : ι → ℝ) (β : ℝ) (i : ι) :
  55    0 < boltzmannProb E β i :=
  56  div_pos (Real.exp_pos _) (partitionFunction_pos E β)
  57
  58theorem boltzmannProb_sum_one (E : ι → ℝ) (β : ℝ) :
  59    ∑ i, boltzmannProb E β i = 1 := by
  60  unfold boltzmannProb partitionFunction
  61  rw [← Finset.sum_div]
  62  exact div_self (ne_of_gt (partitionFunction_pos E β))
  63
  64/-- Helmholtz free energy as a function of the partition function. -/
  65def helmholtzF (E : ι → ℝ) (β : ℝ) : ℝ :=
  66  - Real.log (partitionFunction E β) / β
  67
  68theorem helmholtzF_well_defined (E : ι → ℝ) (β : ℝ) (hβ : β ≠ 0) :
  69    helmholtzF E β = - Real.log (partitionFunction E β) / β := rfl