153theorem prob_normalized (sys : System) (beta : ℝ) (hb : beta > 0) : 154 (Finset.univ.sum fun i => probability sys beta i) = 1 := by
proof body
Tactic-mode proof.
155 unfold probability 156 simp only [div_eq_mul_inv] 157 rw [← Finset.sum_mul] 158 have hz : partitionFunction sys beta ≠ 0 := (partition_positive sys beta hb).ne' 159 -- Sum of Boltzmann factors = partition function (by definition) 160 have hsum : Finset.sum Finset.univ (fun i : Fin sys.levels.length => 161 boltzmannFactor (sys.levels.get i) beta) = partitionFunction sys beta := by 162 unfold partitionFunction 163 exact finset_sum_eq_list_sum sys (fun l => boltzmannFactor l beta) 164 rw [hsum] 165 exact mul_inv_cancel₀ hz 166 167/-! ## The J-Cost Connection -/ 168 169/-- The J-cost of an energy level. 170 J(E) measures the "cost" of having that energy relative to the ground state. 171 Here we use a normalized version: J(E/E_0) where E_0 is a reference energy. -/
depends on (32)
Lean names referenced from this declaration's body.