Fungrim home page

Fungrim entry: 4c0698

1π(12k=0N1(1)k(6k)!(13591409+545140134k)(3k)!(k!)36403203k+3/2)<1151931373056000N\left|\frac{1}{\pi} - \left(12 \sum_{k=0}^{N - 1} \frac{{\left(-1\right)}^{k} \left(6 k\right)! \left(13591409 + 545140134 k\right)}{\left(3 k\right)! {\left(k !\right)}^{3} {640320}^{3 k + 3 / 2}}\right)\right| \lt \frac{1}{{151931373056000}^{N}}
Assumptions:NZ0N \in \mathbb{Z}_{\ge 0}
TeX:
\left|\frac{1}{\pi} - \left(12 \sum_{k=0}^{N - 1} \frac{{\left(-1\right)}^{k} \left(6 k\right)! \left(13591409 + 545140134 k\right)}{\left(3 k\right)! {\left(k !\right)}^{3} {640320}^{3 k + 3 / 2}}\right)\right| \lt \frac{1}{{151931373056000}^{N}}

N \in \mathbb{Z}_{\ge 0}
Definitions:
Fungrim symbol Notation Short description
Absz\left|z\right| Absolute value
ConstPiπ\pi The constant pi (3.14...)
Powab{a}^{b} Power
Factorialn!n ! Factorial
ZZGreaterEqualZn\mathbb{Z}_{\ge n} Integers greater than or equal to n
Source code for this entry:
Entry(ID("4c0698"),
    Formula(Less(Abs(Sub(Div(1, ConstPi), Parentheses(Mul(12, Sum(Div(Mul(Mul(Pow(-1, k), Factorial(Mul(6, k))), Add(13591409, Mul(545140134, k))), Mul(Mul(Factorial(Mul(3, k)), Pow(Factorial(k), 3)), Pow(640320, Add(Mul(3, k), Div(3, 2))))), Tuple(k, 0, Sub(N, 1))))))), Div(1, Pow(151931373056000, N)))),
    Variables(N),
    Assumptions(Element(N, ZZGreaterEqual(0))))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2019-06-18 07:49:59.356594 UTC