theorem
proved
tactic proof
computable_neg
show as:
view Lean formalization →
formal statement (Lean)
150theorem computable_neg {x : ℝ} (hx : Computable x) : Computable (-x) := by
proof body
Tactic-mode proof.
151 obtain ⟨f, hf⟩ := hx.approx
152 constructor
153 use fun n => -f n
154 intro n
155 simp only [Rat.cast_neg]
156 have h := hf n
157 calc |(-x) - (-(f n : ℝ))|
158 = |-(x - f n)| := by ring_nf
159 _ = |x - f n| := abs_neg _
160 _ < (2 : ℝ) ^ (-(↑n : ℤ)) := h
161
162/-- Computable reals are closed under addition.
163 Given approximations f, g with |x - f(n)| < 2^(-n), |y - g(n)| < 2^(-n),
164 we approximate x+y by h(n) = f(n+1) + g(n+1):
165 |x+y - h(n)| ≤ |x - f(n+1)| + |y - g(n+1)| < 2^(-(n+1)) + 2^(-(n+1)) = 2^(-n). -/