`probability`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.BoltzmannDistribution
domain: Thermodynamics
line: 121 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Thermodynamics.BoltzmannDistribution on GitHub at line 121.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 118/-! ## Probability Distribution -/
 119
 120/-- The probability of finding the system in level i. -/
 121noncomputable def probability (sys : System) (beta : ℝ) (i : Fin sys.levels.length) : ℝ :=
 122  let level := sys.levels.get i
 123  boltzmannFactor level beta / partitionFunction sys beta
 124
 125/-- **THEOREM**: Probabilities are non-negative. -/
 126theorem prob_nonneg (sys : System) (beta : ℝ) (hb : beta > 0) (i : Fin sys.levels.length) :
 127    probability sys beta i ≥ 0 := by
 128  unfold probability boltzmannFactor
 129  apply div_nonneg
 130  · apply mul_nonneg
 131    · exact Nat.cast_nonneg _
 132    · exact (exp_pos _).le
 133  · exact (partition_positive sys beta hb).le
 134
 135/-- Helper: Finset.sum over Fin equals List.sum when mapped. -/
 136lemma finset_sum_eq_list_sum_aux (l : List EnergyLevel) (f : EnergyLevel → ℝ) :
 137    Finset.sum Finset.univ (fun i : Fin l.length => f (l.get i)) = (l.map f).sum := by
 138  induction l with
 139  | nil => simp
 140  | cons hd tl ih =>
 141    simp only [List.map_cons, List.sum_cons, List.length_cons, List.get_eq_getElem]
 142    rw [Fin.sum_univ_succ]
 143    simp only [Fin.val_zero, List.getElem_cons_zero, Fin.val_succ, List.getElem_cons_succ]
 144    simp only [List.get_eq_getElem] at ih
 145    rw [ih]
 146
 147lemma finset_sum_eq_list_sum (sys : System) (f : EnergyLevel → ℝ) :
 148    Finset.sum Finset.univ (fun i : Fin sys.levels.length => f (sys.levels.get i)) =
 149    (sys.levels.map f).sum :=
 150  finset_sum_eq_list_sum_aux sys.levels f
 151

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.