English
For every n ≠ 0, the identity (stirlingSeq(n))^4 / (stirlingSeq(2n))^2 · (n/(2n+1)) = W_n holds, relating Stirling sequence to Wallis product.
Русский
Для каждого n ≠ 0 выполняется тождество (stirlingSeq(n))^4 / (stirlingSeq(2n))^2 · (n/(2n+1)) = W_n, связывающее последовательности Стирлинга и Уоллиса.
LaTeX
$$$$ \forall n\in\mathbb{N},\ n\neq 0 \Rightarrow \frac{\mathrm{stirlingSeq}(n)^4}{\mathrm{stirlingSeq}(2n)^2} \cdot \frac{n}{2n+1} = W_n. $$$$
Lean4
/-- For any `n ≠ 0`, we have the identity
`(stirlingSeq n)^4 / (stirlingSeq (2*n))^2 * (n / (2 * n + 1)) = W n`, where `W n` is the
`n`-th partial product of Wallis' formula for `π / 2`. -/
theorem stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq (n : ℕ) (hn : n ≠ 0) :
stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (n / (2 * n + 1)) = Wallis.W n :=
by
have : 4 = 2 * 2 := by rfl
rw [stirlingSeq, this, pow_mul, stirlingSeq, Wallis.W_eq_factorial_ratio]
simp_rw [div_pow, mul_pow]
rw [sq_sqrt, sq_sqrt]
any_goals positivity
simp [field, ← exp_nsmul]
ring_nf
