computable_div

formal source

 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
 245    exact h
 246  | succ n ih =>
 247    simp only [pow_succ]
 248    exact computable_mul ih hx
 249
 250/-- ln is computable on positive reals.
 251
 252    **Proof approach**: Use argument reduction + Taylor series.
 253    1. Find k such that x·2^(-k) ∈ [1/2, 2] (k = ⌊log₂(x)⌋)
 254    2. Let y = x·2^(-k), so log(x) = log(y) + k·log(2)
 255    3. Use log(y) = 2·arctanh((y-1)/(y+1)) for y ∈ [1/2, 2]
 256    4. arctanh(z) = z + z³/3 + z⁵/5 + ... converges for |z| < 1
 257
 258    For y ∈ [1/2, 2], we have |(y-1)/(y+1)| ≤ 1/3, giving fast convergence.
 259
 260    **Status**: Axiom (Taylor series algorithm) -/