partition_function

formal source

  76
  77/-- The Partition Function Z for a discrete set of states.
  78    Z = ∑_ω exp(-J(X(ω))/TR) -/
  79noncomputable def partition_function {Ω : Type*} [Fintype Ω]
  80    (sys : RecognitionSystem) (X : Ω → ℝ) : ℝ :=
  81  ∑ ω, gibbs_weight sys (X ω)
  82
  83/-- The partition function is positive. -/
  84theorem partition_function_pos {Ω : Type*} [Fintype Ω] [Nonempty Ω]
  85    (sys : RecognitionSystem) (X : Ω → ℝ) : 0 < partition_function sys X := by
  86  unfold partition_function
  87  apply Finset.sum_pos
  88  · intro ω _
  89    exact gibbs_weight_pos sys (X ω)
  90  · exact Finset.univ_nonempty
  91
  92/-- The Gibbs probability distribution on a discrete set of states.
  93    p(ω) = exp(-J(X(ω))/TR) / Z -/
  94noncomputable def gibbs_measure {Ω : Type*} [Fintype Ω]
  95    (sys : RecognitionSystem) (X : Ω → ℝ) (ω : Ω) : ℝ :=
  96  gibbs_weight sys (X ω) / partition_function sys X
  97
  98/-- Gibbs measure is non-negative. -/
  99theorem gibbs_measure_nonneg {Ω : Type*} [Fintype Ω] [Nonempty Ω]
 100    (sys : RecognitionSystem) (X : Ω → ℝ) (ω : Ω) : 0 ≤ gibbs_measure sys X ω := by
 101  unfold gibbs_measure
 102  exact div_nonneg (gibbs_weight_pos sys (X ω)).le (partition_function_pos sys X).le
 103
 104/-- Gibbs measure sums to 1. -/
 105theorem gibbs_measure_sum_one {Ω : Type*} [Fintype Ω] [Nonempty Ω]
 106    (sys : RecognitionSystem) (X : Ω → ℝ) : ∑ ω, gibbs_measure sys X ω = 1 := by
 107  unfold gibbs_measure partition_function
 108  rw [← Finset.sum_div]
 109  exact div_self (partition_function_pos sys X).ne'