c_T_squared

formal source

   8
   9open Cosmology
  10
  11noncomputable def c_T_squared (α C_lag : ℝ) : ℝ :=
  12  1 + 0.01 * (α * C_lag)
  13
  14theorem c_T_squared_GR_limit :
  15  c_T_squared 0 0 = 1 := by
  16  simp [c_T_squared]
  17
  18noncomputable def c_T_squared_RS : ℝ :=
  19  c_T_squared ((1 - 1/Constants.phi)/2) (Constants.phi ^ (-5 : ℝ))
  20
  21theorem c_T_squared_near_one (α C_lag : ℝ) (h_α : |α| < 0.3) (h_C : |C_lag| < 0.2) :
  22  |c_T_squared α C_lag - 1| < 0.01 := by
  23  simp [c_T_squared]
  24  -- Goal: |0.01 * (α * C_lag)| < 0.01
  25  calc |0.01 * (α * C_lag)|
  26      = 0.01 * |α * C_lag| := by simp [abs_mul]; norm_num
  27    _ = 0.01 * |α| * |C_lag| := by rw [abs_mul]
  28    _ < 0.01 * 0.3 * 0.2 := by
  29        apply mul_lt_mul
  30        · apply mul_lt_mul
  31          · norm_num
  32          · exact h_α
  33          · exact abs_nonneg α
  34          · norm_num
  35        · exact h_C
  36        · exact abs_nonneg C_lag
  37        · apply mul_pos; norm_num; norm_num
  38    _ = 0.006 := by norm_num
  39    _ < 0.01 := by norm_num
  40
  41class GWObservationalFacts : Prop where