pith. machine review for the scientific record. sign in
theorem proved tactic proof

beta_bound_small

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  56theorem beta_bound_small (C_lag α κ : ℝ)
  57  (h : |C_lag * α| ≤ κ) :
  58  |beta_lin C_lag α - 1| ≤ (1/20 : ℝ) * κ := by

proof body

Tactic-mode proof.

  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

depends on (2)

Lean names referenced from this declaration's body.