English
If sqrtTwoAddSeries(0,n) ≤ 2 − (a/2^{n+1})^2, then a < π.
Русский
Если sqrtTwoAddSeries(0,n) ≤ 2 − (a/2^{n+1})^2, то a < π.
LaTeX
$$$\forall n \in \mathbb{N}, \; a \in \mathbb{R}: \ sqrtTwoAddSeries(0,n) \le 2 - (a/2^{n+1})^{2} \implies a < \pi$$$
Lean4
/-- 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`. -/
theorem pi_lower_bound_start (n : ℕ) {a}
(h : sqrtTwoAddSeries ((0 : ℕ) / (1 : ℕ)) n ≤ (2 : ℝ) - (a / (2 : ℝ) ^ (n + 1)) ^ 2) : a < π :=
by
refine lt_of_le_of_lt ?_ (pi_gt_sqrtTwoAddSeries n); rw [mul_comm]
refine (div_le_iff₀ (pow_pos (by simp) _)).mp (le_sqrt_of_sq_le ?_)
rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]
