baryon_loading_decreasing

formal source

  30noncomputable def baryon_loading (R₀ z : ℝ) : ℝ := R₀ / (1 + z)
  31
  32/-- Baryon loading decreases with redshift (photons more dominant at high z). -/
  33theorem baryon_loading_decreasing (R₀ : ℝ) (hR : 0 < R₀) (z₁ z₂ : ℝ)
  34    (hz₁ : -1 < z₁) (hz₂ : -1 < z₂) (h : z₁ < z₂) :
  35    baryon_loading R₀ z₂ < baryon_loading R₀ z₁ := by
  36  unfold baryon_loading
  37  apply div_lt_div_of_pos_left (by linarith) (by linarith) (by linarith)
  38
  39/-- **SOUND SPEED**: c_s = c/√(3(1+R))
  40    In units c=1: c_s = 1/√(3(1+R)). -/
  41noncomputable def sound_speed (R : ℝ) : ℝ := 1 / Real.sqrt (3 * (1 + R))
  42
  43/-- Sound speed is positive for R ≥ 0. -/
  44theorem sound_speed_positive (R : ℝ) (hR : -1 < R) :
  45    0 < sound_speed R := by
  46  unfold sound_speed
  47  apply div_pos one_pos
  48  apply Real.sqrt_pos_of_pos
  49  linarith
  50
  51/-- In the limit R → 0 (radiation dominated): c_s → c/√3. -/
  52theorem sound_speed_radiation_limit :
  53    sound_speed 0 = 1 / Real.sqrt 3 := by
  54  unfold sound_speed
  55  norm_num
  56
  57/-- Sound speed decreases with R (more baryons → slower sound). -/
  58theorem sound_speed_decreasing (R₁ R₂ : ℝ) (hR₁ : -1 < R₁) (hR₂ : -1 < R₂) (h : R₁ < R₂) :
  59    sound_speed R₂ < sound_speed R₁ := by
  60  unfold sound_speed
  61  apply div_lt_div_of_pos_left one_pos
  62  · apply Real.sqrt_pos_of_pos; linarith
  63  · apply Real.sqrt_lt_sqrt