English
The derivative of the monomial (x−t)^(n+1) with respect to y at y=t is −(n+1)·(x−t)^n, reflecting the standard power rule with a shift.
Русский
Производная по y мононима (x−y)^(n+1) в точке y=t равна −(n+1)·(x−t)^n, что соответствует правилу дифференцирования степеней с учётом сдвига.
LaTeX
$$$HasDerivAt\ (\fun y => (x - y)^{(n+1)})\ (- (n+1) \cdot (x - t)^n)\ t$$$
Lean4
/-- Helper lemma for calculating the derivative of the monomial that appears in Taylor
expansions. -/
theorem monomial_has_deriv_aux (t x : ℝ) (n : ℕ) : HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(n + 1) * (x - t) ^ n) t :=
by
simp_rw [sub_eq_neg_add]
rw [← neg_one_mul, mul_comm (-1 : ℝ), mul_assoc, mul_comm (-1 : ℝ), ← mul_assoc]
convert ((hasDerivAt_id t).neg.add_const x).pow (n + 1)
simp only [Nat.cast_add, Nat.cast_one]
