---

Step * 1 1 1 of Lemma implies-convex-on


1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y]))
4. ∀x,y:ℝ.
     ((x < y)
     ⇒ (∀t:ℝ
           ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))))
5. x : ℝ
6. y : ℝ
7. t : ℝ
8. x ∈ I
9. y ∈ I
10. t ∈ [r0, r1]
11. (t * x) + ((r1 - t) * y) ∈ I
12. ¬(x < y)
13. y < x
14. f[((r1 - t) * y) + ((r1 - r1 - t) * x)] ≤ (((r1 - t) * f[y]) + ((r1 - r1 - t) * f[x]))
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))
BY
{ ((Assert r0 ≤ (r1 - t) BY
          (nRAdd ⌜t⌝ 0⋅ THEN Auto))
   THEN (Assert ((r1 - t) * y) + ((r1 - r1 - t) * x) ∈ I BY
               (BLemma `i-member-convex` THEN Auto))
   THEN (Assert f[(t * x) + ((r1 - t) * y)] = f[((r1 - t) * y) + ((r1 - r1 - t) * x)] BY
               (BackThruSomeHyp THEN Auto))
   THEN (Assert (((r1 - t) * f[y]) + ((r1 - r1 - t) * f[x])) = ((t * f[x]) + ((r1 - t) * f[y])) BY
               Auto)) }

1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y]))
4. ∀x,y:ℝ.
     ((x < y)
     ⇒ (∀t:ℝ
           ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))))
5. x : ℝ
6. y : ℝ
7. t : ℝ
8. x ∈ I
9. y ∈ I
10. t ∈ [r0, r1]
11. (t * x) + ((r1 - t) * y) ∈ I
12. ¬(x < y)
13. y < x
14. f[((r1 - t) * y) + ((r1 - r1 - t) * x)] ≤ (((r1 - t) * f[y]) + ((r1 - r1 - t) * f[x]))
15. r0 ≤ (r1 - t)
16. ((r1 - t) * y) + ((r1 - r1 - t) * x) ∈ I
17. f[(t * x) + ((r1 - t) * y)] = f[((r1 - t) * y) + ((r1 - r1 - t) * x)]
18. (((r1 - t) * f[y]) + ((r1 - r1 - t) * f[x])) = ((t * f[x]) + ((r1 - t) * f[y]))
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  \mforall{}x,y:\mBbbR{}.    ((x  \mmember{}  I)  {}\mRightarrow{}  (y  \mmember{}  I)  {}\mRightarrow{}  (x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
4.  \mforall{}x,y:\mBbbR{}.
          ((x  <  y)
          {}\mRightarrow{}  (\mforall{}t:\mBbbR{}
                      ((x  \mmember{}  I)
                      {}\mRightarrow{}  (y  \mmember{}  I)
                      {}\mRightarrow{}  (t  \mmember{}  [r0,  r1])
                      {}\mRightarrow{}  (f[(t  *  x)  +  ((r1  -  t)  *  y)]  \mleq{}  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))))))
5.  x  :  \mBbbR{}
6.  y  :  \mBbbR{}
7.  t  :  \mBbbR{}
8.  x  \mmember{}  I
9.  y  \mmember{}  I
10.  t  \mmember{}  [r0,  r1]
11.  (t  *  x)  +  ((r1  -  t)  *  y)  \mmember{}  I
12.  \mneg{}(x  <  y)
13.  y  <  x
14.  f[((r1  -  t)  *  y)  +  ((r1  -  r1  -  t)  *  x)]  \mleq{}  (((r1  -  t)  *  f[y])  +  ((r1  -  r1  -  t)  *  f[x]))
\mvdash{}  f[(t  *  x)  +  ((r1  -  t)  *  y)]  \mleq{}  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))


By

---

Latex:
((Assert  r0  \mleq{}  (r1  -  t)  BY
                (nRAdd  \mkleeneopen{}t\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (Assert  ((r1  -  t)  *  y)  +  ((r1  -  r1  -  t)  *  x)  \mmember{}  I  BY
                          (BLemma  `i-member-convex`  THEN  Auto))
  THEN  (Assert  f[(t  *  x)  +  ((r1  -  t)  *  y)]  =  f[((r1  -  t)  *  y)  +  ((r1  -  r1  -  t)  *  x)]  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  (Assert  (((r1  -  t)  *  f[y])  +  ((r1  -  r1  -  t)  *  f[x]))  =  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))  BY
                          Auto))

---

Home Index