coeff_shiftedLegendre — Mathlib

English

The k-th coefficient of shiftedLegendre n is (-1)^k * C(n,k) * C(n+k, n).

Русский

k-й коэффициент shiftedLegendre n равен (-1)^k * C(n,k) * C(n+k, n).

LaTeX

$$$\\mathrm{shiftedLegendre}(n).\\mathrm{coeff}(k) = (-1)^k \\cdot {n \\choose k} \\cdot {n+k \\choose n}$$$

Lean4

/-- The coefficient of the shifted Legendre polynomial at `k` is
`(-1) ^ k * (n.choose k) * (n + k).choose n`. -/
theorem coeff_shiftedLegendre (n k : ℕ) : (shiftedLegendre n).coeff k = (-1) ^ k * n.choose k * (n + k).choose n :=
  by
  rw [shiftedLegendre, finset_sum_coeff]
  simp_rw [coeff_C_mul_X_pow]
  simp +contextual [choose_eq_zero_of_lt, add_one_le_iff]

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