Step
*
1
1
1
1
1
1
1
1
1
1
1
2
1
1
2
1
1
of Lemma
partition-refinement-sum
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. partitions(J;[])
12. ||[]|| ≤ K
13. n : ℕ+
14. partition-mesh(J;[]) ≤ (mc 1 n)
15. p : partition(J)
16. x : partition-choice(full-partition(J;p))
17. y : partition-choice(full-partition(J;[]))
18. p refines []
19. (y 0) = (y 0) ∈ ℝ
20. y 0 ∈ J
21. f ∈ J ⟶ℝ
22. S(f;full-partition(J;[])) ∈ ℝ
23. f (y 0) ∈ ℝ
24. S(f;full-partition(J;[])) = ((f (y 0)) * |J|)
25. mc 1 n ∈ ℝ
26. Σ{(f (y 0)) * (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) | 0≤i≤||full-partition(J;p)|| - 2}
= ((f (y 0)) * |J|)
27. ∀i:ℕ(||full-partition(J;p)|| - 2) + 1. (f (x i) ∈ ℝ)
28. Σ{|((f (y 0)) * (full-partition(J;p)[i + 1] - full-partition(J;p)[i])) - (f (x i))
* (full-partition(J;p)[i + 1] - full-partition(J;p)[i])| | 0≤i≤||full-partition(J;p)|| - 2}
= Σ{|(f (y 0)) - f (x i)| * (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) | 0≤i≤||full-partition(J;p)|| - 2}
29. i : ℤ
30. 0 ≤ i
31. i ≤ (||full-partition(J;p)|| - 2)
32. z : {x:ℝ| r0 ≤ x}
33. (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) = z ∈ {x:ℝ| r0 ≤ x}
34. mc 1 n ∈ {d:ℝ| (r0 < d) ∧ (∀x,y:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n)))))}
⊢ |(f (y 0)) - f (x i)| ≤ (r1/r(n))
BY
{ (Thin 21 THEN (MemTypeHD (-1) THENA Auto) THEN Unhide THEN Auto) }
1
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. partitions(J;[])
12. ||[]|| ≤ K
13. n : ℕ+
14. partition-mesh(J;[]) ≤ (mc 1 n)
15. p : partition(J)
16. x : partition-choice(full-partition(J;p))
17. y : partition-choice(full-partition(J;[]))
18. p refines []
19. (y 0) = (y 0) ∈ ℝ
20. y 0 ∈ J
21. S(f;full-partition(J;[])) ∈ ℝ
22. f (y 0) ∈ ℝ
23. S(f;full-partition(J;[])) = ((f (y 0)) * |J|)
24. mc 1 n ∈ ℝ
25. Σ{(f (y 0)) * (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) | 0≤i≤||full-partition(J;p)|| - 2}
= ((f (y 0)) * |J|)
26. ∀i:ℕ(||full-partition(J;p)|| - 2) + 1. (f (x i) ∈ ℝ)
27. Σ{|((f (y 0)) * (full-partition(J;p)[i + 1] - full-partition(J;p)[i])) - (f (x i))
* (full-partition(J;p)[i + 1] - full-partition(J;p)[i])| | 0≤i≤||full-partition(J;p)|| - 2}
= Σ{|(f (y 0)) - f (x i)| * (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) | 0≤i≤||full-partition(J;p)|| - 2}
28. i : ℤ
29. 0 ≤ i
30. i ≤ (||full-partition(J;p)|| - 2)
31. z : {x:ℝ| r0 ≤ x}
32. (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) = z ∈ {x:ℝ| r0 ≤ x}
33. (mc 1 n) = (mc 1 n) ∈ ℝ
34. r0 < (mc 1 n)
35. ∀x,y:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ (mc 1 n)) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))
⊢ |(f (y 0)) - f (x i)| ≤ (r1/r(n))
Latex:
Latex:
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. partitions(J;[])
12. ||[]|| \mleq{} K
13. n : \mBbbN{}\msupplus{}
14. partition-mesh(J;[]) \mleq{} (mc 1 n)
15. p : partition(J)
16. x : partition-choice(full-partition(J;p))
17. y : partition-choice(full-partition(J;[]))
18. p refines []
19. (y 0) = (y 0)
20. y 0 \mmember{} J
21. f \mmember{} J {}\mrightarrow{}\mBbbR{}
22. S(f;full-partition(J;[])) \mmember{} \mBbbR{}
23. f (y 0) \mmember{} \mBbbR{}
24. S(f;full-partition(J;[])) = ((f (y 0)) * |J|)
25. mc 1 n \mmember{} \mBbbR{}
26. \mSigma{}\{(f (y 0))
* (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) | 0\mleq{}i\mleq{}||full-partition(J;p)|| - 2\}
= ((f (y 0)) * |J|)
27. \mforall{}i:\mBbbN{}(||full-partition(J;p)|| - 2) + 1. (f (x i) \mmember{} \mBbbR{})
28. \mSigma{}\{|((f (y 0)) * (full-partition(J;p)[i + 1] - full-partition(J;p)[i])) - (f (x i))
* (full-partition(J;p)[i + 1] - full-partition(J;p)[i])| | 0\mleq{}i\mleq{}||full-partition(J;p)|| - 2\}
= \mSigma{}\{|(f (y 0)) - f (x i)|
* (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) | 0\mleq{}i\mleq{}||full-partition(J;p)|| - 2\}
29. i : \mBbbZ{}
30. 0 \mleq{} i
31. i \mleq{} (||full-partition(J;p)|| - 2)
32. z : \{x:\mBbbR{}| r0 \mleq{} x\}
33. (full-partition(J;p)[i + 1] - full-partition(J;p)[i]) = z
34. mc 1 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)))))\}
\mvdash{} |(f (y 0)) - f (x i)| \mleq{} (r1/r(n))
By
Latex:
(Thin 21 THEN (MemTypeHD (-1) THENA Auto) THEN Unhide THEN Auto)
Home
Index