text_formalization/local/PCRTTID.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Local Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2012-04-01                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11
  12
  13 module   Pcrttid= struct
  14
  15
  16
  17
  18
  19 open Polyhedron;;
  20 open Sphere;;
  21 open Topology;;
  22 open Fan_misc;;
  23 open Planarity;;
  24 open Conforming;;
  25 open Hypermap;;
  26 open Fan;;
  27 open Topology;;
  28 open Wrgcvdr_cizmrrh;;
  29 open Local_lemmas;;
  30 open Collect_geom;;
  31 open Dih2k_hypermap;;
  32 open Wjscpro;;
  33 open Tecoxbm;;
  34 open Hdplygy;;
  35 open Nkezbfc_local;;
  36 open Flyspeck_constants;;
  37 open Gbycpxs;;
  38
  39
  40
  41 let tri_stable=new_definition
  42 `tri_stable k d s a b J f<=>
  43 constraint_system k d s a b J f /\ k=3
  44 /\
  45 (!i j. i IN s /\ j IN s /\ ~(i=j) ==> &2<= a(i,j)) /\
  46 (!i. i IN s==> a(i,i)= &0 /\ b(i,f i)< &4)/\
  47 (!i j.  {i,j} IN J ==> a(i,j)= sqrt(&8) /\ b(i,j) =cstab)`;;
  48
  49
  50
  51 let EAR_TRI_STABLE_SYSTEM=prove_by_refinement(
  52 `tri_stable 3 ((#0.11)) (0..2) (a_ear0 {{1,2}}) (b_ear0 {{1,2}})  ({{1,2}}) (\i. (1 + i) MOD 3)`,
  53 [
  54 MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`2`][ARITH_RULE`(2+1)-0=3`]
  55 THEN ASM_SIMP_TAC[tri_stable;constraint_system;torsor;ARITH_RULE`3<= 3 /\3<=6/\ 1+3<=6/\ (2+1)-0=3/\ 3=3`;CARD_NUMSEG;Hypermap.CARD_SINGLETON;]
  56 THEN REMOVE_ASSUM_TAC
  57 THEN STRIP_TAC;
  58 STRIP_TAC;
  59 STRIP_TAC;
  60 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
  61 THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`2`[ARITH_RULE`SUC 2=3`];
  62 STRIP_TAC;
  63 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
  64 THEN REPEAT STRIP_TAC
  65 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`3`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=3<=> A<=2)`]
  66 THEN POP_ASSUM MP_TAC
  67 THEN ARITH_TAC;
  68 STRIP_TAC;
  69 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
  70 THEN REPEAT STRIP_TAC
  71 THEN POP_ASSUM MP_TAC
  72 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i /\ 1<3`)
  73 THEN RESA_TAC
  74 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`i:num`]
  75 THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2`)
  76 THEN RESA_TAC
  77 THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
  78 THEN ASM_REWRITE_TAC[]
  79 THEN RESA_TAC
  80 THEN ARITH_TAC;
  81 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
  82 THEN REPEAT STRIP_TAC
  83 THEN ASSUME_TAC(ARITH_RULE`1<=3 /\1<3/\ 1<=2`)
  84 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`3:num`]
  85 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`x:num`][ARITH_RULE`1*3=3`]
  86 THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
  87 THEN ASM_REWRITE_TAC[]
  88 THEN RESA_TAC
  89 THEN ARITH_TAC;
  90 STRIP_TAC;
  91 REWRITE_TAC[b_ear0;a_ear0]
  92 THEN REPEAT GEN_TAC
  93 THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =j MOD 3 \/ ~(i  MOD 3 =j MOD 3:num)`);
  94 ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`];
  95 ASM_REWRITE_TAC[]
  96 THEN  DISJ_CASES_TAC(SET_RULE`{i MOD 3,j MOD 3} IN {{1,2}} \/ ~({i MOD 3,j MOD 3} IN {{1,2}})`);
  97 ASM_REWRITE_TAC[IN_SING]
  98 THEN ONCE_REWRITE_TAC[SET_RULE`{i  MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i  MOD 3}= {1,2}`]
  99 THEN POP_ASSUM MP_TAC
 100 THEN ASM_REWRITE_TAC[IN_SING;cstab]
 101 THEN RESA_TAC
 102 THEN MATCH_MP_TAC REAL_LE_LSQRT
 103 THEN REAL_ARITH_TAC;
 104 ASM_REWRITE_TAC[IN_SING]
 105 THEN ONCE_REWRITE_TAC[SET_RULE`{i MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i MOD 3}= {1,2}`]
 106 THEN POP_ASSUM MP_TAC
 107 THEN ASM_REWRITE_TAC[IN_SING;h0]
 108 THEN RESA_TAC
 109 THEN REAL_ARITH_TAC;
 110 STRIP_TAC;
 111 REPEAT GEN_TAC
 112 THEN MP_TAC(ARITH_RULE`1<= 3 /\ 1<3`)
 113 THEN RESA_TAC
 114 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`j:num`][ARITH_RULE`1*3=3`]
 115 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`j:num`;`3:num`]
 116 THEN SIMP_TAC[b_ear0;a_ear0;ARITH_RULE`A+0=A`;MOD_MOD_REFL;ARITH_RULE`~(3=0)`];
 117 REWRITE_TAC[SUBSET;IN_SING;IN_ELIM_THM;IN_NUMSEG]
 118 THEN REPEAT STRIP_TAC
 119 THEN EXISTS_TAC`1`
 120 THEN ASM_REWRITE_TAC[ARITH_RULE`0<=1 /\ 1<=2/\ (1 +1 ) MOD 3= 2`];
 121 STRIP_TAC;
 122 REWRITE_TAC[a_ear0;IN_NUMSEG]
 123 THEN REPEAT STRIP_TAC
 124 THEN MP_TAC(ARITH_RULE`i<= 2/\ j<= 2==> i< 3 /\ j< 3`)
 125 THEN RESA_TAC
 126 THEN MRESA_TAC MOD_LT[`i:num`;`3`]
 127 THEN MRESA_TAC MOD_LT[`j:num`;`3`]
 128 THEN  DISJ_CASES_TAC(SET_RULE`{i,j} IN {{1,2}} \/ ~({i,j} IN {{1,2}})`);
 129 ASM_REWRITE_TAC[]
 130 THEN MATCH_MP_TAC REAL_LE_RSQRT
 131 THEN REAL_ARITH_TAC;
 132 ASM_REWRITE_TAC[]
 133 THEN REAL_ARITH_TAC;
 134 STRIP_TAC;
 135 REWRITE_TAC[b_ear0;a_ear0;MOD_MOD_REFL]
 136 THEN REPEAT STRIP_TAC
 137 THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =(1+i) MOD 3 MOD 3\/ ~(i  MOD 3 =(1+i) MOD 3 MOD 3:num)`);
 138 ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`;cstab]
 139 THEN REAL_ARITH_TAC;
 140 ASM_REWRITE_TAC[]
 141 THEN  DISJ_CASES_TAC(SET_RULE`{i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}} \/ ~({i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}})`);
 142 ASM_REWRITE_TAC[cstab;h0]
 143 THEN REAL_ARITH_TAC;
 144 ASM_REWRITE_TAC[h0;cstab]
 145 THEN REAL_ARITH_TAC;
 146 REWRITE_TAC[IN_SING;a_ear0;b_ear0]
 147 THEN REPEAT STRIP_TAC
 148 THEN MP_TAC(SET_RULE`{i,j}={1,2} /\ ~(1=2) ==> ~(i=j) /\ (i =1\/ i=2) /\ (j=1\/ j=2)`)
 149 THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=2)`]
 150 THEN DISCH_TAC
 151 THEN MP_TAC(ARITH_RULE`(i =1\/ i=2) /\ (j=1\/ j=2)==> i< 3 /\ j< 3`)
 152 THEN RESA_TAC
 153 THEN MRESA_TAC MOD_LT[`i:num`;`3`]
 154 THEN MRESA_TAC MOD_LT[`j:num`;`3`]]);;
 155
 156
 157
 158
 159 let exist_tri_stable=prove_by_refinement(`?s:(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num)). tri_stable (FST s) (FST (SND s)) (FST (SND (SND s))) (FST (SND (SND (SND s)))) (FST(SND (SND (SND (SND s))))) (FST (SND (SND (SND (SND (SND s))))))
 160 (SND(SND (SND (SND (SND (SND s))))))`,
 161 [EXISTS_TAC`3, (#0.11), (0..2), (a_ear0 {{1,2}}), (b_ear0 {{1,2}}), ({{1,2}}),(\i. (1 + i) MOD 3)`
 162 THEN REWRITE_TAC[EAR_TRI_STABLE_SYSTEM]]);;
 163
 164
 165 let tri_sy_tybij = (new_type_definition "tri_sy" ("tri_sy", "tuple_tri_sy")exist_tri_stable);;
 166
 167
 168 let k_ts = new_definition `k_ts (s:tri_sy) = FST (tuple_tri_sy s)`;;
 169
 170 let d_ts = new_definition `d_ts (s:tri_sy) = (FST (SND (tuple_tri_sy s)))`;;
 171
 172 let I_TS = new_definition `I_TS (s:tri_sy) = (FST (SND (SND  (tuple_tri_sy s))))`;;
 173
 174 let a_ts = new_definition `a_ts (s:tri_sy) = (FST (SND (SND (SND (tuple_tri_sy s)))))`;;
 175
 176 let b_ts = new_definition `b_ts (s:tri_sy) = (FST(SND (SND (SND (SND (tuple_tri_sy s)))))) `;;
 177
 178
 179 let J_TS = new_definition `J_TS (s:tri_sy) = (FST (SND (SND (SND (SND (SND  (tuple_tri_sy s))))))) `;;
 180
 181 let f_ts = new_definition `f_ts (s:tri_sy) = (SND(SND (SND (SND (SND (SND  (tuple_tri_sy s)))))))`;;
 182
 183
 184
 185 let tri_sy_lemma=prove(`!s:tri_sy. tri_stable (k_ts s) (d_ts s) (I_TS s) (a_ts s) (b_ts s) (J_TS s) (f_ts s)`,
 186    ASM_REWRITE_TAC[tri_sy_tybij;k_ts;d_ts;I_TS; a_ts; b_ts; J_TS; f_ts]);;
 187
 188
 189
 190
 191
 192
 193 let augmented_constraint_system1=new_definition
 194 `augmented_constraint_system1 (s:stable_sy) I_lo I_str a b m <=>
 195 d_sy s <= # 0.9
 196 /\ m=CARD {i | i IN I_SY s /\ (?j. j IN I_SY s /\( &2< a_sy s (i,j) \/ &2* h0< b_sy s (i,j)))} DIV 2
 197 /\ m+k_sy s <= 6
 198 /\ (!i j. i IN I_SY s /\ j IN I_SY s ==>
 199 a_sy s (i,j)<= a (i,j)
 200 /\ a (i,j)<= b (i,j)
 201 /\ b (i,j)<= b_sy s (i,j))`;;
 202
 203
 204
 205 let augmented_constraint_system2=new_definition
 206 `augmented_constraint_system3 (s:tri_sy) I_lo I_str a b m <=>
 207 d_ts s <= # 0.9
 208 /\ m=CARD {i | i IN I_TS s /\ (?j. j IN I_TS s /\( &2< a_ts s (i,j) \/ &2* h0< b_ts s (i,j)))} DIV 2
 209 /\ m+k_ts s <= 6
 210 /\ (!i j. i IN I_TS s /\ j IN I_TS s ==>
 211 a_ts s (i,j)<= a (i,j)
 212 /\ a (i,j)<= b (i,j)
 213 /\ b (i,j)<= b_ts s (i,j))`;;
 214
 215
 216
 217
 218 let CLOSED_TRI_SY=prove_by_refinement(`
 219 tri_stable k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
 220 /\ 2<k
 221 ==>
 222 closed {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }`,
 223 [REWRITE_TAC[CONDITION2_SY;CONDITION1_SY;tri_stable]
 224 THEN  REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN  REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist]
 225 THEN REPEAT STRIP_TAC
 226 THEN ASM_TAC
 227 THEN DISCH_THEN(LABEL_TAC"THYGIANG2")
 228 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
 229 THEN DISCH_THEN(LABEL_TAC"THYGIANG1")
 230 THEN REPEAT STRIP_TAC
 231 THEN EXISTS_TAC`vecmats (l:real^(M,3)finite_product)`
 232 THEN SIMP_TAC[MATVEC_VECMATS_ID]
 233 THEN POP_ASSUM MP_TAC
 234 THEN POP_ASSUM MP_TAC
 235 THEN   REWRITE_TAC[SKOLEM_THM]
 236 THEN STRIP_TAC
 237 THEN POP_ASSUM MP_TAC
 238 THEN  DISCH_THEN(LABEL_TAC"THY1")
 239 THEN  DISCH_THEN(LABEL_TAC"THY2")
 240 THEN SUBGOAL_THEN`
 241 !i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M)
 242 ==>
 243 ((\n. row i (v n) - row j ((v:num->real^3^M) n)) --> row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product)))
 244  sequentially`ASSUME_TAC;
 245 SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]
 246 THEN REPEAT STRIP_TAC
 247 THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`]
 248 THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`)
 249 THEN RESA_TAC
 250 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e/ &2:real`)
 251 THEN POP_ASSUM MP_TAC
 252 THEN  DISCH_THEN(LABEL_TAC"THY2")
 253 THEN EXISTS_TAC`N:num`
 254 THEN REPEAT STRIP_TAC
 255 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)
 256 THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\  SUC(i-1)=i`)
 257 THEN RESA_TAC
 258 THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\  SUC(j-1)=j`)
 259 THEN RESA_TAC
 260 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`]
 261 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`]
 262 THEN POP_ASSUM MP_TAC
 263 THEN SIMP_TAC[MATVEC_VECMATS_ID]
 264 THEN STRIP_TAC
 265 THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]
 266 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`((v:num->real^3^M) n)`]
 267 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`vecmats (l:real^(M,3)finite_product)`]
 268 THEN POP_ASSUM MP_TAC
 269 THEN SIMP_TAC[MATVEC_VECMATS_ID]
 270 THEN STRIP_TAC
 271 THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`j-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]
 272 THEN MRESAL_TAC NORM_TRIANGLE[`row i ((v:num->real^3^M) n) - row i (vecmats (l:real^(M,3)finite_product))`;`--(row j ((v:num->real^3^M) n) - row j (vecmats (l:real^(M,3)finite_product)))`][NORM_NEG;VECTOR_ARITH`A+ --B=A-B:real^N` ]
 273 THEN POP_ASSUM MP_TAC
 274 THEN POP_ASSUM MP_TAC
 275 THEN REMOVE_ASSUM_TAC
 276 THEN REMOVE_ASSUM_TAC
 277 THEN POP_ASSUM MP_TAC
 278 THEN REMOVE_ASSUM_TAC
 279 THEN REMOVE_ASSUM_TAC
 280 THEN REMOVE_ASSUM_TAC
 281 THEN REMOVE_ASSUM_TAC
 282 THEN REMOVE_ASSUM_TAC
 283 THEN REMOVE_ASSUM_TAC
 284 THEN POP_ASSUM MP_TAC
 285 THEN REAL_ARITH_TAC;
 286 SUBGOAL_THEN`
 287 !i. 1 <= i /\ i <= dimindex (:M) ==>
 288 ((\n. row i ((v:num->real^3^M) n)) --> row i (vecmats (l:real^(M,3)finite_product)))
 289  sequentially`ASSUME_TAC;
 290 SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]
 291 THEN REPEAT STRIP_TAC
 292 THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`]
 293 THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`)
 294 THEN RESA_TAC
 295 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e:real`)
 296 THEN POP_ASSUM MP_TAC
 297 THEN  DISCH_THEN(LABEL_TAC"THY2")
 298 THEN EXISTS_TAC`N:num`
 299 THEN REPEAT STRIP_TAC
 300 THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)
 301 THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\  SUC(i-1)=i`)
 302 THEN RESA_TAC
 303 THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\  SUC(j-1)=j`)
 304 THEN RESA_TAC
 305 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`]
 306 THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`]
 307 THEN POP_ASSUM MP_TAC
 308 THEN SIMP_TAC[MATVEC_VECMATS_ID]
 309 THEN STRIP_TAC
 310 THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]
 311 THEN POP_ASSUM MP_TAC
 312 THEN REMOVE_ASSUM_TAC
 313 THEN REMOVE_ASSUM_TAC
 314 THEN REMOVE_ASSUM_TAC
 315 THEN REMOVE_ASSUM_TAC
 316 THEN REMOVE_ASSUM_TAC
 317 THEN POP_ASSUM MP_TAC
 318 THEN REAL_ARITH_TAC;
 319 POP_ASSUM MP_TAC
 320 THEN DISCH_THEN(LABEL_TAC"YEU2")
 321 THEN SUBGOAL_THEN`(!i j.
 322       1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M)
 323       ==> (a:num#num->real) (i,j) <= norm (row i (vecmats l) - row j (vecmats l)) /\
 324           norm (row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))) <= (b:num#num->real) (i,j))` ASSUME_TAC;
 325 REPEAT STRIP_TAC;
 326 MRESA_TAC LIM_NORM_LBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(a:num#num->real)(i,j)`]
 327 THEN POP_ASSUM MATCH_MP_TAC
 328 THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY];
 329 MRESA_TAC LIM_NORM_UBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(b:num#num->real)(i,j)`]
 330 THEN POP_ASSUM MATCH_MP_TAC
 331 THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY];
 332 ASM_REWRITE_TAC[]
 333 THEN MP_TAC COMPACT_BALL_ANNULUS
 334 THEN ASM_SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED]
 335 THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN  REWRITE_TAC[ IN_ELIM_THM; dist]
 336 THEN   REWRITE_TAC[SKOLEM_THM]
 337 THEN STRIP_TAC
 338 THEN POP_ASSUM MP_TAC
 339 THEN DISCH_THEN(LABEL_TAC"YEU")
 340 THEN REPEAT STRIP_TAC
 341 THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`(\n. row i ((v:num->real^3^M) n)) `;` row i (vecmats (l:real^(M,3)finite_product))`])
 342 THEN POP_ASSUM MATCH_MP_TAC
 343 THEN ASM_SIMP_TAC[]]);;
 344
 345
 346
 347
 348
 349 let BOUNDED_TRI_SY=prove(`
 350 tri_stable k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
 351 /\  2<k
 352 ==>
 353 bounded {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v}`,
 354 REPEAT STRIP_TAC
 355 THEN MATCH_MP_TAC BOUNDED_SUBSET
 356 THEN EXISTS_TAC`{matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) }`
 357 THEN MP_TAC COMPACT_BALL_ANNULUS_MATVEC
 358 THEN SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED]
 359 THEN RESA_TAC
 360 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
 361 THEN SET_TAC[]);;
 362
 363 let COMPACT_TRI_STABLE= prove (`
 364 tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
 365 /\ 2<k
 366 ==>
 367 compact {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  }`,
 368 SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_TRI_SY; CLOSED_TRI_SY;]
 369 THEN REPEAT STRIP_TAC
 370 THEN MP_TAC(ARITH_RULE`2<k ==> 1<k`)
 371 THEN RESA_TAC
 372 THENL[ MRESA_TAC (GEN_ALL BOUNDED_TRI_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;];
 373 MRESA_TAC (GEN_ALL CLOSED_TRI_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;]]);;
 374
 375
 376
 377
 378
 379
 380
 381 let PCRTTID=prove(`(!d J k a b.
 382 tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
 383 /\ 2<k
 384 ==>
 385 compact {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  })
 386 /\ (!d J k a b.
 387 stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
 388 /\ 2<k
 389 ==>
 390 compact {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v /\ CONDITION2_SY v })`,
 391 STRIP_TAC
 392 THEN REPEAT GEN_TAC
 393 THEN MESON_TAC[COMPACT_TRI_STABLE;WJSCPRO]);;
 394
 395
 396
 397
 398
 399 end;;
 400
 401