theorem
proved
amati_increases
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.GammaRayBursts on GitHub at line 53.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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