HepLean Documentation

Mathlib.Data.Real.Pi.Bounds

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_d2 and pi_lt_d2 (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) :

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

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) :

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_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.

Instances For

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.

Instances For

The below witnesses were generated using the following Mathematica script:

bound[a_, Iters -> n_, Rounding -> extra_, Precision -> prec_] := Module[{r0, r, r2, diff, sign},
  On[Assert];
  sign = If[a >= \[Pi], Print["upper"]; 1, Print["lower"]; -1];
  r0 = 2 - ((a - (sign + 1)/2/4^n)/2^(n + 1))^2;
  r = Log[2 - NestList[#^2 - 2 &, N[r0, prec], n - 1]];
  diff = (r[[-1]] - Log[2 - Sqrt[2]])/(Length[r] + 1);
  If[sign diff <= 0, Return["insufficient iterations"]];
  r2 = Log[Rationalize[Exp[#], extra (Exp[#] - Exp[# - sign diff])] &
    /@ (r - diff Range[1, Length[r]])];
  Assert[sign (2 - Exp@r2[[1]] - r0) >= 0];
  Assert[And @@ Table[
    sign (Sqrt@(4 - Exp@r2[[i + 1]]) - (2 - Exp@r2[[i]])) >= 0, {i, 1, Length[r2] - 1}]];
  Assert[sign (Exp@r2[[-1]] - (2 - Sqrt[2])) >= 0];
  With[{s1 = ToString@InputForm[2 - #], s2 = ToString@InputForm[#]},
    If[StringLength[s1] <= StringLength[s2] + 2, s1, "2-" <> s2]] & /@ Exp@Reverse@r2
];

theorem Real.pi_gt_three :

theorem Real.pi_lt_four :

theorem Real.pi_gt_d2 :

@[deprecated Real.pi_gt_d2]

theorem Real.pi_gt_314 :

Alias of Real.pi_gt_d2.

theorem Real.pi_lt_d2 :

@[deprecated Real.pi_lt_d2]

theorem Real.pi_lt_315 :

Alias of Real.pi_lt_d2.

theorem Real.pi_gt_d4 :

3.1415 < Real.pi

@[deprecated Real.pi_gt_d4]

theorem Real.pi_gt_31415 :

3.1415 < Real.pi

Alias of Real.pi_gt_d4.

theorem Real.pi_lt_d4 :

Real.pi < 3.1416

@[deprecated Real.pi_lt_d4]

theorem Real.pi_lt_31416 :

Real.pi < 3.1416

Alias of Real.pi_lt_d4.

theorem Real.pi_gt_d6 :

3.141592 < Real.pi

@[deprecated Real.pi_gt_d6]

theorem Real.pi_gt_3141592 :

3.141592 < Real.pi

Alias of Real.pi_gt_d6.

theorem Real.pi_lt_d6 :

Real.pi < 3.141593

@[deprecated Real.pi_lt_d6]

theorem Real.pi_lt_3141593 :

Real.pi < 3.141593

Alias of Real.pi_lt_d6.

theorem Real.pi_gt_d20 :

3.14159265358979323846 < Real.pi

theorem Real.pi_lt_d20 :

Real.pi < 3.14159265358979323847