English
A derivative formula for the Taylor evaluation with respect to the variable of evaluation within an arbitrary set, expressing the derivative via iterated derivatives.
Русский
Формула производной оценки Тейлора внутри произвольного множества, выражающая производную через повторные производные.
LaTeX
$$HasDerivWithinAt (fun t => taylorWithinEval f n s t x) ( (n+1)!^{-1} (x - y)^{n} • iteratedDerivWithin(n+1) f s y ) s' y$$
Lean4
/-- Calculate the derivative of the Taylor polynomial with respect to `x₀`.
Version for arbitrary sets -/
theorem hasDerivWithinAt_taylorWithinEval {f : ℝ → E} {x y : ℝ} {n : ℕ} {s s' : Set ℝ} (hs_unique : UniqueDiffOn ℝ s)
(hs' : s' ∈ 𝓝[s] y) (hy : y ∈ s') (h : s' ⊆ s) (hf : ContDiffOn ℝ n f s)
(hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y) :
HasDerivWithinAt (fun t => taylorWithinEval f n s t x)
(((n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y :=
by
have hs'_unique : UniqueDiffWithinAt ℝ s' y :=
UniqueDiffWithinAt.mono_nhds (hs_unique _ (h hy)) (nhdsWithin_le_iff.mpr hs')
induction n with
|
zero =>
simp only [taylor_within_zero_eval, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, mul_one, zero_add,
one_smul]
simp only [iteratedDerivWithin_zero] at hf'
rw [iteratedDerivWithin_one]
exact hf'.hasDerivWithinAt.mono h
| succ k hk =>
simp_rw [Nat.add_succ, taylorWithinEval_succ]
simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
have coe_lt_succ : (k : WithTop ℕ) < k.succ := Nat.cast_lt.2 k.lt_succ_self
have hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s' :=
(hf.differentiableOn_iteratedDerivWithin (mod_cast coe_lt_succ) hs_unique).mono h
specialize hk hf.of_succ ((hdiff y hy).mono_of_mem_nhdsWithin hs')
convert hk.add (hasDerivWithinAt_taylor_coeff_within hs'_unique (nhdsWithin_mono _ h self_mem_nhdsWithin) hf') using
1
exact (add_sub_cancel _ _).symm
