---

Step * of Lemma second-deriv-nonneg-convex

∀I:Interval
  (iproper(I)
  ⇒ (∀f,g,h:I ⟶ℝ.
        ((∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y])))
        ⇒ d(f[x])/dx = λx.g[x] on I
        ⇒ d(g[x])/dx = λx.h[x] on I
        ⇒ (∀x:{a:ℝ| a ∈ I} . (r0 ≤ h[x]))
        ⇒ convex-on(I;x.f[x]))))
BY
{ xxx(InstLemma `Taylor-theorem-for-2` [] THEN RepeatFor 8 ((ParallelLast' THENA Auto)) THEN Auto)xxx }

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])
⊢ convex-on(I;x.f[x])

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,g,h:I  {}\mrightarrow{}\mBbbR{}.
                ((\mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (h[x]  =  h[y])))
                {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
                {}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.h[x]  on  I
                {}\mRightarrow{}  (\mforall{}x:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  (r0  \mleq{}  h[x]))
                {}\mRightarrow{}  convex-on(I;x.f[x]))))


By

---

Latex:
xxx(InstLemma  `Taylor-theorem-for-2`  []  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))  THEN  Auto)xxx

---

Home Index