---

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