beta_lin

formal source

  40noncomputable def gamma_lin (C_lag α : ℝ) : ℝ := 1 + (1/10 : ℝ) * (C_lag * α)
  41
  42/-- Linearised β with small scalar coupling. -/
  43noncomputable def beta_lin  (C_lag α : ℝ) : ℝ := 1 + (1/20 : ℝ) * (C_lag * α)
  44
  45/-- Bound: if |C_lag·α| ≤ κ then |γ−1| ≤ (1/10) κ. -/
  46theorem gamma_bound_small (C_lag α κ : ℝ)
  47  (h : |C_lag * α| ≤ κ) :
  48  |gamma_lin C_lag α - 1| ≤ (1/10 : ℝ) * κ := by
  49  unfold gamma_lin
  50  simp only [add_sub_cancel_left]
  51  rw [abs_mul]
  52  calc |1/10| * |C_lag * α| = (1/10) * |C_lag * α| := by norm_num
  53    _ ≤ (1/10) * κ := by exact mul_le_mul_of_nonneg_left h (by norm_num)
  54
  55/-- Bound: if |C_lag·α| ≤ κ then |β−1| ≤ (1/20) κ. -/
  56theorem beta_bound_small (C_lag α κ : ℝ)
  57  (h : |C_lag * α| ≤ κ) :
  58  |beta_lin C_lag α - 1| ≤ (1/20 : ℝ) * κ := by
  59  unfold beta_lin
  60  simp only [add_sub_cancel_left]
  61  rw [abs_mul]
  62  calc |1/20| * |C_lag * α| = (1/20) * |C_lag * α| := by norm_num
  63    _ ≤ (1/20) * κ := by exact mul_le_mul_of_nonneg_left h (by norm_num)
  64
  65end PPN
  66end ILG
  67end Relativity
  68end IndisputableMonolith