twoLevelSystem

formal source

 250/-! ## Examples -/
 251
 252/-- A two-level system (qubit). -/
 253def twoLevelSystem (gap : ℝ) : System := {
 254  levels := [
 255    ⟨0, 1, by norm_num⟩,      -- Ground state
 256    ⟨gap, 1, by norm_num⟩     -- Excited state
 257  ],
 258  nonempty := by norm_num
 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))