100/lhopital.ml

   1 (* ========================================================================= *)
   2 (* #64: L'Hopital's rule.                                                    *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/analysis.ml";;
   6
   7 override_interface ("-->",`(tends_real_real)`);;
   8
   9 prioritize_real();;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Cauchy mean value theorem.                                                *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let MVT2 = prove
  16  (`!f g a b.
  17         a < b /\
  18         (!x. a <= x /\ x <= b ==> f contl x /\ g contl x) /\
  19         (!x. a < x /\ x < b ==> f differentiable x /\ g differentiable x)
  20         ==> ?z f' g'. a < z /\ z < b /\ (f diffl f') z /\ (g diffl g') z /\
  21                       (f b - f a) * g' = (g b - g a) * f'`,
  22   REPEAT STRIP_TAC THEN
  23   MP_TAC(SPECL [`\x:real. f(x) * (g(b) - g(a)) - g(x) * (f(b) - f(a))`;
  24                 `a:real`; `b:real`] MVT) THEN
  25   ANTS_TAC THENL
  26    [ASM_SIMP_TAC[CONT_SUB; CONT_MUL; CONT_CONST] THEN
  27     X_GEN_TAC `x:real` THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
  28     REWRITE_TAC[differentiable] THEN
  29     DISCH_THEN(CONJUNCTS_THEN2
  30      (X_CHOOSE_TAC `f':real`) (X_CHOOSE_TAC `g':real`)) THEN
  31     EXISTS_TAC `f' * (g(b:real) - g a) - g' * (f b - f a)` THEN
  32     ASM_SIMP_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] DIFF_CMUL; DIFF_SUB];
  33     ALL_TAC] THEN
  34   GEN_REWRITE_TAC LAND_CONV [SWAP_EXISTS_THM] THEN
  35   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `z:real` THEN
  36   REWRITE_TAC[REAL_ARITH
  37    `(fb * (gb - ga) - gb * (fb - fa)) -
  38     (fa * (gb - ga) - ga * (fb - fa)) = y <=> y = &0`] THEN
  39   ASM_SIMP_TAC[REAL_ENTIRE; REAL_SUB_0; REAL_LT_IMP_NE] THEN
  40   DISCH_THEN(X_CHOOSE_THEN `l:real` STRIP_ASSUME_TAC) THEN
  41   UNDISCH_THEN `l = &0` SUBST_ALL_TAC THEN
  42   UNDISCH_TAC
  43    `!x. a < x /\ x < b ==> f differentiable x /\ g differentiable x` THEN
  44   DISCH_THEN(MP_TAC o SPEC `z:real`) THEN ASM_REWRITE_TAC[differentiable] THEN
  45   DISCH_THEN(CONJUNCTS_THEN2
  46      (X_CHOOSE_TAC `f':real`) (X_CHOOSE_TAC `g':real`)) THEN
  47   MAP_EVERY EXISTS_TAC [`f':real`; `g':real`] THEN
  48   ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
  49   CONV_TAC SYM_CONV THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
  50   MATCH_MP_TAC DIFF_UNIQ THEN
  51   EXISTS_TAC `\x:real. f(x) * (g(b) - g(a)) - g(x) * (f(b) - f(a))` THEN
  52   EXISTS_TAC `z:real` THEN
  53   ASM_SIMP_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] DIFF_CMUL; DIFF_SUB]);;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* First, assume f and g actually take value zero at c.                      *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 let LHOPITAL_WEAK = prove
  60  (`!f g f' g' c L d.
  61         &0 < d /\
  62         (!x. &0 < abs(x - c) /\ abs(x - c) < d
  63              ==> (f diffl f'(x)) x /\ (g diffl g'(x)) x /\ ~(g'(x) = &0)) /\
  64         f(c) = &0 /\ g(c) = &0 /\ (f --> &0) c /\ (g --> &0) c /\
  65         ((\x. f'(x) / g'(x)) --> L) c
  66         ==> ((\x. f(x) / g(x)) --> L) c`,
  67   REPEAT STRIP_TAC THEN SUBGOAL_THEN
  68    `!x. &0 < abs(x - c) /\ abs(x - c) < d
  69         ==> ?z. &0 < abs(z - c) /\ abs(z - c) < abs(x - c) /\
  70                 f(x) * g'(z) = f'(z) * g(x)`
  71   (LABEL_TAC "*") THENL
  72    [X_GEN_TAC `x:real` THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
  73      `&0 < abs(x - c) /\ abs(x - c) < d
  74       ==> c < x /\ x < c + d \/ c - d < x /\ x < c`)) THEN
  75     STRIP_TAC THENL
  76      [MP_TAC(SPECL
  77        [`f:real->real`; `g:real->real`; `c:real`; `x:real`] MVT2) THEN
  78       ANTS_TAC THENL
  79        [ASM_REWRITE_TAC[] THEN
  80         GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o funpow 2 LAND_CONV)
  81           [REAL_LE_LT] THEN
  82         ASM_MESON_TAC[CONTL_LIM; DIFF_CONT; REAL_LT_IMP_LE; differentiable;
  83           REAL_ARITH
  84           `c < z /\ z <= x /\ x < c + d ==> &0 < abs(z - c) /\ abs(z - c) < d`];
  85         ALL_TAC] THEN
  86       ASM_REWRITE_TAC[REAL_SUB_RZERO] THEN MATCH_MP_TAC MONO_EXISTS THEN
  87       GEN_TAC THEN GEN_REWRITE_TAC (funpow 4 RAND_CONV) [REAL_MUL_SYM] THEN
  88       REPEAT STRIP_TAC THENL
  89        [ASM_REAL_ARITH_TAC;
  90         ASM_REAL_ARITH_TAC;
  91         FIRST_X_ASSUM(fun th -> MP_TAC th THEN
  92           MATCH_MP_TAC EQ_IMP THEN BINOP_TAC) THEN
  93         ASM_MESON_TAC[DIFF_UNIQ; REAL_ARITH
  94          `c < z /\ z < x /\ x < c + d ==> &0 < abs(z - c) /\ abs(z - c) < d`]];
  95       MP_TAC(SPECL
  96        [`f:real->real`; `g:real->real`; `x:real`; `c:real`] MVT2) THEN
  97       ANTS_TAC THENL
  98        [ASM_REWRITE_TAC[] THEN
  99         GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o LAND_CONV o RAND_CONV)
 100           [REAL_LE_LT] THEN
 101         ASM_MESON_TAC[CONTL_LIM; DIFF_CONT; REAL_LT_IMP_LE; differentiable;
 102           REAL_ARITH
 103           `c - d < x /\ x <= z /\ z < c ==> &0 < abs(z - c) /\ abs(z - c) < d`];
 104         ALL_TAC] THEN
 105       ASM_REWRITE_TAC[REAL_SUB_LZERO; REAL_MUL_LNEG; REAL_EQ_NEG2] THEN
 106       MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
 107       GEN_REWRITE_TAC (funpow 4 RAND_CONV) [REAL_MUL_SYM] THEN
 108       REPEAT STRIP_TAC THENL
 109        [ASM_REAL_ARITH_TAC;
 110         ASM_REAL_ARITH_TAC;
 111         FIRST_X_ASSUM(fun th -> MP_TAC th THEN
 112          MATCH_MP_TAC EQ_IMP THEN BINOP_TAC) THEN
 113         ASM_MESON_TAC[DIFF_UNIQ; REAL_ARITH
 114          `c - d < x /\ x < z /\ z < c
 115           ==> &0 < abs(z - c) /\ abs(z - c) < d`]]];
 116     ALL_TAC] THEN
 117   REWRITE_TAC[LIM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 118   UNDISCH_TAC `((\x. f' x / g' x) --> L) c` THEN REWRITE_TAC[LIM] THEN
 119   DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
 120   DISCH_THEN(X_CHOOSE_THEN `r:real` STRIP_ASSUME_TAC) THEN
 121   MP_TAC(SPECL [`d:real`; `r:real`] REAL_DOWN2) THEN ASM_REWRITE_TAC[] THEN
 122   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:real` THEN STRIP_TAC THEN
 123   ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:real` THEN STRIP_TAC THEN
 124   UNDISCH_TAC
 125    `!x. &0 < abs(x - c) /\ abs(x - c) < r ==> abs(f' x / g' x - L) < e` THEN
 126   REMOVE_THEN "*" (MP_TAC o SPEC `x:real`) THEN
 127   ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 128   DISCH_THEN(X_CHOOSE_THEN `z:real` STRIP_ASSUME_TAC) THEN
 129   DISCH_THEN(MP_TAC o SPEC `z:real`) THEN
 130   ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 131   MATCH_MP_TAC(REAL_ARITH `x = y ==> abs(x - l) < e ==> abs(y - l) < e`) THEN
 132   MATCH_MP_TAC(REAL_FIELD
 133    `~(gz = &0) /\ ~(gx = &0) /\ fx * gz = fz * gx ==> fz / gz = fx / gx`) THEN
 134   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 135    [ASM_MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN
 136   MP_TAC(ASSUME `&0 < abs(x - c)`) THEN DISCH_THEN(MP_TAC o MATCH_MP
 137    (REAL_ARITH `&0 < abs(x - c) ==> c < x \/ x < c`)) THEN
 138   REPEAT STRIP_TAC THENL
 139    [MP_TAC(SPECL [`g:real->real`; `c:real`; `x:real`] ROLLE) THEN
 140     ASM_REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC] THEN CONJ_TAC THENL
 141      [GEN_TAC THEN GEN_REWRITE_TAC (funpow 2 LAND_CONV) [REAL_LE_LT] THEN
 142       ASM_MESON_TAC[CONTL_LIM; DIFF_CONT; REAL_LT_TRANS; REAL_ARITH
 143        `c < z /\ z <= x /\ abs(x - c) < d
 144         ==> &0 < abs(z - c) /\ abs(z - c) < d`];
 145       ALL_TAC] THEN
 146     CONJ_TAC THENL
 147      [ASM_MESON_TAC[differentiable; REAL_LT_TRANS; REAL_ARITH
 148        `c < z /\ z < x /\ abs(x - c) < d
 149         ==> &0 < abs(z - c) /\ abs(z - c) < d`];
 150       ALL_TAC] THEN
 151     REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `w:real` THEN STRIP_TAC THEN
 152     FIRST_X_ASSUM(MP_TAC o SPEC `w:real`) THEN
 153     ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 154     ASM_MESON_TAC[DIFF_UNIQ];
 155     MP_TAC(SPECL [`g:real->real`; `x:real`; `c:real`] ROLLE) THEN
 156     ASM_REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC] THEN CONJ_TAC THENL
 157      [GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [REAL_LE_LT] THEN
 158       ASM_MESON_TAC[CONTL_LIM; DIFF_CONT; REAL_LT_TRANS; REAL_ARITH
 159        `x <= z /\ z < c /\ z < c /\ abs(x - c) < d
 160         ==> &0 < abs(z - c) /\ abs(z - c) < d`];
 161       ALL_TAC] THEN
 162     CONJ_TAC THENL
 163      [ASM_MESON_TAC[differentiable; REAL_LT_TRANS; REAL_ARITH
 164        `x < z /\ z < c /\ abs(x - c) < d
 165         ==> &0 < abs(z - c) /\ abs(z - c) < d`];
 166       ALL_TAC] THEN
 167     REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `w:real` THEN STRIP_TAC THEN
 168     FIRST_X_ASSUM(MP_TAC o SPEC `w:real`) THEN
 169     ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 170     ASM_MESON_TAC[DIFF_UNIQ]]);;
 171
 172 (* ------------------------------------------------------------------------- *)
 173 (* Now generalize by continuity extension.                                   *)
 174 (* ------------------------------------------------------------------------- *)
 175
 176 let LHOPITAL = prove
 177  (`!f g f' g' c L d.
 178         &0 < d /\
 179         (!x. &0 < abs(x - c) /\ abs(x - c) < d
 180              ==> (f diffl f'(x)) x /\ (g diffl g'(x)) x /\ ~(g'(x) = &0)) /\
 181         (f --> &0) c /\ (g --> &0) c /\ ((\x. f'(x) / g'(x)) --> L) c
 182         ==> ((\x. f(x) / g(x)) --> L) c`,
 183   REPEAT GEN_TAC THEN
 184   MP_TAC(SPECL [`\x:real. if x = c then &0 else f(x)`;
 185                 `\x:real. if x = c then &0 else g(x)`;
 186                 `f':real->real`; `g':real->real`;
 187                 `c:real`; `L:real`; `d:real`] LHOPITAL_WEAK) THEN
 188   SIMP_TAC[LIM; REAL_ARITH `&0 < abs(x - c) ==> ~(x = c)`] THEN
 189   REWRITE_TAC[diffl] THEN STRIP_TAC THEN STRIP_TAC THEN
 190   FIRST_X_ASSUM MATCH_MP_TAC THEN
 191   ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[diffl] THENL
 192    [MATCH_MP_TAC LIM_TRANSFORM THEN EXISTS_TAC `\h. (f(x + h) - f x) / h`;
 193     MATCH_MP_TAC LIM_TRANSFORM THEN EXISTS_TAC `\h. (g(x + h) - g x) / h`;
 194     ASM_MESON_TAC[]] THEN
 195   ASM_SIMP_TAC[REAL_ARITH `&0 < abs(x - c) ==> ~(x = c)`] THEN
 196   REWRITE_TAC[LIM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 197   EXISTS_TAC `abs(x - c)` THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
 198   ASM_SIMP_TAC[REAL_ARITH
 199    `&0 < abs(x - c) /\ &0 < abs z /\ abs z < abs(x - c) ==> ~(x + z = c)`] THEN
 200   ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_ABS_NUM]);;