English
The Wallis sequence W_k converges to π/2 as k tends to infinity.
Русский
Последовательность Вальлиса W_k сходится к π/2 при бесконечном стремлении k.
LaTeX
$$$\displaystyle \lim_{k \to \infty} W_k = \frac{\pi}{2}$$$
Lean4
theorem tendsto_W_nhds_pi_div_two : Tendsto W atTop (𝓝 <| π / 2) :=
by
refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds le_W W_le
have : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2)) := by rw [sub_zero, one_mul]
rw [this]
refine Tendsto.mul ?_ tendsto_const_nhds
have h : ∀ n : ℕ, ((2 : ℝ) * n + 1) / (2 * n + 2) = 1 - 1 / (2 * n + 2) :=
by
intro n
rw [sub_div'
(ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)),
one_mul]
congr 1; ring
simp_rw [h]
refine (tendsto_const_nhds.div_atTop ?_).const_sub _
refine Tendsto.atTop_add ?_ tendsto_const_nhds
exact tendsto_natCast_atTop_atTop.const_mul_atTop two_pos
