Sequences, series, summability Series: basic notions Theorem
Leibniz formula for pi
Builds on Alternating series testpi
Statement
The series converges, and
Remarks
The series converges by the alternating series test. Its value comes from the power series of arctangent at , since .
The convergence is very slow. The error after the terms up to is at most .
Mathlib states it as a limit of partial sums, in Real.tendsto_sum_pi_div_four.
History
Madhava of Sangamagrama or his school found the series in the 14th or 15th century. James Gregory found it again in 1671, and Leibniz in 1673.
Reading path
To understand this page from the ground up, read these 59 pages in order. The foundations come first.
- Limit point of a set definition
- Local maximum definition
- Sequence definition
- Limit of a function definition
- Local minimum definition
- Real sequence definition
- Subsequence definition
- Continuity at a point definition
- Derivative definition
- Bounded sequence definition
- Cauchy sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Series definition
- Continuous function definition
- Fermat's theorem on stationary points statement
- Limit superior definition
- Cauchy sequences are bounded statement
- Sum of a finite geometric series statement
- Monotone convergence theorem for sequences statement
- Every sequence has a monotone subsequence statement
- Convergent sequence definition
- Pointwise convergence definition
- Squeeze theorem statement
- Alternating series definition
- Partial sum definition
- Power series definition
- Intermediate value theorem statement
- Bolzano–Weierstrass theorem statement
- The sequence r^n tends to zero for |r| < 1 example
- Alternating series test statement
- Radius of convergence definition
- Uniform convergence definition
- Convergent series definition
- Sine and cosine definition
- Boundedness theorem statement
- Cauchy criterion for sequences statement
- Uniform convergence on a set definition
- Absolute convergence definition
- Series of functions definition
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Sum of a series definition
- Extreme value theorem statement
- Uniformly Cauchy sequence of functions definition
- Geometric series example
- Comparison test statement
- Rolle's theorem statement
- Root test statement
- Weierstrass M-test statement
- Mean value theorem statement
- Cauchy–Hadamard theorem statement
- Power series converge uniformly on smaller discs inside the radius of convergence statement
- Uniform convergence of derivatives allows term-by-term differentiation statement
- Term-by-term differentiation statement
- Power series are differentiable inside the radius of convergence statement
- Derivative of cosine statement
- pi object
- Leibniz formula for pi statement
Where this leads
1 page builds on this one.
Further reading
- Web https://en.wikipedia.org/wiki/Leibniz_formula_for_π, lead section
About this page
| Tag | 037FD5NBRT |
|---|---|
| URI | m2://037FD5NBRT |
| Aliases | madhava-leibniz-series |
| Kind | statement, theorem |
| Writing | W1 stated |
| MSC | 40A05 |
| Status | This copy of the site has no build data. Run m2 status 037FD5NBRT. |
| Uses | Alternating series test, pi |
| Same as |
Markdown · JSON · Edit on GitHub
What this page needs for W2
- edge about out: the concepts that the statement is about (0 of 1)
- edge proves in: at least one proof node (0 of 1)
- edge instance_of or illustrates in: one example that shows the statement at work (0 of 1)
- explanation L2 (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.