Theorems · Theorem · real analysis

Real.pi_upper_bound_start

∀ (n : ℕ) {a : ℝ}, 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n → 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.

Defined in

Mathlib.Analysis.Real.Pi.Bounds

Cited by

5 results in Mathlib

Foundations

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