Step
*
1
1
1
1
of Lemma
second-deriv-nonneg-convex
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. ∀a,b:{a:ℝ| a ∈ I} . ∀e:ℝ.
((r0 < e)
⇒ (∃c:ℝ
((rmin(a;b) ≤ c) ∧ (c ≤ rmax(a;b)) ∧ (|f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e))))
10. ∀x:{a:ℝ| a ∈ I} . (r0 ≤ h[x])
11. a : {a:ℝ| a ∈ I}
12. b : {a:ℝ| a ∈ I}
13. e : {e:ℝ| r0 < e}
14. c : ℝ
15. rmin(a;b) ≤ c
16. c ≤ rmax(a;b)
17. |f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e
⊢ (f[a] + (g[a] * (b - a))) ≤ (f[b] + e)
BY
{ ((Assert [rmin(a;b), rmax(a;b)] ⊆ I BY
EAuto 1)
THEN (Assert r0 ≤ (((b - c) * h[c]) * (b - a)) BY
(StableCases ⌜a < b⌝⋅ THEN Auto))
) }
1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. ∀a,b:{a:ℝ| a ∈ I} . ∀e:ℝ.
((r0 < e)
⇒ (∃c:ℝ
((rmin(a;b) ≤ c) ∧ (c ≤ rmax(a;b)) ∧ (|f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e))))
10. ∀x:{a:ℝ| a ∈ I} . (r0 ≤ h[x])
11. a : {a:ℝ| a ∈ I}
12. b : {a:ℝ| a ∈ I}
13. e : {e:ℝ| r0 < e}
14. c : ℝ
15. rmin(a;b) ≤ c
16. c ≤ rmax(a;b)
17. |f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e
18. [rmin(a;b), rmax(a;b)] ⊆ I
19. a < b
⊢ r0 ≤ (((b - c) * h[c]) * (b - a))
2
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. ∀a,b:{a:ℝ| a ∈ I} . ∀e:ℝ.
((r0 < e)
⇒ (∃c:ℝ
((rmin(a;b) ≤ c) ∧ (c ≤ rmax(a;b)) ∧ (|f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e))))
10. ∀x:{a:ℝ| a ∈ I} . (r0 ≤ h[x])
11. a : {a:ℝ| a ∈ I}
12. b : {a:ℝ| a ∈ I}
13. e : {e:ℝ| r0 < e}
14. c : ℝ
15. rmin(a;b) ≤ c
16. c ≤ rmax(a;b)
17. |f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e
18. [rmin(a;b), rmax(a;b)] ⊆ I
19. ¬(a < b)
⊢ r0 ≤ (((b - c) * h[c]) * (b - a))
3
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. ∀a,b:{a:ℝ| a ∈ I} . ∀e:ℝ.
((r0 < e)
⇒ (∃c:ℝ
((rmin(a;b) ≤ c) ∧ (c ≤ rmax(a;b)) ∧ (|f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e))))
10. ∀x:{a:ℝ| a ∈ I} . (r0 ≤ h[x])
11. a : {a:ℝ| a ∈ I}
12. b : {a:ℝ| a ∈ I}
13. e : {e:ℝ| r0 < e}
14. c : ℝ
15. rmin(a;b) ≤ c
16. c ≤ rmax(a;b)
17. |f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e
18. [rmin(a;b), rmax(a;b)] ⊆ I
19. r0 ≤ (((b - c) * h[c]) * (b - a))
⊢ (f[a] + (g[a] * (b - a))) ≤ (f[b] + e)
Latex:
Latex:
1. I : Interval
2. iproper(I)
3. f : I {}\mrightarrow{}\mBbbR{}
4. g : I {}\mrightarrow{}\mBbbR{}
5. h : I {}\mrightarrow{}\mBbbR{}
6. \mforall{}x,y:\{a:\mBbbR{}| a \mmember{} I\} . ((x = y) {}\mRightarrow{} (h[x] = h[y]))
7. d(f[x])/dx = \mlambda{}x.g[x] on I
8. d(g[x])/dx = \mlambda{}x.h[x] on I
9. \mforall{}a,b:\{a:\mBbbR{}| a \mmember{} I\} . \mforall{}e:\mBbbR{}.
((r0 < e)
{}\mRightarrow{} (\mexists{}c:\mBbbR{}
((rmin(a;b) \mleq{} c)
\mwedge{} (c \mleq{} rmax(a;b))
\mwedge{} (|f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| \mleq{} e))))
10. \mforall{}x:\{a:\mBbbR{}| a \mmember{} I\} . (r0 \mleq{} h[x])
11. a : \{a:\mBbbR{}| a \mmember{} I\}
12. b : \{a:\mBbbR{}| a \mmember{} I\}
13. e : \{e:\mBbbR{}| r0 < e\}
14. c : \mBbbR{}
15. rmin(a;b) \mleq{} c
16. c \mleq{} rmax(a;b)
17. |f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| \mleq{} e
\mvdash{} (f[a] + (g[a] * (b - a))) \mleq{} (f[b] + e)
By
Latex:
((Assert [rmin(a;b), rmax(a;b)] \msubseteq{} I BY
EAuto 1)
THEN (Assert r0 \mleq{} (((b - c) * h[c]) * (b - a)) BY
(StableCases \mkleeneopen{}a < b\mkleeneclose{}\mcdot{} THEN Auto))
)
Home
Index