Real.pi_lower_bound_start
theorem Real.pi_lower_bound_start :
∀ (n : ℕ) {a : ℝ}, (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2 → a < Real.pi
The theorem `Real.pi_lower_bound_start` states that for any natural number `n` and any real number `a`, if `a` is an upper bound of the series `sqrtTwoAddSeries 0 n = 2 cos (π / 2 ^ (n+1))` in the form `sqrtTwoAddSeries 0 n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2`, then `a` is less than π. This conclusion is derived thanks to basic trigonometric inequalities as expressed in `pi_gt_sqrtTwoAddSeries`. In other words, given an upper bound on this specific trigonometric series, we can infer a lower bound on π.
More concisely: If `a` is an upper bound of the series `sqrtTwoAddSeries 0 n`, then `a` is strictly less than `π`.
|
Real.pi_upper_bound_start
theorem 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
This theorem states that for any natural number `n` and any real number `a`, if `a` satisfies the inequality `2 - ((a - 1 / 4^n) / 2^(n + 1))^2 ≤ sqrtTwoAddSeries 0 n` (where `sqrtTwoAddSeries 0 n` equals to `2 * cos(π / 2^(n+1))`), and `a` is at least `1 / 4^n`, then it can be deduced that `π` is less than `a`. Essentially, this theorem provides a method to obtain an upper bound for the mathematical constant `π` using basic trigonometric formulas and a series involving square roots.
More concisely: For any natural number `n` and real number `a` satisfying `2 - ((a - 1 / 4^n) / 2^(n + 1))^2 <= 2 * cos(π / 2^(n+1)) and a >= 1 / 4^n`, it holds that `π < a`.
|