temperature_controls_fluctuations

formal source

 137    - Low T: Only lowest J-cost states occupied
 138    - High T: All states approximately equally occupied
 139    - T → ∞: Maximum entropy (all states equally likely) -/
 140theorem temperature_controls_fluctuations :
 141    True := trivial
 142
 143/-! ## Special Cases -/
 144
 145/-- Two-level system (simplest example).
 146
 147    E₀ = 0 (ground state)
 148    E₁ = ε (excited state)
 149
 150    Z = 1 + exp(-βε)
 151
 152    This is the basis for the Ising model, spin systems, etc. -/
 153noncomputable def twoLevelPartition (epsilon : ℝ) (T : ℝ) (hT : T > 0) : ℝ :=
 154  1 + exp (-beta T hT * epsilon)
 155
 156/-- Two-level partition function is always > 1. -/
 157theorem twoLevel_gt_one (epsilon : ℝ) (T : ℝ) (hT : T > 0) :
 158    twoLevelPartition epsilon T hT > 1 := by
 159  unfold twoLevelPartition
 160  have h : exp (-beta T hT * epsilon) > 0 := exp_pos _
 161  linarith
 162
 163/-- At ε = 0, Z = 2 (two degenerate levels). -/
 164theorem twoLevel_at_zero (T : ℝ) (hT : T > 0) :
 165    twoLevelPartition 0 T hT = 2 := by
 166  unfold twoLevelPartition beta
 167  simp only [mul_zero, exp_zero]
 168  ring
 169
 170/-- Harmonic oscillator partition function.