computable_add

formal source

 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]
 181    exact abs_add_le (x - ↑(f (n + 1))) (y - ↑(g (n + 1)))
 182  have h_sum : |x - ↑(f (n + 1))| + |y - ↑(g (n + 1))| <
 183      (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) + (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) :=
 184    add_lt_add hf' hg'
 185  have h_double : (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) + (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) =
 186      (2 : ℝ) ^ (-(↑n : ℤ)) := by
 187    have h1 : (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) + (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) =
 188        2 * (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) := by ring
 189    rw [h1]
 190    have h2 : (2 : ℝ) * (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) =
 191        (2 : ℝ) ^ (1 : ℤ) * (2 : ℝ) ^ (-(↑(n + 1) : ℤ)) := by norm_num
 192    rw [h2, ← zpow_add₀ (by norm_num : (2 : ℝ) ≠ 0)]
 193    congr 1
 194    omega
 195  linarith [h_tri, h_sum, h_double]
 196