English
From a lower bound on sqrtTwoAddSeries(0, n) of the form 2 − ((a − 4^{−n})/2^{n+1})^2 ≤ sqrtTwoAddSeries(0, n) and a ≥ 4^{−n}, we conclude π < a.
Русский
Из нижней границы sqrtTwoAddSeries(0, n) имеет вид 2 − ((a − 4^{−n})/2^{n+1})^2 ≤ sqrtTwoAddSeries(0, n) и a ≥ 4^{−n}, следует π < a.
LaTeX
$$$\\forall n\\in\\mathbb{N}, \\; a\\in\\mathbb{R},\\; \\Big(2 - \\left(\\frac{a - 4^{-n}}{2^{n+1}}\\right)^2 \\le sqrtTwoAddSeries(0, n)\\Big) \\land \\left(4^{-n} \\le a\\right) \\Rightarrow \\pi < a.$$$
Lean4
theorem pi_gt_d6 : 3.141592 < π := by
-- bound[3141592*^-6, Iters -> 10, Rounding -> .8, Precision -> 16]
pi_lower_bound [11482 / 8119, 7792 / 4217, 54055 / 27557, 2 - 623 / 64690, 2 - 337 / 139887, 2 - 208 / 345307,
2 - 167 / 1108925, 2 - 64 / 1699893, 2 - 31 / 3293535, 2 - 48 / 20398657]
