massive_star_more_luminous

formal source

  92  simp
  93
  94/-- More massive stars are much more luminous. -/
  95theorem massive_star_more_luminous (M : ℝ) (hM : 1 < M) :
  96    1 < luminosity_scaling M := by
  97  unfold luminosity_scaling
  98  have h1 : (1 : ℝ) = 1 ^ (3.9 : ℝ) := (Real.one_rpow _).symm
  99  rw [h1]
 100  exact Real.rpow_lt_rpow (by norm_num) hM (by norm_num)
 101
 102/-! ## Main Sequence Lifetime -/
 103
 104/-- **MAIN SEQUENCE LIFETIME**: t_MS = ε_H X M / L ∝ M^(1-3.9) = M^(-2.9)
 105    where X ≈ 0.7 is hydrogen mass fraction, ε_H = 0.007 c². -/
 106noncomputable def ms_lifetime (M : ℝ) : ℝ :=
 107  nuclear_efficiency * 0.7 * M / luminosity_scaling M
 108
 109/-- Lifetime decreases with mass (massive stars burn out faster). -/
 110theorem lifetime_decreases (M₁ M₂ : ℝ) (hM₁ : 1 < M₁) (h : M₁ < M₂) :
 111    ms_lifetime M₂ < ms_lifetime M₁ := by
 112  unfold ms_lifetime luminosity_scaling nuclear_efficiency
 113  have hM₁pos : 0 < M₁ := by linarith
 114  have hM₂pos : 0 < M₂ := by linarith
 115  have hpow : M₁ ^ (2.9 : ℝ) < M₂ ^ (2.9 : ℝ) :=
 116    Real.rpow_lt_rpow (le_of_lt hM₁pos) h (by norm_num)
 117  have hpow₁_pos : 0 < M₁ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₁pos _
 118  have hpow₂_pos : 0 < M₂ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₂pos _
 119  have hrecip : 1 / M₂ ^ (2.9 : ℝ) < 1 / M₁ ^ (2.9 : ℝ) :=
 120    one_div_lt_one_div_of_lt hpow₁_pos hpow
 121  have hconst : 0 < (7e-3 : ℝ) * 0.7 := by
 122    norm_num
 123  have hrewrite₁ : (7e-3 : ℝ) * 0.7 * M₁ / M₁ ^ (3.9 : ℝ) =
 124      (7e-3 : ℝ) * 0.7 / M₁ ^ (2.9 : ℝ) := by
 125    rw [show (3.9 : ℝ) = 1 + 2.9 by norm_num, Real.rpow_add hM₁pos, Real.rpow_one]