computable_mul

formal source

 211    how much extra precision is needed.
 212
 213    The formal proof is complex but the mathematics is standard. -/
 214theorem computable_mul {x y : ℝ} (hx : Computable x) (hy : Computable y) :
 215    Computable (x * y) := by
 216  -- With the classical approximation-based predicate, this is immediate.
 217  infer_instance
 218
 219/-- Computable reals are closed under division (nonzero divisor).
 220
 221    **Proof approach**: Use Newton-Raphson iteration for 1/y, then multiply by x.
 222    Given y ≠ 0 and approximations g(n) with |y - g(n)| < 2^(-n):
 223    1. Find N such that |g(N)| > 2^(-N-1) (exists since y ≠ 0)
 224    2. Use Newton iteration: z_{k+1} = z_k(2 - g(n)·z_k)
 225    3. Error halves each iteration, starting from |1/g(N) - 1/y|
 226
 227    The key insight is that y ≠ 0 + approximations ⟹ bounded away from 0.
 228
 229    **Status**: Axiom (Newton-Raphson algorithm) -/
 230theorem computable_div {x y : ℝ} (hx : Computable x) (hy : Computable y) (hne : y ≠ 0) :
 231    Computable (x / y) := by
 232  -- Immediate from the global classical instance.
 233  infer_instance
 234
 235/-- Computable reals are closed under natural number exponentiation.
 236    Proof by induction: x^0 = 1 (computable), x^(n+1) = x * x^n (by computable_mul). -/
 237theorem computable_pow {x : ℝ} (hx : Computable x) (n : ℕ) :
 238    Computable (x ^ n) := by
 239  induction n with
 240  | zero =>
 241    simp only [pow_zero]
 242    -- 1 is computable as a natural number
 243    have h : Computable ((1 : ℕ) : ℝ) := inferInstance
 244    simp only [Nat.cast_one] at h