Pi

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

See also Mathlib/Data/Real/Pi/Leibniz.lean and Mathlib/Data/Real/Pi/Wallis.lean for infinite formulas for π.

theorem Real.pi_gt_sqrtTwoAddSeries (n : ℕ) : 2 ^ (n + 1) * √(2 - Real.sqrtTwoAddSeries 0 n) < Real.pi

theorem Real.pi_lt_sqrtTwoAddSeries (n : ℕ) : Real.pi < 2 ^ (n + 1) * √(2 - Real.sqrtTwoAddSeries 0 n) + 1 / 4 ^ n

theorem Real.pi_lower_bound_start (n : ℕ) {a : ℝ} (h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2) : a < Real.pi

From an upper bound on sqrtTwoAddSeries 0 n = 2 cos (π / 2 ^ (n+1)) of the form sqrtTwoAddSeries 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_sqrtTwoAddSeries.

theorem Real.sqrtTwoAddSeries_step_up (c : ℕ) (d : ℕ) {a : ℕ} {b : ℕ} {n : ℕ} {z : ℝ} (hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z) (hb : 0 < b) (hd : 0 < d) (h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b) : (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ z

def Real.«tacticPi_lower_bound[_,,]» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

theorem Real.pi_upper_bound_start (n : ℕ) {a : ℝ} (h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n) (h₂ : 1 / 4 ^ n ≤ a) : Real.pi < a

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

theorem Real.sqrtTwoAddSeries_step_down (a : ℕ) (b : ℕ) {c : ℕ} {d : ℕ} {n : ℕ} {z : ℝ} (hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n) (hb : 0 < b) (hd : 0 < d) (h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2) : z ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)

def Real.«tacticPi_upper_bound[_,,]» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

theorem Real.pi_gt_three : 3 < Real.pi

theorem Real.pi_gt_314 : 3.14 < Real.pi

theorem Real.pi_lt_315 : Real.pi < 3.15

theorem Real.pi_gt_31415 : 3.1415 < Real.pi

theorem Real.pi_lt_31416 : Real.pi < 3.1416

theorem Real.pi_gt_3141592 : 3.141592 < Real.pi

theorem Real.pi_lt_3141593 : Real.pi < 3.141593