Step
*
1
1
1
2
1
1
of Lemma
derivative_unique
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. x : ℝ
7. x ∈ I
8. m : ℕ+
9. n : ℕ+
10. iproper(i-approx(I;n))
11. x ∈ i-approx(I;n)
12. icompact(i-approx(I;n))
13. del : ℝ
14. r0 < del
15. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
16. d1 : ℝ
17. r0 < d1
18. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d1)
⇒ (|f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
19. y : ℝ
20. y ∈ I
21. y ∈ i-approx(I;n)
22. |y - x| ≤ del
23. |y - x| ≤ d1
24. r0 < |y - x|
25. |f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)
26. |(g2[x] * (y - x)) - f[y] - f[x]| ≤ ((r1/r(2 * m)) * |y - x|)
⊢ |g1(x) - g2(x)| ≤ (r1/r(m))
BY
{ ((Assert (|f[y] - f[x] - g1[x] * (y - x)| + |(g2[x] * (y - x)) - f[y] - f[x]|) ≤ (((r1/r(2 * m)) * |y - x|)
+ ((r1/r(2 * m)) * |y - x|)) BY
(RWO "-1 -2" 0 THEN Auto))
THEN (RWO "r-triangle-inequality<" (-1) THENA Auto)
THEN (Assert |(f[y] - f[x] - g1[x] * (y - x)) + ((g2[x] * (y - x)) - f[y] - f[x])| = (|g2(x) - g1(x)| * |y - x|) BY
((RWO "rabs-rmul<" 0 THENA Auto)
THEN GenConclTerms Auto [⌜f[y] - f[x]⌝;⌜y - x⌝]⋅
THEN RepUR ``r-ap so_apply`` 0
THEN nRNorm 0
THEN Auto))
THEN (RWO "-1" (-2) THENA Auto)) }
1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. x : ℝ
7. x ∈ I
8. m : ℕ+
9. n : ℕ+
10. iproper(i-approx(I;n))
11. x ∈ i-approx(I;n)
12. icompact(i-approx(I;n))
13. del : ℝ
14. r0 < del
15. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
16. d1 : ℝ
17. r0 < d1
18. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d1)
⇒ (|f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
19. y : ℝ
20. y ∈ I
21. y ∈ i-approx(I;n)
22. |y - x| ≤ del
23. |y - x| ≤ d1
24. r0 < |y - x|
25. |f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)
26. |(g2[x] * (y - x)) - f[y] - f[x]| ≤ ((r1/r(2 * m)) * |y - x|)
27. (|g2(x) - g1(x)| * |y - x|) ≤ (((r1/r(2 * m)) * |y - x|) + ((r1/r(2 * m)) * |y - x|))
28. |(f[y] - f[x] - g1[x] * (y - x)) + ((g2[x] * (y - x)) - f[y] - f[x])| = (|g2(x) - g1(x)| * |y - x|)
⊢ |g1(x) - g2(x)| ≤ (r1/r(m))
Latex:
Latex:
1. I : Interval
2. iproper(I)
3. f : I {}\mrightarrow{}\mBbbR{}
4. g1 : I {}\mrightarrow{}\mBbbR{}
5. g2 : I {}\mrightarrow{}\mBbbR{}
6. x : \mBbbR{}
7. x \mmember{} I
8. m : \mBbbN{}\msupplus{}
9. n : \mBbbN{}\msupplus{}
10. iproper(i-approx(I;n))
11. x \mmember{} i-approx(I;n)
12. icompact(i-approx(I;n))
13. del : \mBbbR{}
14. r0 < del
15. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} del)
{}\mRightarrow{} (|f[y] - f[x] - g2[x] * (y - x)| \mleq{} ((r1/r(2 * m)) * |y - x|)))
16. d1 : \mBbbR{}
17. r0 < d1
18. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} d1)
{}\mRightarrow{} (|f[y] - f[x] - g1[x] * (y - x)| \mleq{} ((r1/r(2 * m)) * |y - x|)))
19. y : \mBbbR{}
20. y \mmember{} I
21. y \mmember{} i-approx(I;n)
22. |y - x| \mleq{} del
23. |y - x| \mleq{} d1
24. r0 < |y - x|
25. |f[y] - f[x] - g1[x] * (y - x)| \mleq{} ((r1/r(2 * m)) * |y - x|)
26. |(g2[x] * (y - x)) - f[y] - f[x]| \mleq{} ((r1/r(2 * m)) * |y - x|)
\mvdash{} |g1(x) - g2(x)| \mleq{} (r1/r(m))
By
Latex:
((Assert (|f[y] - f[x] - g1[x] * (y - x)| + |(g2[x] * (y - x)) - f[y] - f[x]|) \mleq{} (((r1/r(2 * m))
* |y - x|)
+ ((r1/r(2 * m)) * |y - x|)) BY
(RWO "-1 -2" 0 THEN Auto))
THEN (RWO "r-triangle-inequality<" (-1) THENA Auto)
THEN (Assert |(f[y] - f[x] - g1[x] * (y - x)) + ((g2[x] * (y - x)) - f[y] - f[x])|
= (|g2(x) - g1(x)| * |y - x|) BY
((RWO "rabs-rmul<" 0 THENA Auto)
THEN GenConclTerms Auto [\mkleeneopen{}f[y] - f[x]\mkleeneclose{};\mkleeneopen{}y - x\mkleeneclose{}]\mcdot{}
THEN RepUR ``r-ap so\_apply`` 0
THEN nRNorm 0
THEN Auto))
THEN (RWO "-1" (-2) THENA Auto))
Home
Index