two_zpow_pos

proof body

Tactic-mode proof.

  92  positivity
  93
  94/-! ## Classical approximation: every real has fast rational approximations
  95
  96`Real` in Mathlib is constructed as a completion of `ℚ`, so (classically) every
  97real number admits rational approximations at any prescribed precision. This is
  98enough to satisfy our existential `Computable` predicate. -/
  99
 100instance (x : ℝ) : Computable x where
 101  approx := by
 102    classical
 103    refine ⟨fun n => Classical.choose (exists_rat_btwn (a := x - (2 : ℝ) ^ (-(n : ℤ)))
 104      (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by
 105        have hpos : (0 : ℝ) < (2 : ℝ) ^ (-(n : ℤ)) := two_zpow_pos (-(n : ℤ))
 106        linarith)), ?_⟩
 107    intro n
 108    -- Unpack the chosen rational bounds.
 109    have hpos : (0 : ℝ) < (2 : ℝ) ^ (-(n : ℤ)) := two_zpow_pos (-(n : ℤ))
 110    have hbtwn :=
 111      Classical.choose_spec (exists_rat_btwn (a := x - (2 : ℝ) ^ (-(n : ℤ)))
 112        (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith))
 113    -- `hbtwn` gives: x - ε < q and q < x + ε.
 114    have hleft : x - (Classical.choose (exists_rat_btwn (a := x - (2 : ℝ) ^ (-(n : ℤ)))
 115      (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith)) : ℝ) < (2 : ℝ) ^ (-(n : ℤ)) := by
 116      linarith [hbtwn.1]
 117    have hright : -(2 : ℝ) ^ (-(n : ℤ)) < x - (Classical.choose (exists_rat_btwn
 118      (a := x - (2 : ℝ) ^ (-(n : ℤ))) (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith)) : ℝ) := by
 119      linarith [hbtwn.2]
 120    have : |x - (Classical.choose (exists_rat_btwn
 121      (a := x - (2 : ℝ) ^ (-(n : ℤ))) (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith)) : ℝ)|
 122        < (2 : ℝ) ^ (-(n : ℤ)) := by
 123      exact abs_lt.mpr ⟨hright, hleft⟩
 124    simpa using this
 125
 126/-- Natural numbers are trivially computable. -/
 127instance (n : ℕ) : Computable (n : ℝ) where
 128  approx := ⟨fun _ => n, by
 129    intro k
 130    simp only [Rat.cast_natCast, sub_self, abs_zero]
 131    exact two_zpow_pos _⟩
 132
 133/-- Integers are computable. -/
 134instance (n : ℤ) : Computable (n : ℝ) where
 135  approx := ⟨fun _ => n, by
 136    intro k
 137    simp only [Rat.cast_intCast, sub_self, abs_zero]
 138    exact two_zpow_pos _⟩
 139
 140/-- Rationals are computable (constant approximation). -/