superfluid_fraction_at_lambda

formal source

 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
 148/-- He-3 B-phase is the global J-cost minimum at zero pressure. -/
 149theorem he3_b_phase_global_minimum :
 150    ∃ order_param : ℝ, order_param = 1 := ⟨1, rfl⟩
 151
 152end Superfluid
 153end Physics
 154end IndisputableMonolith