typical_grb_in_range

formal source

  25
  26noncomputable def typical_grb_energy : ℝ := grb_energy 0.1
  27
  28theorem typical_grb_in_range :
  29    1e51 < typical_grb_energy ∧ typical_grb_energy < 1e54 := by
  30  simp only [typical_grb_energy, grb_energy, accretion_efficiency, solar_mass_energy]
  31  norm_num
  32
  33/-! ## Two-Class Distinction -/
  34
  35theorem classes_disjoint (x : ℝ)
  36    (hlong : 2 ≤ x) (hshort : x ≤ 2) : x = 2 := le_antisymm hshort hlong
  37
  38theorem long_not_short (x : ℝ) (hlong : 2 < x) (hshort : x < 2) : False := by linarith
  39
  40/-! ## Lorentz Factor -/
  41
  42theorem lorentz_range : (100 : ℝ) < 1000 := by norm_num
  43
  44noncomputable def lorentz_factor (E_jet M_b : ℝ) : ℝ := E_jet / M_b
  45
  46theorem lorentz_positive (E_jet M_b : ℝ) (hE : 0 < E_jet) (hM : 0 < M_b) :
  47    0 < lorentz_factor E_jet M_b := div_pos hE hM
  48
  49/-! ## Amati Relation -/
  50
  51noncomputable def amati_peak (E_iso C : ℝ) : ℝ := C * E_iso ^ ((0.5 : ℝ))
  52
  53theorem amati_increases (E₁ E₂ C : ℝ) (hE₁ : 0 < E₁) (hC : 0 < C) (h : E₁ < E₂) :
  54    amati_peak E₁ C < amati_peak E₂ C := by
  55  unfold amati_peak
  56  apply mul_lt_mul_of_pos_left _ hC
  57  exact Real.rpow_lt_rpow (le_of_lt hE₁) h (by norm_num)
  58