computable_add

proof body

Tactic-mode proof.

 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
 197/-- Computable reals are closed under subtraction.
 198    Using x - y = x + (-y) and computable_neg and computable_add. -/