pith. machine review for the scientific record. sign in
theorem proved term proof

cmb_is_planck_spectrum

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

formal statement (Lean)

 111theorem cmb_is_planck_spectrum (ν : ℝ) (hν : 0 < ν) :
 112    0 < planck_radiance ν rs_cmb_temperature := by

proof body

Term-mode proof.

 113  apply planck_positive ν rs_cmb_temperature hν
 114  unfold rs_cmb_temperature cmb_temperature
 115    recombination_temperature_K rs_recombination_redshift
 116  norm_num
 117
 118/-! ## CMB Anisotropy Peaks -/
 119
 120/-- First CMB acoustic peak position: ℓ₁ ≈ π/θ_s ≈ π/r_s × D_A(z*).
 121    For standard ΛCDM: ℓ₁ ≈ 220. -/

depends on (7)

Lean names referenced from this declaration's body.