by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
In the following let \begin{array}{|c|}\hline A=2\ \hline \end{array}\; and P0=q0=23. \ni) Using a PC , find pk and qk for k∈{1,2,3,4,5}. \nii) Show that \n\n pn=F2n(β)=21−β2n1+β2nqn=F5n(β)=21−β5n1+β5n,β:=3+223−22=(2+12−1)2<521. \niii) Prove the inequalities \n 0<p5−2<104210<q5−2<10104161. \nThis means that p5≈2 , both numbers having in common at least 41 decimals. On the other hand, q5 approximate 2 with at least 10415 exact decimals ! \nNote that 2=1.4142135623730950488...
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37686 (a : ℝ)
(p q : ℕ → ℝ)
(h₀ : a = 2)
(h₁ : p 0 = 3 / 2)
(h₂ : q 0 = 3 / 2)
(h₃ : ∀ n, p (n + 1) = 2 * p n ^ 2 - 1)
(h₄ : ∀ n, q (n + 1) = 2 * q n ^ 2 - 1)
(h₅ : 0 < 5)
(h₆ : 0 < 2)
(h₇ : 0 < a)
(h₈ : ∀ n, 0 ≤ p n)
(h₉ : ∀ n, 0 ≤ q n)
(h₁₀ : ∀ n, p n ≤ q n)
(h₁₁ : ∃ β < 1 / 5^2, ∀ n, p n = Real.sqrt 2 * (1 + β^(2^n)) / (1 - β^(2^n)))
(h₁₂ : ∃ β < 1 / 5^2, ∀ n, q n = Real.sqrt 2 * (1 + β^(5^n)) / (1 - β^(5^n)))
(h₁₃ : 0 < p 5 - Real.sqrt 2)
(h₁₄ : 0 < q 5 - Real.sqrt 2)
(h₁₅ : p 5 - Real.sqrt 2 < 1 / 10^42)
(h₁₆ : q 5 - Real.sqrt 2 < 1 / 10^10416) :
|p 5 - Real.sqrt 2| < 1 / 10^42 ∧ |q 5 - Real.sqrt 2| < 1 / 10^10416 := by sorry