theorem
proved
gamma_bound_small
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.ILG.PPN on GitHub at line 46.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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