#use "Multivariate/realanalysis.ml";;
#use "Multivariate/derivatives.ml";;
g `!p e. p <= &1 ==> &0 < e ==> ?d. &0 < d /\ !x y. &1 <= x /\ &1 <= y /\ y <= x /\ abs(x - y) < d ==> abs(x rpow p - y rpow p) < e` ;;
e( REPEAT STRIP_TAC );;
e( ASM_CASES_TAC `p = &0` );;
e( ASM_SIMP_TAC [RPOW_POW;real_pow] );;
e( EXISTS_TAC `&1`);;
e( REPEAT STRIP_TAC );;
e( REAL_ARITH_TAC );;
e( ASM_REAL_ARITH_TAC );;
e( EXISTS_TAC `e/(abs(p))`);;
e( REPEAT STRIP_TAC );;
e( ASM_MESON_TAC [REAL_ABS_NZ;REAL_LT_DIV] );;
e( DISJ_CASES_TAC (UNDISCH_ALL(REAL_ARITH`y:real <=x==>x=y\/y<x`)) );;
e( ASM_SIMP_TAC [] THEN ASM_REAL_ARITH_TAC );;
e( MP_TAC (SPECL[`(\x. x rpow p)`;`(\x. p * x rpow (p - &1))`;`y:real`;`x:real`]REAL_MVT) );;
e( SUBGOAL_TAC""`~(y <= &0)` [ASM_REAL_ARITH_TAC]);;
e( ASM_SIMP_TAC [IN_ELIM_THM;real_interval] THEN BETA_TAC );;
e( ASM_SIMP_TAC [SIMP_RULE[IN_ELIM_THM;real_interval](SPECL[`real_interval [y,x:real]`;`p:real`]REAL_CONTINUOUS_ON_RPOW);] );;
e( SUBGOAL_TAC "" `(!x'. y < x' /\ x' < x ==> ((\x. x rpow p) has_real_derivative p * x' rpow (p - &1)) (atreal x'))` [ASM_MESON_TAC [HAS_REAL_DERIVATIVE_RPOW;REAL_ARITH`&1<=y /\ y<z ==> &0<z`]] );;
e( ASM_SIMP_TAC [] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC [REAL_ABS_MUL]);;
e( SUBGOAL_TAC""`abs (x - y) * abs p < e` [ASM_MESON_TAC [REAL_ABS_NZ;REAL_LT_RDIV_EQ]] );;
e( SUBGOAL_TAC""`~(x' = &0)` [ASM_REAL_ARITH_TAC] );;
e( SUBGOAL_TAC""`&0 < abs (x' rpow (&1 - p))` [ASM_MESON_TAC[REAL_ABS_NZ;RPOW_EQ_0]] );;
e( ASM_SIMP_TAC[REAL_ARITH`p - &1= --(&1 - p)`;RPOW_NEG;REAL_ABS_INV;REAL_RING`(a*s)*d=(a*d)*s:real`] THEN ASM_SIMP_TAC[GSYM real_div;REAL_LT_LDIV_EQ]);;
e( SUBGOAL_TAC""`&0 <= &1 /\ &1 <= abs x' /\ &0 <= &1 - p` [ASM_REAL_ARITH_TAC] );;
e( SUBGOAL_TAC""`e <= e * abs (x' rpow (&1 - p))` [ASM_MESON_TAC[REAL_ABS_RPOW;RPOW_LE2;RPOW_ONE;REAL_LE_LMUL_EQ;REAL_MUL_RID]] );;
e( ASM_REAL_ARITH_TAC );;
let lemma = MESON[REAL_ABS_SUB;REAL_LE_TOTAL]`(!x y. &1 <= x /\ &1 <= y /\ y <= x /\ abs (x - y) < d ==> abs (x rpow p - y rpow p) < e) <=> (!x y. &1 <= x /\ &1 <= y /\ abs (x - y) < d ==> abs (x rpow p - y rpow p) < e)`;;
let demo = ONCE_REWRITE_RULE[lemma](top_thm ());;
g `!p. p <= &1 ==> (\x. x rpow p) real_uniformly_continuous_on {x | &1 <= x}` ;;
e( SIMP_TAC [real_uniformly_continuous_on;IN_ELIM_THM] );;
e( MESON_TAC [demo] );;
top_thm();;
