---

Step * of Lemma second-deriv-nonpos-concave

∀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} . (h[x] ≤ r0))
        ⇒ concave-on(I;x.f[x]))))
BY
{ xxx(InstLemma `second-deriv-nonneg-convex` []
      THEN RepeatFor 2 ((ParallelLast' THENA Auto))
      THEN ((D 0 THENA Auto) THEN (D -2 With ⌜λ2x.-(f[x])⌝  THENA Auto))
      THEN ((D 0 THENA Auto) THEN (D -2 With ⌜λ2x.-(g[x])⌝  THENA Auto))
      THEN (D 0 THENA Auto)
      THEN (D -2 With ⌜λ2x.-(h[x])⌝  THENA Auto)
      THEN All (RepUR ``so_apply so_lambda``)
      THEN (ParallelLast THENA (Auto THEN BLemma `rminus_functionality` THEN Auto))
      THEN RepeatFor 2 ((ParallelLast THENA (ProveDerivative THEN Auto)))
      THEN (ParallelLast THENA 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. ∀x:{a:ℝ| a ∈ I} . ((h x) ≤ r0)
10. convex-on(I;x.-(f x))
⊢ concave-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\}  .  (h[x]  \mleq{}  r0))
                {}\mRightarrow{}  concave-on(I;x.f[x]))))


By

---

Latex:
xxx(InstLemma  `second-deriv-nonneg-convex`  []
        THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
        THEN  ((D  0  THENA  Auto)  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}\msubtwo{}x.-(f[x])\mkleeneclose{}    THENA  Auto))
        THEN  ((D  0  THENA  Auto)  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}\msubtwo{}x.-(g[x])\mkleeneclose{}    THENA  Auto))
        THEN  (D  0  THENA  Auto)
        THEN  (D  -2  With  \mkleeneopen{}\mlambda{}\msubtwo{}x.-(h[x])\mkleeneclose{}    THENA  Auto)
        THEN  All  (RepUR  ``so\_apply  so\_lambda``)
        THEN  (ParallelLast  THENA  (Auto  THEN  BLemma  `rminus\_functionality`  THEN  Auto))
        THEN  RepeatFor  2  ((ParallelLast  THENA  (ProveDerivative  THEN  Auto)))
        THEN  (ParallelLast  THENA  Auto))xxx

---

Home Index