Pi

This file contains lemmas which establish bounds on or approximations of real.pi. Notably, these include pi_gt_sqrt_two_add_series and pi_lt_sqrt_two_add_series, which bound pi using series; numerical bounds on pi such as pi_gt_314and pi_lt_315 (more precise versions are given, too); and tendsto_sum_pi_div_four, Leibniz's series for pi.

source

theorem real.pi_gt_sqrt_two_add_series (n : ℕ) :

(2 ^ (n + 1)) * real.sqrt (2 - 0.sqrt_two_add_series n) < π

source

theorem real.pi_lt_sqrt_two_add_series (n : ℕ) :

π < (2 ^ (n + 1)) * real.sqrt (2 - 0.sqrt_two_add_series n) + 1 / 4 ^ n

source

theorem real.pi_lower_bound_start (n : ℕ) {a : ℝ} :

(↑0 / ↑1).sqrt_two_add_series n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2 → a < π

From an upper bound on sqrt_two_add_series 0 n = 2 cos (pi / 2 ^ (n+1)) of the form sqrt_two_add_series 0 n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2), one can deduce the lower bound a < pi thanks to basic trigonometric inequalities as expressed in pi_gt_sqrt_two_add_series.

source

theorem real.sqrt_two_add_series_step_up (c d : ℕ) {a b n : ℕ} {z : ℝ} :

(↑c / ↑d).sqrt_two_add_series n ≤ z → 0 < b → 0 < d → (2 * b + a) * d ^ 2 ≤ (c ^ 2) * b → (↑a / ↑b).sqrt_two_add_series (n + 1) ≤ z

source

meta def real.pi_lower_bound :

list ℚ → tactic unit

Create a proof of a < pi for a fixed rational number a, given a witness, which is a sequence of rational numbers sqrt 2 < r 1 < r 2 < ... < r n < 2 satisfying the property that sqrt (2 + r i) ≤ r(i+1), where r 0 = 0 and sqrt (2 - r n) ≥ a/2^(n+1).

source

theorem real.pi_upper_bound_start (n : ℕ) {a : ℝ} :

2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrt_two_add_series n → 1 / 4 ^ n ≤ a → π < a

From a lower bound on sqrt_two_add_series 0 n = 2 cos (pi / 2 ^ (n+1)) of the form 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrt_two_add_series 0 n, one can deduce the upper bound pi < a thanks to basic trigonometric formulas as expressed in pi_lt_sqrt_two_add_series.

source

theorem real.sqrt_two_add_series_step_down (a b : ℕ) {c d n : ℕ} {z : ℝ} :

z ≤ (↑a / ↑b).sqrt_two_add_series n → 0 < b → 0 < d → (a ^ 2) * d ≤ (2 * d + c) * b ^ 2 → z ≤ (↑c / ↑d).sqrt_two_add_series (n + 1)

source

meta def real.pi_upper_bound :

list ℚ → tactic unit

Create a proof of pi < a for a fixed rational number a, given a witness, which is a sequence of rational numbers sqrt 2 < r 1 < r 2 < ... < r n < 2 satisfying the property that sqrt (2 + r i) ≥ r(i+1), where r 0 = 0 and sqrt (2 - r n) ≥ (a - 1/4^n) / 2^(n+1).

source

theorem real.pi_gt_three :

3 < π

source

theorem real.pi_gt_314 :

157 / 50 < π

source

theorem real.pi_lt_315 :

π < 63 / 20

source

theorem real.pi_gt_31415 :

6283 / 2000 < π

source

theorem real.pi_lt_31416 :

π < 3927 / 1250

source

theorem real.pi_gt_3141592 :

392699 / 125000 < π

source

theorem real.pi_lt_3141593 :

π < 3141593 / 1000000

Leibniz's Series for Pi

source

theorem real.tendsto_sum_pi_div_four :

filter.tendsto (λ (k : ℕ), ∑ (i : ℕ) in finset.range k, (-1) ^ i / (2 * ↑i + 1)) filter.at_top (𝓝 (π / 4))

This theorem establishes Leibniz's series for π: The alternating sum of the reciprocals of the odd numbers is π/4. Note that this is a conditionally rather than absolutely convergent series. The main tool that this proof uses is the Mean Value Theorem (specifically avoiding the Fundamental Theorem of Calculus).

Intuitively, the theorem holds because Leibniz's series is the Taylor series of arctan x centered about 0 and evaluated at the value x = 1. Therefore, much of this proof consists of reasoning about a function f := arctan x - ∑ i in finset.range k, (-(1:ℝ))^i * x^(2*i+1) / (2*i+1), the difference between arctan and the k-th partial sum of its Taylor series. Some ingenuity is required due to the fact that the Taylor series is not absolutely convergent at x = 1.

This proof requires a bound on f 1, the key idea being that f 1 can be split as the sum of f 1 - f u and f u, where u is a sequence of values in [0,1], carefully chosen such that each of these two terms can be controlled (in different ways).

We begin the proof by (1) introducing that sequence u and then proving that another sequence constructed from u tends to 0 at +∞. After (2) converting the limit in our goal to an inequality, we (3) introduce the auxiliary function f defined above. Next, we (4) compute the derivative of f, denoted by f', first generally and then on each of two subintervals of [0,1]. We then (5) prove a bound for f', again both generally as well as on each of the two subintervals. Finally, we (6) apply the Mean Value Theorem twice, obtaining bounds on f 1 - f u and f u - f 0 from the bounds on f' (note that f 0 = 0).