def
definition
lorentz_factor
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.GammaRayBursts on GitHub at line 44.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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