W_eq_factorial_ratio — Mathlib

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

Похожие утверждения