theorem
proved
term proof
computable_pow
show as:
view Lean formalization →
formal statement (Lean)
237theorem computable_pow {x : ℝ} (hx : Computable x) (n : ℕ) :
238 Computable (x ^ n) := by
proof body
Term-mode proof.
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) -/