English
Wallis's product at index n equals a rational expression involving factorials: W(n) = 2^{4n} (n!)^4 / ((2n)!)^2 (2n+1).
Русский
Произведение Уоллиса имеет вид 2^{4n} (n!)^4 / ((2n)!)^2 (2n+1).
LaTeX
$$W(n) = \\frac{2^{4n} (n!)^{4}}{((2n)!)^{2} (2n+1)}$$
Lean4
theorem W_eq_factorial_ratio (n : ℕ) : W n = 2 ^ (4 * n) * n ! ^ 4 / ((2 * n)! ^ 2 * (2 * n + 1)) := by
induction n with
| zero =>
simp only [W, prod_range_zero, Nat.factorial_zero, mul_zero, pow_zero]
norm_num
| succ n IH =>
unfold W at IH ⊢
rw [prod_range_succ, IH, _root_.div_mul_div_comm, _root_.div_mul_div_comm]
refine (div_eq_div_iff ?_ ?_).mpr ?_
any_goals exact ne_of_gt (by positivity)
simp_rw [Nat.mul_succ, Nat.factorial_succ, pow_succ]
push_cast
ring_nf