theorem
proved
tactic proof
lambda_point_lt_bec
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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:
72 `T_λ ≈ 2.17 K`. -/