legacy/oldnonlinear/nonlinear/partials.hl

   1
   2 (* for derivatives in 6 dimensions *)
   3
   4 let HAS_SIZE_6 = define_finite_type 6;;
   5
   6 let DIMINDEX_6 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_6;;
   7
   8 let lift_6 = new_definition `lift_6 (f:real->real->real->real->real->real->real) =
   9   (\ (v:real^6). lift (f (v$1) (v$2) (v$3) (v$4) (v$5) (v$6)) )`;;
  10
  11 let drop_6 = new_definition `drop_6 (f:real^6->real^1) =
  12   (\x1 x2 x3 x4 x5 x6. drop (f (vector [x1;x2;x3;x4;x5;x6])))`;;
  13
  14 let lambda_ext = prove_by_refinement(
  15   `!P Q.  (!i. 1 <= i /\ i <= dimindex (:B) ==> ((P:num->A) i = Q i)) =
  16     (((lambda i. P i):A^B) = (lambda i. Q i))`,
  17   (* {{{ proof *)
  18   [
  19 REPEAT STRIP_TAC ;
  20 REWRITE_TAC [GSYM LAMBDA_UNIQUE];
  21 SIMP_TAC [LAMBDA_BETA];
  22 MESON_TAC []
  23   ]);;
  24   (* }}} *)
  25
  26 let vector6 = prove_by_refinement(
  27   `!(v:real^6). vector [v$1; v$2; v$3; v$4; v$5; v$6] = v`,
  28   (* {{{ proof *)
  29   [
  30 REWRITE_TAC [vector;GSYM LAMBDA_UNIQUE];
  31 REWRITE_TAC [DIMINDEX_6;ARITH_RULE `1 <= i /\ i <=6 <=> (i=1 \/ i=2 \/ i=3 \/ i=4 \/ i=5 \/ i=6)`];
  32 REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[EL;HD;TL;ARITH_RULE `1-1=0 /\ 2 - 1 = SUC 0 /\ 3 - 1 =  SUC (SUC 0) /\ 4 - 1 = SUC (SUC(SUC 0)) /\ 5 - 1 = SUC (SUC(SUC(SUC 0))) /\ 6 - 1 = SUC(SUC(SUC(SUC(SUC 0))))`]
  33   ]);;
  34   (* }}} *)
  35
  36 let vector6_comp = prove_by_refinement(
  37   `!x1 x2 x3 x4 x5 x6.
  38     (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$1 = x1 /\
  39     (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$2 = x2 /\
  40     (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$3 = x3 /\
  41     (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$4 = x4 /\
  42     (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$5 = x5 /\
  43     (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$6 = x6
  44  `,
  45   (* {{{ proof *)
  46   [
  47 REWRITE_TAC [vector];
  48 SIMP_TAC [REWRITE_RULE[DIMINDEX_6] (INST_TYPE[`:6`,`:B`] LAMBDA_BETA); ARITH_RULE `1 <= 1 /\ 1 <=6 /\ 1 <= 2 /\ 2 <= 6 /\ 1 <= 3 /\ 3 <= 6 /\ 1 <= 4 /\ 4 <= 6 /\ 1 <= 5 /\ 5 <= 6 /\ 1 <= 6 /\ 6 <= 6 `;EL;HD;TL;ARITH_RULE `1-1=0 /\ 2 - 1 = SUC 0 /\ 3 - 1 =  SUC (SUC 0) /\ 4 - 1 = SUC (SUC(SUC 0)) /\ 5 - 1 = SUC (SUC(SUC(SUC 0))) /\ 6 - 1 = SUC(SUC(SUC(SUC(SUC 0))))`]
  49   ]);;
  50   (* }}} *)
  51
  52
  53 let lift6_drop6 = prove_by_refinement(
  54   `!f. lift_6 (drop_6 f) = f`,
  55   (* {{{ proof *)
  56   [
  57 REWRITE_TAC [lift_6;drop_6;lift;drop];
  58 GEN_TAC ;
  59 ONCE_REWRITE_TAC[FUN_EQ_THM];
  60 BETA_TAC;
  61 GEN_TAC ;
  62 REWRITE_TAC [(GSYM VECTOR_ONE)];
  63 AP_TERM_TAC ;
  64 REWRITE_TAC [vector6]
  65   ]);;
  66   (* }}} *)
  67
  68 let drop6_lift6 = prove_by_refinement(
  69   `!f. drop_6 (lift_6 f) = f`,
  70   (* {{{ proof *)
  71   [
  72 REWRITE_TAC [lift_6;drop_6;vector6_comp;LIFT_DROP];
  73 GEN_TAC ;
  74 REPEAT (MATCH_MP_TAC EQ_EXT THEN GEN_TAC);
  75 BETA_TAC;
  76 REWRITE_TAC []
  77   ]);;
  78   (* }}} *)
  79
  80
  81 (* f'' is the Hessian, viewed as a bilinear function at x.
  82    I plan to use this always on a product X of compact intervals in 6-d,
  83    such that X SUBSET P.  We should be able to take `s = (:real^6)` in every case. *)
  84
  85
  86 let derived_form2a = new_definition `derived_form2a
  87    p (f:real^6->real) (f':real^6->real^6->real)
  88    (f'':real^6 -> real^6 ->real^6 ->real) (x:real^6) (s:real^6->bool) =
  89    ((!(y:real^6). p y ==> ((has_derivative) (lift o f) (lift o (f' y)) (at y)) ) /\
  90   (!t.   p x ==> (has_derivative) (\u. lift (f' u t)) (\t'. lift (f'' x t t')) (at x within s)) /\
  91    (!(y:real^6) t t'. p y ==> (continuous) (\u. lift (f'' u t t')) (at y within s)))
  92    `;;
  93
  94
  95 let derived_form2b = new_definition `derived_form2b
  96    p (f:real^6->real) (f':real^6->real^6->real)
  97    (f'':real^6 -> real^6 ->real^6 ->real) (x:real^6) (s:real^6->bool) =
  98    ((!(y:real^6). p y ==> ((has_derivative) (lift o f) (lift o (f' y)) (at y)) ) /\
  99   (!t.   p x ==> (has_derivative) (\u. lift (f' u t)) (\t'. lift (f'' x t t')) (at x within s)) /\ ( open p) /\
 100    (!(y:real^6) t t'. p y ==> (continuous) (\u. lift (f'' u t t')) (at y within s)))
 101    `;;
 102
 103 (* Theorems needed:
 104
 105    1. Clairaut's theorem on equality of mixed partials.
 106    This uses the continuity and openness assumptions, so they have beeen added
 107    to derived_form2b.
 108    Many proofs are available, google search "Equality of Mixed Partials"
 109    For example, http://www.math.ubc.ca/~feldman/m226/mixed.pdf
 110
 111    2. Multivariate Taylor's theorem,
 112    This can be deduced from REAL_TAYLOR by
 113    taking t-derivative along a line segement `\t. f(x + t % v)`
 114
 115    3. Identification of Hessian as a bilinear function with the
 116    matrix of second partials. This should follow from JACOBIAN_WORKS.
 117
 118    Tactic needed:
 119    Automatic generation of derived_form2b from f.
 120  *)
 121
 122
 123 (*
 124 let mixed_equal = prove_by_refinement(
 125   `!f f' f'' x s.  derived_form2b p f f' f'' x s ==>
 126     (!t t'. p y ==> f'' y t t' = f'' y t' t)`,
 127   (* {{{ proof *)
 128   [
 129   ]);;
 130   (* }}} *)
 131 *)
 132
 133
 134
 135