def
definition
ly_SI
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.SIConversion on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
58def Mpc_SI : ℝ := 3.0857e22
59
60/-- 1 light-year in meters. -/
61def ly_SI : ℝ := 9.461e15
62
63/-- 1 Gyr (billion years) in seconds. -/
64def Gyr_SI : ℝ := 3.1557e16
65
66theorem planck_length_SI_pos : 0 < planck_length_SI := by
67 unfold planck_length_SI; norm_num
68
69theorem planck_time_SI_pos : 0 < planck_time_SI := by
70 unfold planck_time_SI; norm_num
71
72theorem c_SI_pos : 0 < c_SI := by
73 unfold c_SI; norm_num
74
75theorem Mpc_SI_pos : 0 < Mpc_SI := by
76 unfold Mpc_SI; norm_num
77
78/-! ## Part 2: Conversion Functions -/
79
80/-- Convert a distance from Planck lengths to meters. -/
81def planck_to_meters (r_planck : ℝ) : ℝ := r_planck * planck_length_SI
82
83/-- Convert a time from Planck times to seconds. -/
84def planck_to_seconds (t_planck : ℝ) : ℝ := t_planck * planck_time_SI
85
86/-- Convert a Hubble parameter from 1/t_P to km/s/Mpc.
87 H₀ [1/t_P] × (t_P [s] / Mpc [m]) × (1 km) = H₀ [km/s/Mpc]. -/
88def hubble_to_kms_mpc (h_planck : ℝ) : ℝ :=
89 h_planck * planck_time_SI⁻¹ * (1000 / Mpc_SI)
90
91/-- Convert seconds to Gyr. -/