groundStateProb

formal source

 259}
 260
 261/-- Ground state probability for a two-level system. -/
 262noncomputable def groundStateProb (gap : ℝ) (beta : ℝ) : ℝ :=
 263  1 / (1 + Real.exp (-beta * gap))
 264
 265/-- At β = 0, the ground state probability is exactly 0.5. -/
 266theorem high_temp_value (gap : ℝ) :
 267    groundStateProb gap 0 = 0.5 := by
 268  unfold groundStateProb
 269  simp
 270  norm_num
 271
 272/-- **THEOREM**: At high temperature (small β), states are equally populated.
 273    Proof: groundStateProb is continuous and groundStateProb(0) = 0.5.
 274
 275    The rigorous proof uses continuity of the composition of continuous functions. -/
 276theorem high_temp_limit (gap : ℝ) (_hg : gap > 0) :
 277    Filter.Tendsto (groundStateProb gap) (nhds 0) (nhds 0.5) := by
 278  rw [← high_temp_value gap]
 279  unfold groundStateProb
 280  -- Use continuity: the function is a composition of continuous functions
 281  have hcont : Continuous (fun beta : ℝ => 1 / (1 + Real.exp (-beta * gap))) := by
 282    refine Continuous.div continuous_const ?_ (fun x => ?_)
 283    · exact continuous_const.add (Real.continuous_exp.comp (continuous_neg.mul continuous_const))
 284    · have : 1 + Real.exp (-x * gap) > 0 := add_pos_of_pos_of_nonneg one_pos (exp_pos _).le
 285      exact this.ne'
 286  exact hcont.continuousAt.tendsto
 287
 288/-- **THEOREM**: At low temperature (large β), ground state dominates.
 289    Proof: As β → ∞, exp(-β*gap) → 0 (for gap > 0), so prob → 1/(1+0) = 1
 290
 291    Uses Real.tendsto_exp_neg_atTop_nhds_zero. -/
 292theorem low_temp_limit (gap : ℝ) (hg : gap > 0) :