be_occupation_positive

formal source

  24  1 / (Real.exp ((ε - μ) / T) - 1)
  25
  26/-- BE occupation is positive when ε > μ. -/
  27theorem be_occupation_positive (ε μ T : ℝ) (hT : 0 < T) (hεμ : μ < ε) :
  28    0 < be_occupation ε μ T := by
  29  unfold be_occupation
  30  apply div_pos one_pos
  31  have harg : 0 < (ε - μ) / T := div_pos (by linarith) hT
  32  linarith [Real.one_lt_exp_iff.mpr harg]
  33
  34/-! ## BEC Critical Temperature -/
  35
  36/-- BEC temperature for an ideal Bose gas. In natural units. -/
  37noncomputable def bec_temperature (m n : ℝ) : ℝ :=
  38  (2 * Real.pi / m) * (n / 2.612) ^ ((2:ℝ)/3)
  39
  40/-- BEC temperature is positive. -/
  41theorem bec_temperature_positive (m n : ℝ) (hm : 0 < m) (hn : 0 < n) :
  42    0 < bec_temperature m n := by
  43  unfold bec_temperature
  44  apply mul_pos
  45  · positivity
  46  · apply Real.rpow_pos_of_pos; positivity
  47
  48/-! ## λ-point from Van der Waals Interactions -/
  49
  50/-- λ-point: T_lambda ≈ T_BEC × (1 - c₁ aₛ n^(1/3)) -/
  51noncomputable def lambda_point (T_BEC a_s n : ℝ) : ℝ :=
  52  T_BEC * (1 - 0.43 * a_s * n ^ ((1:ℝ)/3))
  53
  54/-- λ-point < T_BEC when interaction correction < 1. -/
  55theorem lambda_point_lt_bec (T_BEC a_s n : ℝ)
  56    (hT : 0 < T_BEC) (ha : 0 < a_s) (hn : 0 < n)
  57    (hsmall : 0.43 * a_s * n ^ ((1:ℝ)/3) < 1) :