theorem
proved
tactic proof
gamma_bound_small
show as:
view Lean formalization →
formal statement (Lean)
46theorem gamma_bound_small (C_lag α κ : ℝ)
47 (h : |C_lag * α| ≤ κ) :
48 |gamma_lin C_lag α - 1| ≤ (1/10 : ℝ) * κ := by
proof body
Tactic-mode proof.
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) κ. -/