---

Step * 2 of Lemma fun-converges-to-derivative


1. I : Interval
2. iproper(I)
3. f : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. F : I ⟶ℝ
6. G : I ⟶ℝ
7. ∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y]))
8. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
9. lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
10. ∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I
11. r : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))
⊢ d(F[x])/dx = λx.G[x] on I
BY
{ ((InstLemma `fun-converges-to-integral` [⌜I⌝;⌜f'⌝;⌜G⌝;⌜r⌝]⋅
    THENA (Try (Complete (Auto))
           THEN ParallelOp -2
           THEN Auto
           THEN MemTypeHD (-4)
           THEN Try (Unhide)
           THEN All Reduce
           THEN Auto)
    )
   THEN (Assert λx.G[x] ∈ {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))}  BY
               (MemTypeCD THEN Reduce 0 THEN Auto))
   THEN (Assert d(r_∫-x G[t] dt)/dx = λx.G[x] on I BY
               (BLemma `derivative-of-integral` THEN Auto))) }

1
1. I : Interval
2. iproper(I)
3. f : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. F : I ⟶ℝ
6. G : I ⟶ℝ
7. ∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y]))
8. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
9. lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
10. ∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I
11. r : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))
14. lim n→∞.r_∫-x f'[n;t] dt = λx.r_∫-x G[t] dt for x ∈ I
15. λx.G[x] ∈ {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} 
16. d(r_∫-x G[t] dt)/dx = λx.G[x] on I
⊢ d(F[x])/dx = λx.G[x] on I

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  \mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}
4.  f'  :  \mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}
5.  F  :  I  {}\mrightarrow{}\mBbbR{}
6.  G  :  I  {}\mrightarrow{}\mBbbR{}
7.  \mforall{}n:\mBbbN{}.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[n;x]  =  f'[n;y]))
8.  lim  n\mrightarrow{}\minfty{}.f[n;x]  =  \mlambda{}y.F[y]  for  x  \mmember{}  I
9.  lim  n\mrightarrow{}\minfty{}.f'[n;x]  =  \mlambda{}y.G[y]  for  x  \mmember{}  I
10.  \mforall{}n:\mBbbN{}.  d(f[n;x])/dx  =  \mlambda{}x.f'[n;x]  on  I
11.  r  :  \mBbbR{}
12.  r  \mmember{}  I
13.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (G[x]  =  G[y]))
\mvdash{}  d(F[x])/dx  =  \mlambda{}x.G[x]  on  I


By

---

Latex:
((InstLemma  `fun-converges-to-integral`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
    THENA  (Try  (Complete  (Auto))
                  THEN  ParallelOp  -2
                  THEN  Auto
                  THEN  MemTypeHD  (-4)
                  THEN  Try  (Unhide)
                  THEN  All  Reduce
                  THEN  Auto)
    )
  THEN  (Assert  \mlambda{}x.G[x]  \mmember{}  \{f:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\}    BY
                          (MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  d(r\_\mint{}\msupminus{}x  G[t]  dt)/dx  =  \mlambda{}x.G[x]  on  I  BY
                          (BLemma  `derivative-of-integral`  THEN  Auto)))

---

Home Index