planck_positive

formal source

  99  2 * ν ^ 3 / (Real.exp (ν / T) - 1)   -- in natural units hbar=c=kB=1
 100
 101/-- Planck spectrum is positive for T > 0, ν > 0. -/
 102theorem planck_positive (ν T : ℝ) (hν : 0 < ν) (hT : 0 < T) :
 103    0 < planck_radiance ν T := by
 104  unfold planck_radiance
 105  apply div_pos
 106  · positivity
 107  · have harg : 0 < ν / T := div_pos hν hT
 108    linarith [Real.one_lt_exp_iff.mpr harg]
 109
 110/-- CMB photons follow the Planck spectrum at T = T₀. -/
 111theorem cmb_is_planck_spectrum (ν : ℝ) (hν : 0 < ν) :
 112    0 < planck_radiance ν rs_cmb_temperature := by
 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. -/
 122def first_acoustic_peak_ell : ℝ := 220
 123
 124/-- Peak positions scale as ℓ_n ≈ n × 220. -/
 125noncomputable def acoustic_peak (n : ℕ) : ℝ := n * first_acoustic_peak_ell
 126
 127theorem acoustic_peaks_positive (n : ℕ) (hn : 0 < n) :
 128    0 < acoustic_peak n := by
 129  unfold acoustic_peak first_acoustic_peak_ell
 130  positivity
 131
 132/-- Second peak at ℓ₂ ≈ 540, third at ℓ₃ ≈ 810. -/