computable_neg

formal source

 147/-! ## Closure Properties -/
 148
 149/-- Negation is computable: approximate -x by -f(n). -/
 150theorem computable_neg {x : ℝ} (hx : Computable x) : Computable (-x) := by
 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). -/
 166theorem computable_add {x y : ℝ} (hx : Computable x) (hy : Computable y) :
 167    Computable (x + y) := by
 168  obtain ⟨f, hf⟩ := hx.approx
 169  obtain ⟨g, hg⟩ := hy.approx
 170  constructor
 171  use fun n => f (n + 1) + g (n + 1)
 172  intro n
 173  have hf' := hf (n + 1)
 174  have hg' := hg (n + 1)
 175  simp only [Rat.cast_add]
 176  have h_tri : |x + y - (↑(f (n + 1)) + ↑(g (n + 1)))| ≤
 177      |x - ↑(f (n + 1))| + |y - ↑(g (n + 1))| := by
 178    have heq : x + y - (↑(f (n + 1)) + ↑(g (n + 1))) =
 179        (x - ↑(f (n + 1))) + (y - ↑(g (n + 1))) := by ring
 180    rw [heq]