lorentz_range

formal source

  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
  59/-- Amati exponent 1/2 from Γ ∝ E_iso^(1/4) × √(E_iso) combination. -/
  60theorem amati_exponent : (1:ℝ)/4 + 1/4 = 1/2 := by norm_num
  61
  62/-! ## Key Energy Scale -/
  63
  64/-- GRB isotropic energy: 10^51 to 10^54 erg. -/
  65theorem grb_energy_range :
  66    ∃ E : ℝ, 1e51 < E ∧ E < 1e54 :=
  67  ⟨typical_grb_energy, typical_grb_in_range.1, typical_grb_in_range.2⟩
  68
  69end GRB
  70end Physics
  71end IndisputableMonolith