mathlib docs: data.real.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 : ℝ} (h : (↑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 : ℝ} (hz : (↑c / ↑d).sqrt_two_add_series n ≤ z) (hb : 0 < b) (hd : 0 < d) (h : (2 * b + a) * d ^ 2 ≤ (c ^ 2) * b) :

(↑a / ↑b).sqrt_two_add_series (n + 1) ≤ z

source

meta def real.pi_lower_bound (l : 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 : ℝ} (h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrt_two_add_series n) (h₂ : 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 : ℝ} (hz : z ≤ (↑a / ↑b).sqrt_two_add_series n) (hb : 0 < b) (hd : 0 < d) (h : (a ^ 2) * d ≤ (2 * d + c) * b ^ 2) :

z ≤ (↑c / ↑d).sqrt_two_add_series (n + 1)

source

meta def real.pi_upper_bound (l : 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 < π