 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) -/
 261theorem computable_log {x : ℝ} (hx : Computable x) (hpos : x > 0) :
 262    Computable (Real.log x) := by
 263  -- Immediate from the global classical instance.
 264  infer_instance
 265
 266/-! ## RS Constants Are Computable -/
 267

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.