Extended domain of rpow (powr)

src/probability/martingaleScript.sml

@@ -1898,6 +1898,12 @@ Proof
  >> PROVE_TAC [FCP_CONCAT_THM]
 QED
 
+Theorem pair_operation_CONS :
+    pair_operation (\x y. [x; y]) (EL 0) (EL 1)
+Proof
+    rw [pair_operation_def]
+QED
+
 val general_cross_def = Define
    ‘general_cross (cons :'a -> 'b -> 'c) A B = {cons a b | a IN A /\ b IN B}’;
 
@@ -7696,6 +7702,7 @@ Proof
  >> rw [extreal_abs_def]
  >> ‘0 < abs (a + b) /\ 0 < abs a /\ 0 < abs b’ by rw []
  >> rw [normal_powr, extreal_of_num_def, extreal_add_def, extreal_mul_def, extreal_le_eq]
+ >> ONCE_REWRITE_TAC [REAL_MUL_COMM]
  (* below is real-only *)
  >> MATCH_MP_TAC REAL_LE_TRANS
  >> Q.EXISTS_TAC ‘(max (abs a powr r) (abs b powr r)) * 2 powr r’

src/real/analysis/derivativeScript.sml

@@ -1704,6 +1704,7 @@ QED
 (* CONTINUOUS_ON_EXP                                                         *)
 (* ------------------------------------------------------------------------- *)
 
+(* See limTheory.HAS_DERIVATIVE_POW' for a better version without sum *)
 val HAS_DERIVATIVE_POW = store_thm ("HAS_DERIVATIVE_POW",
  ``!q0 n.
      ((\q. q pow n) has_derivative

src/real/analysis/limScript.sml

@@ -5,8 +5,8 @@
 open HolKernel Parse bossLib boolLib;
 
 open numLib reduceLib pairLib pairTheory arithmeticTheory numTheory jrhUtils
-     prim_recTheory realTheory realLib metricTheory netsTheory combinTheory;
-open pred_setTheory mesonLib;
+     prim_recTheory realTheory realLib metricTheory netsTheory combinTheory
+     pred_setTheory mesonLib hurdUtils;
 
 open topologyTheory real_topologyTheory derivativeTheory seqTheory;
 
@@ -15,17 +15,9 @@ val _ = ParseExtras.temp_loose_equality()
 
 val _ = Parse.reveal "B";
 
-(* mini hurdUtils *)
-val Know = Q_TAC KNOW_TAC;
-val Suff = Q_TAC SUFF_TAC;
-fun wrap a = [a];
-val Rewr = DISCH_THEN (REWRITE_TAC o wrap);
-val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);
-val POP_ORW = POP_ASSUM (ONCE_REWRITE_TAC o wrap);
-val art = ASM_REWRITE_TAC;
-
 val tendsto = netsTheory.tendsto;   (* conflict with real_topologyTheory.tendsto *)
 val GEN_ALL = hol88Lib.GEN_ALL;     (* this gives old (reverted) variable orders *)
+val EXACT_CONV = jrhUtils.EXACT_CONV; (* there's one also in hurdUtils *)
 
 (*---------------------------------------------------------------------------*)
 (* Specialize nets theorems to the pointwise limit of real->real functions   *)
@@ -700,6 +692,18 @@ val DIFF_POW = store_thm("DIFF_POW",
     REWRITE_TAC[ONE, pow] THEN
     REWRITE_TAC[SYM ONE, REAL_MUL_RID]]);
 
+val lemma = REWRITE_RULE [diffl_has_derivative, Once REAL_MUL_COMM] DIFF_POW;
+
+Theorem HAS_DERIVATIVE_POW' :
+    !n x. ((\x. x pow n) has_derivative (\y. &n * x pow (n - 1) * y)) (at x)
+Proof
+    REWRITE_TAC [lemma]
+QED
+
+(* !n x. ((\x. x pow n) has_vector_derivative &n * x pow (n - 1)) (at x) *)
+Theorem HAS_VECTOR_DERIVATIVE_POW =
+        REWRITE_RULE [diffl_has_vector_derivative] DIFF_POW
+
 (*---------------------------------------------------------------------------*)
 (* Now power of -1 (then differentiation of inverses follows from chain rule)*)
 (*---------------------------------------------------------------------------*)

src/real/analysis/real_topologyScript.sml

@@ -22,7 +22,7 @@ open numTheory numLib unwindLib tautLib prim_recTheory
      combinTheory quotientTheory arithmeticTheory realTheory real_sigmaTheory
      jrhUtils pairTheory boolTheory pred_setTheory optionTheory
      sumTheory InductiveDefinition listTheory mesonLib
-     RealArith realSimps topologyTheory metricTheory netsTheory;
+     realLib topologyTheory metricTheory netsTheory;
 
 open wellorderTheory cardinalTheory permutesTheory iterateTheory hurdUtils;
 
@@ -6229,22 +6229,39 @@ val LIM_TRANSFORM_WITHIN_SET_IMP = store_thm ("LIM_TRANSFORM_WITHIN_SET_IMP",
 (* Common case assuming being away from some crucial point like 0.           *)
 (* ------------------------------------------------------------------------- *)
 
-val LIM_TRANSFORM_AWAY_WITHIN = store_thm ("LIM_TRANSFORM_AWAY_WITHIN",
- ``!f:real->real g a b s. ~(a = b) /\
+Theorem LIM_TRANSFORM_AWAY_WITHIN_lemma[local] :
+   !f:real->real g a b s. ~(a = b) /\
   (!x. x IN s /\ ~(x = a) /\ ~(x = b) ==> (f(x) = g(x))) /\
-  (f --> l) (at a within s) ==> (g --> l) (at a within s)``,
+  (f --> l) (at a within s) ==> (g --> l) (at a within s)
+Proof
   REPEAT STRIP_TAC THEN MATCH_MP_TAC LIM_TRANSFORM_WITHIN THEN
   MAP_EVERY EXISTS_TAC [``f:real->real``, ``dist(a:real,b)``] THEN
   ASM_REWRITE_TAC[GSYM DIST_NZ] THEN X_GEN_TAC ``y:real`` THEN
   REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
-  ASM_MESON_TAC[DIST_SYM, REAL_LT_REFL]);
+  ASM_MESON_TAC[DIST_SYM, REAL_LT_REFL]
+QED
 
-val LIM_TRANSFORM_AWAY_AT = store_thm ("LIM_TRANSFORM_AWAY_AT",
- ``!f:real->real g a b. ~(a = b) /\
-  (!x. ~(x = a) /\ ~(x = b) ==> (f(x) = g(x))) /\
-  (f --> l) (at a) ==> (g --> l) (at a)``,
+(* NOTE: removed the unused quantifier ‘b’ *)
+Theorem LIM_TRANSFORM_AWAY_WITHIN :
+   !f:real->real g a s l.
+      (!x. x IN s /\ ~(x = a) ==> (f(x) = g(x))) /\
+      (f --> l) (at a within s) ==> (g --> l) (at a within s)
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC LIM_TRANSFORM_AWAY_WITHIN_lemma
+ >> qexistsl_tac [‘f’, ‘a + 1’] >> rw []
+ >> REAL_ARITH_TAC
+QED
+
+(* NOTE: removed the unused quantifier ‘b’ *)
+Theorem LIM_TRANSFORM_AWAY_AT :
+   !f:real->real g a l.
+      (!x. ~(x = a) ==> (f(x) = g(x))) /\
+      (f --> l) (at a) ==> (g --> l) (at a)
+Proof
   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
-  MESON_TAC[LIM_TRANSFORM_AWAY_WITHIN]);
+  MESON_TAC[LIM_TRANSFORM_AWAY_WITHIN]
+QED
 
 (* ------------------------------------------------------------------------- *)
 (* Alternatively, within an open set. *)
@@ -6261,6 +6278,21 @@ val LIM_TRANSFORM_WITHIN_OPEN = store_thm ("LIM_TRANSFORM_WITHIN_OPEN",
   STRIP_TAC THEN EXISTS_TAC ``e:real`` THEN POP_ASSUM MP_TAC THEN
   REWRITE_TAC[SUBSET_DEF, IN_BALL] THEN ASM_MESON_TAC[DIST_NZ, DIST_SYM]);
 
+Theorem LIM_TRANSFORM_WITHIN_OPEN_EQ :
+    !f g:real->real s a l.
+       open s /\ a IN s /\ (!x. x IN s /\ ~(x = a) ==> (f x = g x)) ==>
+      ((f --> l) (at a) <=> (g --> l) (at a))
+Proof
+    rpt STRIP_TAC
+ >> EQ_TAC >> DISCH_TAC
+ >| [ (* goal 1 (of 2) *)
+      MATCH_MP_TAC LIM_TRANSFORM_WITHIN_OPEN \\
+      qexistsl_tac [‘f’, ‘s’] >> rw [],
+      (* goal 2 (of 2) *)
+      MATCH_MP_TAC LIM_TRANSFORM_WITHIN_OPEN \\
+      qexistsl_tac [‘g’, ‘s’] >> rw [] ]
+QED
+
 val LIM_TRANSFORM_WITHIN_OPEN_IN = store_thm ("LIM_TRANSFORM_WITHIN_OPEN_IN",
  ``!f g:real->real s t a l.
   open_in (subtopology euclidean t) s /\ a IN s /\