two_zpow_pos

formal source

  88theorem phi_computable : Computable Constants.phi := by infer_instance
  89
  90/-- Helper: 2^n > 0 for any integer n -/
  91lemma two_zpow_pos (n : ℤ) : (0 : ℝ) < (2 : ℝ) ^ n := by
  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)) : ℝ)|