Verified rational bounds for pi

Rational lower and upper bounds for Real.pi are derived from the Real.sqrtTwoAddSeries approximation, shown to converge, and packaged into a ComputableℝSeq.Pi, giving an IsComputable instance for Real.pi. The bounds go through the noncomputable square-root sequences, so Pi and the derived bounds piLb/piUb are noncomputable Lean terms.

@[implicit_reducible]

noncomputable instance ComputableℝSeq.instComputableSqrtTwoAddSeries (x : ℝ) [hx : IsComputable x] (n : ℕ) : IsComputable (x.sqrtTwoAddSeries n)

Equations

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

noncomputable def ComputableℝSeq.sqrtTwoAddSeriesN : ℕ → ComputableℝSeq

Definition of sqrtTwoAddSeriesN.

Equations

• ComputableℝSeq.sqrtTwoAddSeriesN n = IsComputable.seq (Real.sqrtTwoAddSeries 0 n)

theorem ComputableℝSeq.sqrtTwoAddSeriesN_lb_le (n k : ℕ) : ↑(↑(sqrtTwoAddSeriesN n).lb k) ≤ Real.sqrtTwoAddSeries 0 n

theorem ComputableℝSeq.sqrtTwoAddSeriesN_ub_ge (n k : ℕ) : Real.sqrtTwoAddSeries 0 n ≤ ↑(↑(sqrtTwoAddSeriesN n).ub k)

theorem ComputableℝSeq.sqrtTwoAddSeriesN_ub_pos (n k : ℕ) : 0 ≤ ↑(↑(sqrtTwoAddSeriesN n).ub k)

theorem ComputableℝSeq.sqrtTwoAddSeriesN_lb_lt_two (n k : ℕ) : ↑(sqrtTwoAddSeriesN n).lb k < 2

theorem ComputableℝSeq.sqrtTwoAddSeriesN_succ_lb (n k : ℕ) : ↑(sqrtTwoAddSeriesN (n + 1)).lb k = (Sqrt.sqrtq (2 + (sqrtTwoAddSeriesN n).lub k) k).toProd.1

theorem ComputableℝSeq.sqrtTwoAddSeriesN_succ_ub (n k : ℕ) : ↑(sqrtTwoAddSeriesN (n + 1)).ub k = (Sqrt.sqrtq (2 + (sqrtTwoAddSeriesN n).lub k) k).toProd.2

theorem ComputableℝSeq.sqrtTwoAddSeriesN_lb_nonneg (n k : ℕ) : 0 ≤ ↑(sqrtTwoAddSeriesN n).lb k

theorem ComputableℝSeq.sqrtTwoAddSeriesN_lb_gt_one (n k : ℕ) (hk : 3 ≤ k) : 1 ≤ ↑(sqrtTwoAddSeriesN (n + 1)).lb k

theorem ComputableℝSeq.sqrtTwoAddSeriesN_bounds (n k : ℕ) (hk : 3 ≤ k) : ↑(sqrtTwoAddSeriesN n).ub k ≤ ↑(sqrtTwoAddSeriesN n).lb k + 18 * ↑n / 2 ^ k

noncomputable def ComputableℝSeq.sqrtTwoSubSqrtTwoAddSeriesN : ℕ → ComputableℝSeq

Definition of sqrtTwoSubSqrtTwoAddSeriesN.

Equations

• ComputableℝSeq.sqrtTwoSubSqrtTwoAddSeriesN n = IsComputable.seq √(2 - Real.sqrtTwoAddSeries 0 n)

theorem ComputableℝSeq.sqrtTwoSubSqrtTwoAddSeries_eq (n k : ℕ) : (sqrtTwoSubSqrtTwoAddSeriesN n).lub k = Sqrt.sqrtq ((2 - sqrtTwoAddSeriesN n).lub k) k

theorem ComputableℝSeq.real_sqrtTwoAddSeries_lb (n : ℕ) : 1 / 2 ^ n < √(2 - Real.sqrtTwoAddSeries 0 n)

theorem ComputableℝSeq.sqrtTwoSubSqrtTwoAddSeries_lb (n k : ℕ) (hk : 3 ≤ k) : √(2 - Real.sqrtTwoAddSeries 0 n) ≤ ↑(↑(sqrtTwoSubSqrtTwoAddSeriesN n).lb k) + (18 * ↑n * 2 ^ n + 4) / 2 ^ k

theorem ComputableℝSeq.sqrtTwoSubSqrtTwoAddSeries_ub (n k : ℕ) (hk : 3 ≤ k) : ↑(↑(sqrtTwoSubSqrtTwoAddSeriesN n).ub k) - (18 * ↑n * 2 ^ n + 14) / 2 ^ k ≤ √(2 - Real.sqrtTwoAddSeries 0 n)

noncomputable def ComputableℝSeq.piLb (n : ℕ) : ℚ

See theorem Real.pi_lt_sqrtTwoAddSeries in Mathlib

Equations

• ComputableℝSeq.piLb n = 2 ^ (n + 1) * ↑(ComputableℝSeq.sqrtTwoSubSqrtTwoAddSeriesN n).lb (3 * n)

noncomputable def ComputableℝSeq.piUb (n : ℕ) : ℚ

See theorem Real.pi_gt_sqrtTwoAddSeries in Mathlib

Equations

• ComputableℝSeq.piUb n = 2 ^ (n + 1) * ↑(ComputableℝSeq.sqrtTwoSubSqrtTwoAddSeriesN n).ub (3 * n) + 1 / 4 ^ n

theorem ComputableℝSeq.piLb_le_pi (n : ℕ) : ↑(piLb n) ≤ Real.pi

theorem ComputableℝSeq.piUb_ge_pi (n : ℕ) : Real.pi ≤ ↑(piUb n)

theorem ComputableℝSeq.piLb_ge_pi_sub_pow (n : ℕ) (hn : 0 < n) : Real.pi - 41 * ↑n / 2 ^ n ≤ ↑(piLb n)

theorem ComputableℝSeq.piUb_le_pi_add_pow (n : ℕ) (hn : 0 < n) : ↑(piUb n) ≤ Real.pi + 51 * ↑n / 2 ^ n

theorem ComputableℝSeq.piLb_causeq : ∃ (h' : IsCauSeq abs piLb), Real.mk ⟨piLb, h'⟩ = Real.pi

theorem ComputableℝSeq.piUb_causeq : ∃ (h' : IsCauSeq abs piUb), Real.mk ⟨piUb, h'⟩ = Real.pi

noncomputable def ComputableℝSeq.Pi : ComputableℝSeq

Definition of Pi.

Equations

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

@[implicit_reducible]

noncomputable instance IsComputable.instComputablePi : IsComputable Real.pi

Equations

• IsComputable.instComputablePi = { seq := ComputableℝSeq.Pi, prop := IsComputable.instComputablePi._proof_1 }