English
catalan(n) = centralBinom(n) / (n+1).
Русский
catalan(n) = центральный биномиал(n) / (n+1).
LaTeX
$$$ catalan(n) = \\dfrac{n\\text{ centralBinom}}{n+1} $$$
Lean4
theorem catalan_eq_centralBinom_div (n : ℕ) : catalan n = n.centralBinom / (n + 1) :=
by
suffices (catalan n : ℚ) = Nat.centralBinom n / (n + 1)
by
have h := Nat.succ_dvd_centralBinom n
exact mod_cast this
induction n using Nat.caseStrongRecOn with
| zero => simp
| ind d hd =>
simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) * (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
· congr
ext1 x
have m_le_d : x.val ≤ d := by omega
have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
rw [hd _ m_le_d, hd _ d_minus_x_le_d]
norm_cast
· trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
· refine sum_congr rfl fun i _ => ?_
rw [gosper_trick i.is_le, mul_div]
· rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i, sum_range_sub,
Nat.succ_eq_add_one]
rw [gosper_catalan_sub_eq_central_binom_div d]
norm_cast
