English
As in dvd_degree', there exists m with hf.degree * q^m = f.natDegree.
Русский
Как и в dvd_degree', существует m такое, что hf.degree · q^m = f.natDegree.
LaTeX
$$$\\exists m:\\mathbb{N}, hf.degree \\cdot q^m = f.natDegree$$$
Lean4
/-- The shifted Legendre polynomial multiplied by a factorial equals the higher-order derivative of
the combinatorial function `X ^ n * (1 - X) ^ n`. This is the analogue of Rodrigues' formula for
the shifted Legendre polynomials. -/
theorem factorial_mul_shiftedLegendre_eq (n : ℕ) :
(n ! : ℤ[X]) * (shiftedLegendre n) = derivative^[n] (X ^ n * (1 - (X : ℤ[X])) ^ n) :=
by
symm
calc
_ = derivative^[n] (((X : ℤ[X]) - X ^ 2) ^ n) := by rw [← mul_pow, mul_one_sub, ← pow_two]
_ = derivative^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) :=
by
congr
rw [sub_eq_add_neg, add_comm, add_pow]
congr! 1 with m hm
rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc, ← pow_add, ←
mul_assoc, nsmul_eq_mul, add_comm]
rw [Finset.mem_range] at hm
linarith
_ = ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x :=
by
rw [iterate_derivative_sum]
congr! 1 with x _
rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp, iterate_derivative_C_mul,
iterate_derivative_X_pow_eq_smul, descFactorial_eq_div (by cutsat), show n + x - n = x by cutsat]
simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast, Int.cast_pow, Int.cast_neg,
Int.cast_one, zsmul_eq_mul]
ring
_ = ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i :=
by
congr! 2 with x _
rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x), mul_assoc]
congr 1
rw [add_comm, add_choose]
simp only [Int.natCast_ediv, cast_mul, eq_intCast]
norm_cast
rw [mul_comm, ← Nat.mul_div_assoc]
· rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
· simp only [factorial_mul_factorial_dvd_factorial_add]
_ = (n ! : ℤ[X]) * (shiftedLegendre n) := by simp [← mul_assoc, shiftedLegendre, mul_sum]
