bec_temperature_positive

formal source

  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) :
  58    lambda_point T_BEC a_s n < T_BEC := by
  59  unfold lambda_point
  60  have hn3 : (0 : ℝ) < n ^ ((1:ℝ)/3) := Real.rpow_pos_of_pos hn _
  61  have hcorr_pos : 0 < 0.43 * a_s * n ^ ((1:ℝ)/3) := by positivity
  62  -- T_BEC * (1 - 0.43 * ...) < T_BEC iff 0 < T_BEC * (0.43 * ...)
  63  have hkey : lambda_point T_BEC a_s n = T_BEC - T_BEC * (0.43 * a_s * n ^ ((1:ℝ)/3)) := by
  64    simp [lambda_point]; ring
  65  linarith [mul_pos hT hcorr_pos, hkey.symm.le]
  66
  67/-- A calibrated He-4 λ-point estimate.
  68
  69    The raw `lambda_point` formula is dimensionful, and this file does not carry
  70    the unit normalization needed to insert the physical He-4 density directly.
  71    We therefore record the standard normalized estimate used by the paper: