Step
*
1
1
2
1
3
6
of Lemma
partition-refinement-sum
1. I : Interval@i
2. icompact(I)@i
3. f : I ⟶ℝ@i
4. mc : f[x] continuous for x ∈ I@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
⇒ (|partition-sum(f;y;full-partition(J;q))
- partition-sum(f;x;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)))))))))
8. J : Interval@i
9. icompact(J)@i
10. J ⊆ I @i
11. u : ℝ
12. v : ℝ List
13. partitions(J;[u / v])@i
14. ||[u / v]|| ≤ K@i
15. n : ℕ+@i
16. partition-mesh(J;[u / v]) ≤ (mc 1 n)@i
17. frs-increasing([u / v])@i
18. p : partition(J)@i
19. x : partition-choice(full-partition(J;p))@i
20. y : partition-choice(full-partition(J;[u / v]))@i
21. p refines [u / v]@i
22. partitions([left-endpoint(J), u];[])
∧ partitions([u, right-endpoint(J)];v)
∧ (left-endpoint(J) ≤ u)
∧ (u ≤ right-endpoint(J))
∧ (partition-mesh([left-endpoint(J), u];[]) ≤ partition-mesh(J;[u / v]))
∧ (partition-mesh([u, right-endpoint(J)];v) ≤ partition-mesh(J;[u / v]))
23. u ∈ J
24. (left-endpoint(J) ∈ J) ∧ (right-endpoint(J) ∈ J)
25. ∀p:partition([u, right-endpoint(J)]). ∀x:partition-choice(full-partition([u, right-endpoint(J)];p)).
∀y:partition-choice(full-partition([u, right-endpoint(J)];v)).
(p refines v
⇒ (|partition-sum(f;y;full-partition([u, right-endpoint(J)];v))
- partition-sum(f;x;full-partition([u, right-endpoint(J)];p))| ≤ ((r1/r(n)) * |[u, right-endpoint(J)]|)))
26. ∀p:partition([left-endpoint(J), u]). ∀x:partition-choice(full-partition([left-endpoint(J), u];p)).
∀y:partition-choice(full-partition([left-endpoint(J), u];[])).
(p refines []
⇒ (|partition-sum(f;y;full-partition([left-endpoint(J), u];[]))
- partition-sum(f;x;full-partition([left-endpoint(J), u];p))| ≤ ((r1/r(n)) * |[left-endpoint(J), u]|)))
⊢ |partition-sum(f;y;full-partition(J;[u / v])) - partition-sum(f;x;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)
BY
{ ((InstLemma `partition-refines-cons` [⌜J⌝;⌜u⌝;⌜v⌝;⌜p⌝]⋅
THENA (Auto
THEN OnMaybeHyp 17 (\h. (UnfoldTop `frs-increasing` h
THEN (InstHyp [⌜0⌝;⌜1⌝] h⋅ THENA Auto)
THEN Reduce (-1)
THEN RWO "select0" (-1)
THEN Complete (Auto)))
)
)
THEN ExRepD
THEN (With ⌜x⌝ (D (-1))⋅ THENA Auto)) }
1
1. I : Interval@i
2. icompact(I)@i
3. f : I ⟶ℝ@i
4. mc : f[x] continuous for x ∈ I@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
⇒ (|partition-sum(f;y;full-partition(J;q))
- partition-sum(f;x;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)))))))))
8. J : Interval@i
9. icompact(J)@i
10. J ⊆ I @i
11. u : ℝ
12. v : ℝ List
13. partitions(J;[u / v])@i
14. ||[u / v]|| ≤ K@i
15. n : ℕ+@i
16. partition-mesh(J;[u / v]) ≤ (mc 1 n)@i
17. frs-increasing([u / v])@i
18. p : partition(J)@i
19. x : partition-choice(full-partition(J;p))@i
20. y : partition-choice(full-partition(J;[u / v]))@i
21. p refines [u / v]@i
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. ∀p:partition([u, right-endpoint(J)]). ∀x:partition-choice(full-partition([u, right-endpoint(J)];p)).
∀y:partition-choice(full-partition([u, right-endpoint(J)];v)).
(p refines v
⇒ (|partition-sum(f;y;full-partition([u, right-endpoint(J)];v))
- partition-sum(f;x;full-partition([u, right-endpoint(J)];p))| ≤ ((r1/r(n)) * |[u, right-endpoint(J)]|)))
32. ∀p:partition([left-endpoint(J), u]). ∀x:partition-choice(full-partition([left-endpoint(J), u];p)).
∀y:partition-choice(full-partition([left-endpoint(J), u];[])).
(p refines []
⇒ (|partition-sum(f;y;full-partition([left-endpoint(J), u];[]))
- partition-sum(f;x;full-partition([left-endpoint(J), u];p))| ≤ ((r1/r(n)) * |[left-endpoint(J), u]|)))
33. q : partition([left-endpoint(J), u])
34. r : partition([u, right-endpoint(J)])
35. q refines []
36. r refines v
37. x1 : ℝ
38. x1 = u
39. p = (q @ [x1 / r]) ∈ (ℝ List)
40. ||r|| + ||q|| < ||p||
41. 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)))
⊢ |partition-sum(f;y;full-partition(J;[u / v])) - partition-sum(f;x;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)
Latex:
Latex:
1. I : Interval@i
2. icompact(I)@i
3. f : I {}\mrightarrow{}\mBbbR{}@i
4. mc : f[x] continuous for x \mmember{} I@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{} (|partition-sum(f;y;full-partition(J;q))
- partition-sum(f;x;full-partition(J;p))| \mleq{} ((r1/r(n)) * |J|)))))))))
8. J : Interval@i
9. icompact(J)@i
10. J \msubseteq{} I @i
11. u : \mBbbR{}
12. v : \mBbbR{} List
13. partitions(J;[u / v])@i
14. ||[u / v]|| \mleq{} K@i
15. n : \mBbbN{}\msupplus{}@i
16. partition-mesh(J;[u / v]) \mleq{} (mc 1 n)@i
17. frs-increasing([u / v])@i
18. p : partition(J)@i
19. x : partition-choice(full-partition(J;p))@i
20. y : partition-choice(full-partition(J;[u / v]))@i
21. p refines [u / v]@i
22. partitions([left-endpoint(J), u];[])
\mwedge{} partitions([u, right-endpoint(J)];v)
\mwedge{} (left-endpoint(J) \mleq{} u)
\mwedge{} (u \mleq{} right-endpoint(J))
\mwedge{} (partition-mesh([left-endpoint(J), u];[]) \mleq{} partition-mesh(J;[u / v]))
\mwedge{} (partition-mesh([u, right-endpoint(J)];v) \mleq{} partition-mesh(J;[u / v]))
23. u \mmember{} J
24. (left-endpoint(J) \mmember{} J) \mwedge{} (right-endpoint(J) \mmember{} J)
25. \mforall{}p:partition([u, right-endpoint(J)]).
\mforall{}x:partition-choice(full-partition([u, right-endpoint(J)];p)).
\mforall{}y:partition-choice(full-partition([u, right-endpoint(J)];v)).
(p refines v
{}\mRightarrow{} (|partition-sum(f;y;full-partition([u, right-endpoint(J)];v))
- partition-sum(f;x;full-partition([u, right-endpoint(J)];p))| \mleq{} ((r1/r(n))
* |[u, right-endpoint(J)]|)))
26. \mforall{}p:partition([left-endpoint(J), u]).
\mforall{}x:partition-choice(full-partition([left-endpoint(J), u];p)).
\mforall{}y:partition-choice(full-partition([left-endpoint(J), u];[])).
(p refines []
{}\mRightarrow{} (|partition-sum(f;y;full-partition([left-endpoint(J), u];[]))
- partition-sum(f;x;full-partition([left-endpoint(J), u];p))| \mleq{} ((r1/r(n))
* |[left-endpoint(J), u]|)))
\mvdash{} |partition-sum(f;y;full-partition(J;[u / v]))
- partition-sum(f;x;full-partition(J;p))| \mleq{} ((r1/r(n)) * |J|)
By
Latex:
((InstLemma `partition-refines-cons` [\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
THENA (Auto
THEN OnMaybeHyp 17 (\mbackslash{}h. (UnfoldTop `frs-increasing` h
THEN (InstHyp [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}] h\mcdot{} THENA Auto)
THEN Reduce (-1)
THEN RWO "select0" (-1)
THEN Complete (Auto)))
)
)
THEN ExRepD
THEN (With \mkleeneopen{}x\mkleeneclose{} (D (-1))\mcdot{} THENA Auto))
Home
Index