English
A technical derivative formula giving the derivative of the Taylor coefficient, showing how the coefficient changes with the base point within a set when differentiability holds inside the set.
Русский
Техническая формула производной коэффициента Тейлора внутри множества, устанавливающая зависимость коэффициента от базовой точки при условий дифференцирования внутри множества.
LaTeX
$$HasDerivWithinAt( z ↦ (((k+1)! )^{-1} (x - z)^{k+1}) • iteratedDerivWithin(k+1) f s z) = ... (дериватные выражения) t y$$
Lean4
theorem hasDerivWithinAt_taylor_coeff_within {f : ℝ → E} {x y : ℝ} {k : ℕ} {s t : Set ℝ} (ht : UniqueDiffWithinAt ℝ t y)
(hs : s ∈ 𝓝[t] y) (hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y) :
HasDerivWithinAt (fun z => (((k + 1 : ℝ) * k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z)
((((k + 1 : ℝ) * k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
((k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
t y :=
by
replace hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y :=
by
convert (hf.mono_of_mem_nhdsWithin hs).hasDerivWithinAt using 1
rw [iteratedDerivWithin_succ]
exact (derivWithin_of_mem_nhdsWithin hs ht hf).symm
have : HasDerivWithinAt (fun t => ((k + 1 : ℝ) * k !)⁻¹ * (x - t) ^ (k + 1)) (-((k ! : ℝ)⁻¹ * (x - y) ^ k)) t y := by
-- Commuting the factors:
have : -((k ! : ℝ)⁻¹ * (x - y) ^ k) = ((k + 1 : ℝ) * k !)⁻¹ * (-(k + 1) * (x - y) ^ k) := by field_simp
rw [this]
exact (monomial_has_deriv_aux y x _).hasDerivWithinAt.const_mul _
convert this.smul hf using 1
field_simp
rw [neg_smul, sub_eq_add_neg]
