miller/formalize/extra_realScript.sml

942 (* --------------------- exp is a convex function -------------------------- *)
957    ``!t. (t + (1 - t) * exp 0 - exp ((1 - t) * 0) = 0) /\
958          (t * exp 0 + (1 - t) - exp (t * 0) = 0)``,
963    ``!t x. ((\x. (1 - t) * exp x - exp ((1 - t) * x)) diffl
964             (\x. (1-t) * exp x - (1 - t)*exp ((1-t)*x)) x) x``,
966    >> `(\x. (1 - t) * exp x - exp ((1 - t) * x)) =
967        (\x. (\x. (1 - t) * exp x) x - (\x. exp ((1 - t) * x)) x)`
970    >> `((1 - t) * exp x - (1 - t) * exp ((1 - t) * x)) =
971        (\x. (1 - t) * exp x) x - (\x. (1-t) * exp ((1- t) * x)) x`
974    >> Suff `((\x. (1 - t) * exp x) diffl (\x. (1 - t) * exp x) x) x /\
975                 ((\x. exp ((1 - t) * x)) diffl (\x. (1 - t) * exp ((1 - t) * x)) x) x`
978    >- (`(\x. (1 - t) * exp x) x = 0 * exp x + (exp x) * (\x. 1 - t) x` by RW_TAC real_ss [REAL_MUL_COMM]
980        >> Q.ABBREV_TAC `foo = (0 * exp x + exp x * (\x. 1 - t) x)`
981        >> `(\x. (1 - t) * exp x) = (\x. (\x. 1 - t) x * exp x)` by RW_TAC std_ss [FUN_EQ_THM]
986    >> `(\x. exp ((1 - t) * x)) = (\x. exp ((\x. (1-t)*x) x))` by RW_TAC std_ss [FUN_EQ_THM]
988    >> `(\x. (1 - t) * exp ((1 - t) * x)) x = exp ((\x. (1-t)*x) x) * (1-t)`
1001    ``!t x. (\x. (1-t) * exp x - exp ((1-t)*x)) contl x``,
1006    ``!x. 0 < x /\ 0 < t /\ t < 1 ==> 0 < (\x. (1-t) * exp x - (1 - t)*exp ((1-t)*x)) x``,
1035                 exp (t * x + (1 - t) * y) <= t * exp x + (1 - t) * exp y``,
1039    >> Suff `exp (t * x + (1 - t) * (x+z)) <= t * exp x + (1 - t) * exp (x+z)`
1044    >> `t * exp x + (1 - t) * (exp x * exp z) = exp x * (t + (1 - t) * exp z)`
1048    >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `0 + exp ((1 - t) * z)` >> CONJ_TAC >- RW_TAC real_ss []
1051    >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `t + (1 - t) * exp 0 - exp ((1 - t) * 0)`
1053    >> `t + (1 - t) * exp 0 - exp ((1 - t) * 0) = ((1 - t) * exp 0 - exp ((1 - t) * 0)) + t`
1056    >> `t + (1 - t) * exp z - exp ((1 - t) * z) - t = (1 - t) * exp z - exp ((1 - t) * z)`
1059    >> Q.ABBREV_TAC `f = (\x. (1-t) * exp x - exp ((1-t)*x))`
1062    >> Q.EXISTS_TAC `(\x. (1-t) * exp x - (1 - t)*exp ((1-t)*x))`
1068    ``exp IN convex_fn``,
1111    >> Suff `(\v. t * v + (1 - t) * (@u. exp u = y) <= x') (@u. exp u = x)`
1115    >> Suff `(\v. t * x'' + (1 - t) * v <= x') (@u. exp u = y)`