IndisputableMonolith.Relativity.GW.PropagationSpeed

   1import Mathlib
   2import IndisputableMonolith.Relativity.GW.ActionExpansion
   3import IndisputableMonolith.Constants
   4
   5namespace IndisputableMonolith
   6namespace Relativity
   7namespace GW
   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
  42  gw170817_bound : |c_T_squared_RS - 1| < 1e-15
  43
  44theorem GW170817_bound_satisfied [GWObservationalFacts] :
  45  |c_T_squared_RS - 1| < 1e-15 :=
  46  GWObservationalFacts.gw170817_bound
  47
  48theorem c_T_squared_derived :
  49  c_T_squared 0 0 = 1 ∧
  50  (∀ α C_lag, ∃ coeff, c_T_squared α C_lag = 1 + coeff * (α * C_lag)) := by
  51  constructor
  52  · exact c_T_squared_GR_limit
  53  · intro α C_lag
  54    refine ⟨0.01, ?_⟩
  55    simp [c_T_squared]
  56
  57end GW
  58end Relativity
  59end IndisputableMonolith
  60