Step * 1 of Lemma second-deriv-nonneg-convex


1. Interval
2. iproper(I)
3. I ⟶ℝ
4. I ⟶ℝ
5. 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])
⊢ convex-on(I;x.f[x])
BY
Assert ⌜∀a,b:{a:ℝa ∈ I} .  ((f[a] (g[a] (b a))) ≤ f[b])⌝⋅ }

1
.....assertion..... 
1. Interval
2. iproper(I)
3. I ⟶ℝ
4. I ⟶ℝ
5. 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])
⊢ ∀a,b:{a:ℝa ∈ I} .  ((f[a] (g[a] (b a))) ≤ f[b])

2
1. Interval
2. iproper(I)
3. I ⟶ℝ
4. I ⟶ℝ
5. 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,b:{a:ℝa ∈ I} .  ((f[a] (g[a] (b a))) ≤ f[b])
⊢ convex-on(I;x.f[x])


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])
\mvdash{}  convex-on(I;x.f[x])


By


Latex:
Assert  \mkleeneopen{}\mforall{}a,b:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((f[a]  +  (g[a]  *  (b  -  a)))  \mleq{}  f[b])\mkleeneclose{}\mcdot{}




Home Index