module module

`IndisputableMonolith.Physics.CMBTemperature`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (22)

def ionization_energy_eV L28
def kB_eV_per_K L31
def rs_eta L34
abbrev recombination_temperature_K L43
theorem recombination_temperature_positive L46
theorem recombination_energy_approx_eV L50
abbrev rs_recombination_redshift L59
theorem recombination_redshift_positive L62
def cmb_temperature L68
theorem cmb_temperature_positive L71
def rs_cmb_temperature L78
theorem rs_cmb_approx_2725 L82
theorem rs_cmb_consistent_with_firas L91
def planck_radiance L98
theorem planck_positive L102
theorem cmb_is_planck_spectrum L111
def first_acoustic_peak_ell L122
def acoustic_peak L125
theorem acoustic_peaks_positive L127
theorem acoustic_peak_positions L133
theorem cmb_temperature_scales_with_redshift L141
theorem cmb_temperature_now L149