superfluid_fraction

formal source

 114  · exact Real.log_pos (by norm_num)
 115
 116/-- Superfluid fraction: ρ_s(T)/ρ = 1 - (T/Tlam)^α. -/
 117noncomputable def superfluid_fraction (T Tlam : ℝ) : ℝ :=
 118  1 - (T / Tlam) ^ rs_critical_exponent
 119
 120/-- At T = 0, fully superfluid. -/
 121theorem superfluid_fraction_at_zero (Tlam : ℝ) (hTlam : 0 < Tlam) :
 122    superfluid_fraction 0 Tlam = 1 := by
 123  unfold superfluid_fraction
 124  simp [Real.zero_rpow (ne_of_gt rs_critical_exponent_positive)]
 125
 126/-- At T = Tlam, normal fluid. -/
 127theorem superfluid_fraction_at_lambda (Tlam : ℝ) (hTlam : 0 < Tlam) :
 128    superfluid_fraction Tlam Tlam = 0 := by
 129  unfold superfluid_fraction
 130  simp [div_self (ne_of_gt hTlam), Real.one_rpow]
 131
 132/-- For 0 < T < Tlam, fraction is strictly between 0 and 1. -/
 133theorem superfluid_fraction_between (T Tlam : ℝ) (hT : 0 < T)
 134    (hTlam : 0 < Tlam) (h : T < Tlam) :
 135    0 < superfluid_fraction T Tlam ∧ superfluid_fraction T Tlam < 1 := by
 136  unfold superfluid_fraction
 137  have hratio : 0 < T / Tlam := div_pos hT hTlam
 138  have hratio_lt : T / Tlam < 1 := (div_lt_one hTlam).mpr h
 139  have hα := rs_critical_exponent_positive
 140  have hpow_lt : (T / Tlam) ^ rs_critical_exponent < 1 :=
 141    Real.rpow_lt_one hratio.le hratio_lt hα
 142  have hpow_pos : 0 < (T / Tlam) ^ rs_critical_exponent :=
 143    Real.rpow_pos_of_pos hratio _
 144  constructor <;> linarith
 145
 146/-! ## He-3 Superfluid -/
 147