---

Step * 1 2 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. x : ℝ
12. y : ℝ
13. t : ℝ
14. x ∈ I
15. y ∈ I
16. t ∈ [r0, r1]
17. (t * x) + ((r1 - t) * y) ∈ I
18. ∀b:{a:ℝ| a ∈ I} 
      ((f[(t * x) + ((r1 - t) * y)] + (g[(t * x) + ((r1 - t) * y)] * (b - (t * x) + ((r1 - t) * y)))) ≤ f[b])
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))
BY
{ ((InstHyp [⌜x⌝] (-1)⋅ THENA Auto)
   THEN (Assert (x - (t * x) + ((r1 - t) * y)) = ((r1 - t) * (x - y)) BY
               Auto)
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-1)) }

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. x : ℝ
12. y : ℝ
13. t : ℝ
14. x ∈ I
15. y ∈ I
16. t ∈ [r0, r1]
17. (t * x) + ((r1 - t) * y) ∈ I
18. ∀b:{a:ℝ| a ∈ I} 
      ((f[(t * x) + ((r1 - t) * y)] + (g[(t * x) + ((r1 - t) * y)] * (b - (t * x) + ((r1 - t) * y)))) ≤ f[b])
19. (f[(t * x) + ((r1 - t) * y)] + (g[(t * x) + ((r1 - t) * y)] * (r1 - t) * (x - y))) ≤ f[x]
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))

---

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.  x  :  \mBbbR{}
12.  y  :  \mBbbR{}
13.  t  :  \mBbbR{}
14.  x  \mmember{}  I
15.  y  \mmember{}  I
16.  t  \mmember{}  [r0,  r1]
17.  (t  *  x)  +  ((r1  -  t)  *  y)  \mmember{}  I
18.  \mforall{}b:\{a:\mBbbR{}|  a  \mmember{}  I\} 
            ((f[(t  *  x)  +  ((r1  -  t)  *  y)]
            +  (g[(t  *  x)  +  ((r1  -  t)  *  y)]  *  (b  -  (t  *  x)  +  ((r1  -  t)  *  y))))  \mleq{}  f[b])
\mvdash{}  f[(t  *  x)  +  ((r1  -  t)  *  y)]  \mleq{}  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (Assert  (x  -  (t  *  x)  +  ((r1  -  t)  *  y))  =  ((r1  -  t)  *  (x  -  y))  BY
                          Auto)
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index