Proof of Nuprl Lemma : Taylor-remainder-as-integral

Step * 2 2 2 2 1 2 2 2 1 2 1 2 2 2 2 1 1 1 1 1 1 1 of Lemma Taylor-remainder-as-integral

1. I : Interval
2. iproper(I)
3. a : {a:ℝ| a ∈ I}
4. b : {a:ℝ| a ∈ I}
5. [rmin(a;b), rmax(a;b)] ⊆ I
6. n : ℤ
7. 0 < n
8. ∀F:ℕ(n - 1) + 2 ⟶ I ⟶ℝ
     ((∀k:ℕ(n - 1) + 2. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (F[k;x] = F[k;y])))
     ⇒ finite-deriv-seq(I;(n - 1) + 1;i,x.F[i;x])
     ⇒

 (Taylor-remainder(I;n - 1;b;a;k,x.F[k;x]) = a_∫^-b (F[(n - 1) + 1;t]/r((n - 1)!)) * b - t^n - 1 dt))

9. F : ℕn + 2 ⟶ I ⟶ℝ
10. ∀k:ℕn + 2. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (F[k;x] = F[k;y]))
11. finite-deriv-seq(I;n + 1;i,x.F[i;x])

12. λt.((F[n + 1;t]/r((n)!)) * b - t^n) ∈ {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])}

13. a_∫^-b (F[n + 1;t]/r((n)!)) * b - t^n dt = a_∫^-b (b - t^n/r((n)!)) * F[n + 1;t] dt
14. ∀n:ℕ. (λt.(b - t^n/r((n)!)) ∈ {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} )
15. λt.F[n + 1;t] ∈ {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))}
16. λt.F[n;t] ∈ {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))}
17. λt.(r(-1) * (b - t^n - 1/r((n - 1)!))) ∈ {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))}

18. λt.((r(-1) * (b - t^n - 1/r((n - 1)!))) * F[n;t]) ∈ {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])}

19. X : ℝ
20. a_∫^-b (b - t^n/r((n)!)) * F[n + 1;t] dt = X ∈ ℝ
21. Y : ℝ
22. a_∫^-b (F[n;t]/r((n - 1)!)) * b - t^n - 1 dt = Y ∈ ℝ
23. Z : ℝ
24. a_∫^-b (r(-1) * (b - t^n - 1/r((n - 1)!))) * F[n;t] dt = Z ∈ ℝ
25. Z = (r(-1) * Y)
26. X = (((b - b^n/r((n)!)) * F[n;b]) - (b - a^n/r((n)!)) * F[n;a] - Z)
27. ((b - b^n/r((n)!)) * F[n;b]) = r0
28. Taylor-remainder(I;n - 1;b;a;k,x.F[k;x]) = Y
29. v : ℝ
30. ((b - a^n/r((n)!)) * F[n;a]) = v ∈ ℝ
31. v1 : ℝ
32. Taylor-approx(n;a;b;k,x.F[k;x]) = v1 ∈ ℝ
33. v2 : ℝ
34. Taylor-approx(n - 1;a;b;k,x.F[k;x]) = v2 ∈ ℝ
35. v3 : ℝ
36. F[0;b] = v3 ∈ ℝ
⊢ v = (v1 - v2)
BY
{ ((Assert v1 = Taylor-approx(n;a;b;k,x.F[k;x]) BY
          Auto)
   THEN Unfold `Taylor-approx` -1
   THEN (RWO "rsum-split-last" (-1) THENA Auto)) }

1
1. I : Interval
2. iproper(I)
3. a : {a:ℝ| a ∈ I}
4. b : {a:ℝ| a ∈ I}
5. [rmin(a;b), rmax(a;b)] ⊆ I
6. n : ℤ
7. 0 < n
8. ∀F:ℕ(n - 1) + 2 ⟶ I ⟶ℝ
     ((∀k:ℕ(n - 1) + 2. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (F[k;x] = F[k;y])))
     ⇒ finite-deriv-seq(I;(n - 1) + 1;i,x.F[i;x])
     ⇒

 (Taylor-remainder(I;n - 1;b;a;k,x.F[k;x]) = a_∫^-b (F[(n - 1) + 1;t]/r((n - 1)!)) * b - t^n - 1 dt))

9. F : ℕn + 2 ⟶ I ⟶ℝ
10. ∀k:ℕn + 2. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (F[k;x] = F[k;y]))
11. finite-deriv-seq(I;n + 1;i,x.F[i;x])

12. λt.((F[n + 1;t]/r((n)!)) * b - t^n) ∈ {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])}

18. λt.((r(-1) * (b - t^n - 1/r((n - 1)!))) * F[n;t]) ∈ {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])}

Latex:

Latex:
1. I : Interval 2. iproper(I) 3. a : \{a:\mBbbR{}| a \mmember{} I\} 4. b : \{a:\mBbbR{}| a \mmember{} I\} 5. [rmin(a;b), rmax(a;b)] \msubseteq{} I 6. n : \mBbbZ{} 7. 0 < n 8. \mforall{}F:\mBbbN{}(n - 1) + 2 {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{} ((\mforall{}k:\mBbbN{}(n - 1) + 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) + 1;i,x.F[i;x]) {}\mRightarrow{} (Taylor-remainder(I;n - 1;b;a;k,x.F[k;x]) = a\_\mint{}\msupminus{}b (F[(n - 1) + 1;t]/r((n - 1)!)) * b - t\^{}n - 1 dt)) 9. F : \mBbbN{}n + 2 {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{} 10. \mforall{}k:\mBbbN{}n + 2. \mforall{}x,y:\{a:\mBbbR{}| a \mmember{} I\} . ((x = y) {}\mRightarrow{} (F[k;x] = F[k;y])) 11. finite-deriv-seq(I;n + 1;i,x.F[i;x]) 12. \mlambda{}t.((F[n + 1;t]/r((n)!)) * b - t\^{}n) \mmember{} \{f:[rmin(a;b), rmax(a;b)] {}\mrightarrow{}\mBbbR{}| ifun(f;[rmin(a;b), rmax(a;b)])\} 13. a\_\mint{}\msupminus{}b (F[n + 1;t]/r((n)!)) * b - t\^{}n dt = a\_\mint{}\msupminus{}b (b - t\^{}n/r((n)!)) * F[n + 1;t] dt 14. \mforall{}n:\mBbbN{}. (\mlambda{}t.(b - t\^{}n/r((n)!)) \mmember{} \{h:I {}\mrightarrow{}\mBbbR{}| \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} ((h x) = (h y)))\} ) 15. \mlambda{}t.F[n + 1;t] \mmember{} \{h:I {}\mrightarrow{}\mBbbR{}| \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} ((h x) = (h y)))\} 16. \mlambda{}t.F[n;t] \mmember{} \{h:I {}\mrightarrow{}\mBbbR{}| \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} ((h x) = (h y)))\} 17. \mlambda{}t.(r(-1) * (b - t\^{}n - 1/r((n - 1)!))) \mmember{} \{h:I {}\mrightarrow{}\mBbbR{}| \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} ((h x) = (h y)))\} 18. \mlambda{}t.((r(-1) * (b - t\^{}n - 1/r((n - 1)!))) * F[n;t]) \mmember{} \{f:[rmin(a;b), rmax(a;b)] {}\mrightarrow{}\mBbbR{}| ifun(f;[rmin(a;b), rmax(a;b)])\} 19. X : \mBbbR{} 20. a\_\mint{}\msupminus{}b (b - t\^{}n/r((n)!)) * F[n + 1;t] dt = X 21. Y : \mBbbR{} 22. a\_\mint{}\msupminus{}b (F[n;t]/r((n - 1)!)) * b - t\^{}n - 1 dt = Y 23. Z : \mBbbR{} 24. a\_\mint{}\msupminus{}b (r(-1) * (b - t\^{}n - 1/r((n - 1)!))) * F[n;t] dt = Z 25. Z = (r(-1) * Y) 26. X = (((b - b\^{}n/r((n)!)) * F[n;b]) - (b - a\^{}n/r((n)!)) * F[n;a] - Z) 27. ((b - b\^{}n/r((n)!)) * F[n;b]) = r0 28. Taylor-remainder(I;n - 1;b;a;k,x.F[k;x]) = Y 29. v : \mBbbR{} 30. ((b - a\^{}n/r((n)!)) * F[n;a]) = v 31. v1 : \mBbbR{} 32. Taylor-approx(n;a;b;k,x.F[k;x]) = v1 33. v2 : \mBbbR{} 34. Taylor-approx(n - 1;a;b;k,x.F[k;x]) = v2 35. v3 : \mBbbR{} 36. F[0;b] = v3 \mvdash{} v = (v1 - v2) By Latex: ((Assert v1 = Taylor-approx(n;a;b;k,x.F[k;x]) BY Auto) THEN Unfold `Taylor-approx` -1 THEN (RWO "rsum-split-last" (-1) THENA Auto)) Home Index