rational_computable

formal source

 138    exact two_zpow_pos _⟩
 139
 140/-- Rationals are computable (constant approximation). -/
 141instance rational_computable (q : ℚ) : Computable (q : ℝ) where
 142  approx := ⟨fun _ => q, by
 143    intro k
 144    simp only [sub_self, abs_zero]
 145    exact two_zpow_pos _⟩
 146
 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)