def
definition
accretion_efficiency
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 18.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
15/-! ## GRB Energy Scale -/
16
17noncomputable def solar_mass_energy : ℝ := 1.8e54
18noncomputable def accretion_efficiency : ℝ := 0.1
19
20noncomputable def grb_energy (M_frac : ℝ) : ℝ :=
21 accretion_efficiency * M_frac * solar_mass_energy
22
23theorem grb_energy_positive (M_frac : ℝ) (hM : 0 < M_frac) : 0 < grb_energy M_frac := by
24 unfold grb_energy accretion_efficiency solar_mass_energy; positivity
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