Theorems · Theorem · real analysis

Real.pi_lower_bound_start

∀ (n : ℕ) {a : ℝ}, (↑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.

Defined in

Mathlib.Analysis.Real.Pi.Bounds

Cited by

5 results in Mathlib

Foundations

Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound