Step
*
1
1
2
1
3
4
1
1
1
1
1
1
1
2
1
1
2
2
1
1
2
1
4
2
2
1
1
1
2
1
1
of Lemma
partition-refinement-sum
.....assertion.....
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. ∀m,n:ℕ+.
(mc m n ∈ {d:ℝ| (r0 < d) ∧ (∀x,y:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n)))))} )
6. K : ℕ
7. ∀K:ℕK. ∀J:Interval.
(icompact(J)
⇒ J ⊆ I
⇒ (∀q:partition(J)
((||q|| ≤ K)
⇒ (∀n:ℕ+
((partition-mesh(J;q) ≤ (mc 1 n))
⇒ frs-increasing(q)
⇒ (∀p:partition(J). ∀x:partition-choice(full-partition(J;p)).
∀y:partition-choice(full-partition(J;q)).
(p refines q
⇒ (|S(f;full-partition(J;q)) - S(f;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)))))))))
8. J : Interval
9. icompact(J)
10. J ⊆ I
11. u : ℝ
12. v : ℝ List
13. partitions(J;[u / v])
14. ||[u / v]|| ≤ K
15. n : ℕ+
16. partition-mesh(J;[u / v]) ≤ (mc 1 n)
17. frs-increasing([u / v])
18. p : partition(J)
19. x : partition-choice(full-partition(J;p))
20. y : partition-choice(full-partition(J;[u / v]))
21. p refines [u / v]
22. partitions([left-endpoint(J), u];[])
23. partitions([u, right-endpoint(J)];v)
24. left-endpoint(J) ≤ u
25. u ≤ right-endpoint(J)
26. partition-mesh([left-endpoint(J), u];[]) ≤ partition-mesh(J;[u / v])
27. partition-mesh([u, right-endpoint(J)];v) ≤ partition-mesh(J;[u / v])
28. u ∈ J
29. left-endpoint(J) ∈ J
30. right-endpoint(J) ∈ J
31. q : partition([left-endpoint(J), u])
32. r : partition([u, right-endpoint(J)])
33. q refines []
34. r refines v
35. x1 : ℝ
36. x1 = u
37. p = (q @ [x1 / r]) ∈ (ℝ List)
38. ||r|| + ||q|| < ||p||
39. is-partition-choice(full-partition([left-endpoint(J), u];q);x)
∧ is-partition-choice(full-partition([u, right-endpoint(J)];r);λi.(x (i + ||q|| + 1)))
40. icompact([left-endpoint(J), u]) ∧ icompact([u, right-endpoint(J)])
41. (||r|| + ||q|| + 1) + 1 < ||full-partition(J;p)||
42. λi.(x (i + ||q|| + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];r))
43. x ∈ partition-choice(full-partition([left-endpoint(J), u];q))
44. ||v|| + 2 < ||full-partition(J;[u / v])||
45. λi.(y 0) ∈ partition-choice(full-partition([left-endpoint(J), u];[]))
46. |S(f;full-partition([left-endpoint(J), u];[])) - S(f;full-partition([left-endpoint(J), u];q))| ≤ ((r1/r(n))
* |[left-endpoint(J), u]|)
47. λi.(y (i + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];v))
48. |S(f;full-partition([u, right-endpoint(J)];v)) - S(f;full-partition([u, right-endpoint(J)];r))| ≤ ((r1/r(n))
* |[u, right-endpoint(J)]|)
49. [left-endpoint(J), u] ⊆ I ∧ [u, right-endpoint(J)] ⊆ I
50. a : ℝ
51. left-endpoint(J) = a ∈ ℝ
52. b : ℝ
53. right-endpoint(J) = b ∈ ℝ
54. ∀i:ℕ. ((i ≤ (||q|| + ||r|| + 1)) ⇒ (f (x i) ∈ ℝ))
55. v1 : ℝ
56. Σ{(f (x i)) * ([a / ((q @ [x1 / r]) @ [b])][i + 1] - [a / ((q @ [x1 / r]) @ [b])][i]) | 0≤i≤||q|| + ||r|| + 1}
= v1
∈ ℝ
57. v2 : ℝ
58. Σ{(f (x i)) * ([a / ((q @ [x1 / r]) @ [b])][i + 1] - [a / ((q @ [x1 / r]) @ [b])][i]) | 0≤i≤||q||} = v2 ∈ ℝ
59. v3 : ℝ
60. Σ{(f (x i)) * ([a / ((q @ [x1 / r]) @ [b])][i + 1] - [a / ((q @ [x1 / r]) @ [b])][i]) | ||q|| + 1≤i≤||q||
+ ||r||
+ 1}
= v3
∈ ℝ
61. Σ{(f (x i)) * ([a / (q @ [u])][i + 1] - [a / (q @ [u])][i]) | 0≤i≤(||q @ [u]|| + 1) - 2} ∈ ℝ
62. v4 : ℝ
63. Σ{(f (x i)) * ([a / (q @ [u])][i + 1] - [a / (q @ [u])][i]) | 0≤i≤(||q @ [u]|| + 1) - 2} = v4 ∈ ℝ
⊢ Σ{(f (x (i + ||q|| + 1))) * ([u / (r @ [b])][i + 1] - [u / (r @ [b])][i]) | 0≤i≤(||r @ [b]|| + 1) - 2} ∈ ℝ
BY
{ (DVar `q'
THEN DVar `r'
THEN RepeatFor 2 (MemCD')
THEN Try (BackThruSomeHyp)
THEN Try ((All Thin THEN Complete (Auto')))) }
Latex:
Latex:
.....assertion.....
1. I : Interval
2. icompact(I)
3. f : I {}\mrightarrow{}\mBbbR{}
4. mc : f[x] continuous for x \mmember{} I
5. \mforall{}m,n:\mBbbN{}\msupplus{}.
(mc m n \mmember{} \{d:\mBbbR{}|
(r0 < d)
\mwedge{} (\mforall{}x,y:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (y \mmember{} I) {}\mRightarrow{} (|x - y| \mleq{} d) {}\mRightarrow{} (|f[x] - f[y]| \mleq{} (r1/r(n)))))\} )
6. K : \mBbbN{}
7. \mforall{}K:\mBbbN{}K. \mforall{}J:Interval.
(icompact(J)
{}\mRightarrow{} J \msubseteq{} I
{}\mRightarrow{} (\mforall{}q:partition(J)
((||q|| \mleq{} K)
{}\mRightarrow{} (\mforall{}n:\mBbbN{}\msupplus{}
((partition-mesh(J;q) \mleq{} (mc 1 n))
{}\mRightarrow{} frs-increasing(q)
{}\mRightarrow{} (\mforall{}p:partition(J). \mforall{}x:partition-choice(full-partition(J;p)).
\mforall{}y:partition-choice(full-partition(J;q)).
(p refines q
{}\mRightarrow{} (|S(f;full-partition(J;q)) - S(f;full-partition(J;p))| \mleq{} ((r1/r(n))
* |J|)))))))))
8. J : Interval
9. icompact(J)
10. J \msubseteq{} I
11. u : \mBbbR{}
12. v : \mBbbR{} List
13. partitions(J;[u / v])
14. ||[u / v]|| \mleq{} K
15. n : \mBbbN{}\msupplus{}
16. partition-mesh(J;[u / v]) \mleq{} (mc 1 n)
17. frs-increasing([u / v])
18. p : partition(J)
19. x : partition-choice(full-partition(J;p))
20. y : partition-choice(full-partition(J;[u / v]))
21. p refines [u / v]
22. partitions([left-endpoint(J), u];[])
23. partitions([u, right-endpoint(J)];v)
24. left-endpoint(J) \mleq{} u
25. u \mleq{} right-endpoint(J)
26. partition-mesh([left-endpoint(J), u];[]) \mleq{} partition-mesh(J;[u / v])
27. partition-mesh([u, right-endpoint(J)];v) \mleq{} partition-mesh(J;[u / v])
28. u \mmember{} J
29. left-endpoint(J) \mmember{} J
30. right-endpoint(J) \mmember{} J
31. q : partition([left-endpoint(J), u])
32. r : partition([u, right-endpoint(J)])
33. q refines []
34. r refines v
35. x1 : \mBbbR{}
36. x1 = u
37. p = (q @ [x1 / r])
38. ||r|| + ||q|| < ||p||
39. is-partition-choice(full-partition([left-endpoint(J), u];q);x)
\mwedge{} is-partition-choice(full-partition([u, right-endpoint(J)];r);\mlambda{}i.(x (i + ||q|| + 1)))
40. icompact([left-endpoint(J), u]) \mwedge{} icompact([u, right-endpoint(J)])
41. (||r|| + ||q|| + 1) + 1 < ||full-partition(J;p)||
42. \mlambda{}i.(x (i + ||q|| + 1)) \mmember{} partition-choice(full-partition([u, right-endpoint(J)];r))
43. x \mmember{} partition-choice(full-partition([left-endpoint(J), u];q))
44. ||v|| + 2 < ||full-partition(J;[u / v])||
45. \mlambda{}i.(y 0) \mmember{} partition-choice(full-partition([left-endpoint(J), u];[]))
46. |S(f;full-partition([left-endpoint(J), u];[]))
- S(f;full-partition([left-endpoint(J), u];q))| \mleq{} ((r1/r(n)) * |[left-endpoint(J), u]|)
47. \mlambda{}i.(y (i + 1)) \mmember{} partition-choice(full-partition([u, right-endpoint(J)];v))
48. |S(f;full-partition([u, right-endpoint(J)];v))
- S(f;full-partition([u, right-endpoint(J)];r))| \mleq{} ((r1/r(n)) * |[u, right-endpoint(J)]|)
49. [left-endpoint(J), u] \msubseteq{} I \mwedge{} [u, right-endpoint(J)] \msubseteq{} I
50. a : \mBbbR{}
51. left-endpoint(J) = a
52. b : \mBbbR{}
53. right-endpoint(J) = b
54. \mforall{}i:\mBbbN{}. ((i \mleq{} (||q|| + ||r|| + 1)) {}\mRightarrow{} (f (x i) \mmember{} \mBbbR{}))
55. v1 : \mBbbR{}
56. \mSigma{}\{(f (x i))
* ([a / ((q @ [x1 / r]) @ [b])][i + 1] - [a / ((q @ [x1 / r]) @ [b])][i]) | 0\mleq{}i\mleq{}||q|| + ||r|| + 1\}
= v1
57. v2 : \mBbbR{}
58. \mSigma{}\{(f (x i))
* ([a / ((q @ [x1 / r]) @ [b])][i + 1] - [a / ((q @ [x1 / r]) @ [b])][i]) | 0\mleq{}i\mleq{}||q||\}
= v2
59. v3 : \mBbbR{}
60. \mSigma{}\{(f (x i)) * ([a / ((q @ [x1 / r]) @ [b])][i + 1] - [a / ((q @ [x1 / r]) @ [b])][i]) | ||q||
+ 1\mleq{}i\mleq{}||q|| + ||r|| + 1\}
= v3
61. \mSigma{}\{(f (x i)) * ([a / (q @ [u])][i + 1] - [a / (q @ [u])][i]) | 0\mleq{}i\mleq{}(||q @ [u]|| + 1) - 2\} \mmember{} \mBbbR{}
62. v4 : \mBbbR{}
63. \mSigma{}\{(f (x i)) * ([a / (q @ [u])][i + 1] - [a / (q @ [u])][i]) | 0\mleq{}i\mleq{}(||q @ [u]|| + 1) - 2\} = v4
\mvdash{} \mSigma{}\{(f (x (i + ||q|| + 1))) * ([u / (r @ [b])][i + 1] - [u / (r @ [b])][i]) | 0\mleq{}i\mleq{}(||r @ [b]|| + 1)
- 2\} \mmember{} \mBbbR{}
By
Latex:
(DVar `q'
THEN DVar `r'
THEN RepeatFor 2 (MemCD')
THEN Try (BackThruSomeHyp)
THEN Try ((All Thin THEN Complete (Auto'))))
Home
Index