mathlib3 documentation

data.real.pi.bounds

Pi #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains lemmas which establish bounds on real.pi. Notably, these include pi_gt_sqrt_two_add_series and pi_lt_sqrt_two_add_series, which bound π using series; numerical bounds on π such as pi_gt_314and pi_lt_315 (more precise versions are given, too).

See also data.real.pi.leibniz and data.real.pi.wallis for infinite formulas for π.

theorem real.pi_lt_sqrt_two_add_series (n : ) :
real.pi < 2 ^ (n + 1) * (2 - real.sqrt_two_add_series 0 n) + 1 / 4 ^ n
theorem real.pi_lower_bound_start (n : ) {a : } (h : real.sqrt_two_add_series (0 / 1) n 2 - (a / 2 ^ (n + 1)) ^ 2) :

From an upper bound on sqrt_two_add_series 0 n = 2 cos (π / 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 < π thanks to basic trigonometric inequalities as expressed in pi_gt_sqrt_two_add_series.

theorem real.sqrt_two_add_series_step_up (c d : ) {a b n : } {z : } (hz : real.sqrt_two_add_series (c / d) n z) (hb : 0 < b) (hd : 0 < d) (h : (2 * b + a) * d ^ 2 c ^ 2 * b) :
meta def real.pi_lower_bound (l : list ) :

Create a proof of 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/2^(n+1).

theorem real.pi_upper_bound_start (n : ) {a : } (h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 real.sqrt_two_add_series (0 / 1) n) (h₂ : 1 / 4 ^ n a) :

From a lower bound on sqrt_two_add_series 0 n = 2 cos (π / 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 π < a thanks to basic trigonometric formulas as expressed in pi_lt_sqrt_two_add_series.

theorem real.sqrt_two_add_series_step_down (a b : ) {c d n : } {z : } (hz : z real.sqrt_two_add_series (a / b) n) (hb : 0 < b) (hd : 0 < d) (h : a ^ 2 * d (2 * d + c) * b ^ 2) :
meta def real.pi_upper_bound (l : list ) :

Create a proof of π < 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).

theorem real.pi_gt_314  :
157 / 50 < real.pi
theorem real.pi_lt_315  :
real.pi < 63 / 20
theorem real.pi_gt_31415  :
6283 / 2000 < real.pi
theorem real.pi_lt_31416  :
real.pi < 3927 / 1250
theorem real.pi_gt_3141592  :
392699 / 125000 < real.pi
theorem real.pi_lt_3141593  :
real.pi < 3141593 / 1000000