pith. machine review for the scientific record. sign in
theorem proved term proof

superfluid_fraction_between

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

depends on (15)

Lean names referenced from this declaration's body.