theorem
proved
superfluid_fraction_between
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.Superfluidity on GitHub at line 133.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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