English
Let n be a natural number and a a real number. If 2 − ((a − 1/4^n)/2^{n+1})^2 ≤ sqrtTwoAddSeries(0, n) and (1/4^n) ≤ a, then π < a.
Русский
Пусть n ∈ ℕ и a ∈ ℝ. Если 2 − ((a − 4^{−n})/2^{n+1})^2 ≤ sqrtTwoAddSeries(0, n) и 4^{-n} ≤ a, то π < a.
LaTeX
$$$\\forall n\\in\\mathbb{N},\\; a\\in\\mathbb{R},\\; \\Big(2 - \\left(\\frac{a - 4^{-n}}{2^{\,n+1}}\\right)^{2} \\le sqrtTwoAddSeries(0, n)\\Big) \\land \\left(4^{-n} \\le a\\right) \\Rightarrow \\pi < a.$$
Lean4
/-- 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 pi_upper_bound_start (n : ℕ) {a}
(h : (2 : ℝ) - ((a - 1 / (4 : ℝ) ^ n) / (2 : ℝ) ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries ((0 : ℕ) / (1 : ℕ)) n)
(h₂ : (1 : ℝ) / (4 : ℝ) ^ n ≤ a) : π < a :=
by
refine lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) ?_
rw [← le_sub_iff_add_le, ← le_div_iff₀', sqrt_le_left, sub_le_comm]
· rwa [Nat.cast_zero, zero_div] at h
· exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)
· exact pow_pos zero_lt_two _
