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

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

    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
      ];
      
      @[deprecated Real.pi_gt_d2]
      theorem Real.pi_gt_314 :
      3.14 < Real.pi

      Alias of Real.pi_gt_d2.

      @[deprecated Real.pi_lt_d2]
      theorem Real.pi_lt_315 :
      Real.pi < 3.15

      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