ProbabilityDistribution

formal source

 117  · exact partition_function_pos sys X
 118
 119/-- A probability distribution on a discrete set of states. -/
 120structure ProbabilityDistribution (Ω : Type*) [Fintype Ω] where
 121  p : Ω → ℝ
 122  nonneg : ∀ ω, 0 ≤ p ω
 123  sum_one : ∑ ω, p ω = 1
 124
 125/-! ## Entropy and Free Energy -/
 126
 127/-- Recognition Entropy S_R for a probability distribution p.
 128    S_R(p) = -∑_ω p(ω) ln(p(ω))
 129    Convention: 0 * ln(0) = 0 (handled via lim). -/
 130noncomputable def recognition_entropy {Ω : Type*} [Fintype Ω] (p : Ω → ℝ) : ℝ :=
 131  - ∑ ω, if p ω > 0 then p ω * log (p ω) else 0
 132
 133/-- Expected J-cost under a probability distribution p.
 134    E_p[J] = ∑_ω p(ω) * J(X(ω)) -/
 135noncomputable def expected_cost {Ω : Type*} [Fintype Ω] (p : Ω → ℝ) (X : Ω → ℝ) : ℝ :=
 136  ∑ ω, p ω * Jcost (X ω)
 137
 138/-- Recognition Free Energy F_R = E[J] - TR * S_R.
 139    This is the fundamental variational quantity in RS thermodynamics. -/
 140noncomputable def recognition_free_energy {Ω : Type*} [Fintype Ω]
 141    (sys : RecognitionSystem) (p : Ω → ℝ) (X : Ω → ℝ) : ℝ :=
 142  expected_cost p X - sys.TR * recognition_entropy p
 143
 144/-- Alternative formulation: F_R = -TR * ln(Z) for the Gibbs measure. -/
 145noncomputable def free_energy_from_Z {Ω : Type*} [Fintype Ω]
 146    (sys : RecognitionSystem) (X : Ω → ℝ) : ℝ :=
 147  - sys.TR * log (partition_function sys X)
 148
 149/-- **THEOREM: Free Energy Identity**
 150    F_R = -TR * ln(Z) for the Gibbs measure. -/