Step
*
of Lemma
derivative-Taylor-approx
∀I:Interval
(iproper(I)
⇒ (∀n:ℕ. ∀F:ℕn + 2 ⟶ I ⟶ℝ. ∀b:{a:ℝ| a ∈ I} .
((∀k:ℕn + 2. ∀x,y:{a:ℝ| a ∈ I} . ((x = y)
⇒ (F[k;x] = F[k;y])))
⇒ finite-deriv-seq(I;n + 1;i,x.F[i;x])
⇒ d(Taylor-approx(n;a;b;i,x.F[i;x]))/da = λx.b - x^n * (F[n + 1;x]/r((n)!)) on I)))
BY
{ TACTIC:(Auto THEN Unfold `Taylor-approx` 0) }
1
1. I : Interval
2. iproper(I)
3. n : ℕ
4. F : ℕn + 2 ⟶ I ⟶ℝ
5. b : {a:ℝ| a ∈ I}
6. ∀k:ℕn + 2. ∀x,y:{a:ℝ| a ∈ I} . ((x = y)
⇒ (F[k;x] = F[k;y]))
7. finite-deriv-seq(I;n + 1;i,x.F[i;x])
⊢ d(Σ{(F[k;a]/r((k)!)) * b - a^k | 0≤k≤n})/da = λx.b - x^n * (F[n + 1;x]/r((n)!)) on I
Latex:
Latex:
\mforall{}I:Interval
(iproper(I)
{}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mforall{}F:\mBbbN{}n + 2 {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{}. \mforall{}b:\{a:\mBbbR{}| a \mmember{} I\} .
((\mforall{}k:\mBbbN{}n + 2. \mforall{}x,y:\{a:\mBbbR{}| a \mmember{} I\} . ((x = y) {}\mRightarrow{} (F[k;x] = F[k;y])))
{}\mRightarrow{} finite-deriv-seq(I;n + 1;i,x.F[i;x])
{}\mRightarrow{} d(Taylor-approx(n;a;b;i,x.F[i;x]))/da = \mlambda{}x.b - x\^{}n * (F[n + 1;x]/r((n)!)) on I)))
By
Latex:
TACTIC:(Auto THEN Unfold `Taylor-approx` 0)
Home
Index