computable_log

formal source

 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
 268/-- The geometric seed 4π·11 is computable. -/
 269theorem alpha_seed_computable : Computable (4 * Real.pi * 11) := by
 270  have h1 : Computable ((4 : ℕ) : ℝ) := inferInstance
 271  have h2 : Computable Real.pi := pi_computable
 272  have h3 : Computable ((11 : ℕ) : ℝ) := inferInstance
 273  simp only [Nat.cast_ofNat] at h1 h3
 274  exact computable_mul (computable_mul h1 h2) h3
 275
 276/-- ln φ is computable. -/
 277theorem log_phi_computable : Computable (Real.log Constants.phi) := by
 278  have hphi : Computable Constants.phi := phi_computable
 279  have hpos : Constants.phi > 0 := Constants.phi_pos
 280  exact computable_log hphi hpos
 281
 282/-- The curvature term 103/(102π⁵) is computable. -/
 283theorem curvature_computable : Computable ((103 : ℝ) / (102 * Real.pi ^ 5)) := by
 284  have h103 : Computable ((103 : ℕ) : ℝ) := inferInstance
 285  have h102 : Computable ((102 : ℕ) : ℝ) := inferInstance
 286  simp only [Nat.cast_ofNat] at h103 h102
 287  have hpi : Computable Real.pi := pi_computable
 288  have hpi5 : Computable (Real.pi ^ 5) := computable_pow hpi 5
 289  have hdenom : Computable (102 * Real.pi ^ 5) := computable_mul h102 hpi5
 290  have hne : (102 : ℝ) * Real.pi ^ 5 ≠ 0 := by
 291    apply mul_ne_zero