2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Local Fan *)
6 (* Author: Hoang Le Truong *)
8 (* ========================================================================= *)
13 module Hdplygy = struct
33 open Prove_by_refinement;;
35 open Wrgcvdr_cizmrrh;;
41 let a_ear0=new_definition`a_ear0 J (i,j)=( if i MOD 3=j MOD 3 then &0 else
42 (if {i MOD 3,j MOD 3} IN J then sqrt(&8) else &2)) `;;
44 let b_ear0=new_definition`b_ear0 J (i,j)=( if i MOD 3=j MOD 3 then &0 else
45 (if {i MOD 3,j MOD 3} IN J then cstab else &2* h0)) `;;
48 let MOD_EQ_MOD1=prove(`!x1 x2 y n. ~(n=0) /\ (y + x1) MOD n = (y + x2) MOD n /\ x2<= x1
49 ==> x1 MOD n = x2 MOD n`,
51 THEN MRESA_TAC DIVISION[`y+x1:num`;`n:num`]
52 THEN MRESA_TAC DIVISION[`y+x2:num`;`n:num`]
53 THEN MP_TAC(ARITH_RULE`y + x2 = (y + x2) DIV n * n + (y + x2) MOD n
54 /\ y + x1 = (y + x1) DIV n * n + (y + x2) MOD n
55 ==> x1- x2= (y + x1) DIV n *n- (y + x2) DIV n * n `)
56 THEN POP_ASSUM( fun th-> GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
59 THEN POP_ASSUM( fun th-> GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
60 THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
62 THEN MRESA_TAC MOD_MULT[`n:num`;`(y + x1) DIV n - (y + x2) DIV n`]
64 THEN ONCE_REWRITE_TAC[ARITH_RULE`n * ((y + x1) DIV n - (y + x2) DIV n) = ((y + x1) DIV n - (y + x2) DIV n) *n`]
66 THEN MP_TAC(ARITH_RULE`x2<= x1 ==> x1= x2 + (x1- x2):num`)
68 THEN MRESAL_TAC MOD_ADD_MOD[`x2:num`;`x1-x2:num`;`n:num`][ARITH_RULE` A+0=A/\ (A+B)+C=A+B+C`]
70 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SYM th])
71 THEN MRESAL_TAC MOD_MOD_REFL[`x2:num`;`n:num`][ARITH_RULE`3*1=3/\ ~(3=0)`]
76 let MOD_EQ_MOD=prove(`!x1 x2 y n. ~(n=0) /\ (y + x1) MOD n = (y + x2) MOD n
77 ==> x1 MOD n = x2 MOD n`,
79 THEN DISJ_CASES_TAC(ARITH_RULE`x2<= x1 \/ x1<= x2:num`)
80 THENL[MRESA_TAC MOD_EQ_MOD1[`x1:num`;`x2:num`;`y:num`;`n:num`];
81 MRESA_TAC MOD_EQ_MOD1[`x2:num`;`x1:num`;`y:num`;`n:num`]]);;
84 let EAR_STABLE_SYSTEM=prove_by_refinement(`stable_system 3 ((#0.11)) (0..2) (a_ear0 {{1,2}}) (b_ear0 {{1,2}}) ({{1,2}}) (\i. (1 + i) MOD 3)`,
86 MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`2`][ARITH_RULE`(2+1)-0=3`]
87 THEN ASM_SIMP_TAC[stable_system;constraint_system;torsor;ARITH_RULE`3<= 3 /\3<=6/\ 1+3<=6/\ (2+1)-0=3`;CARD_NUMSEG;Hypermap.CARD_SINGLETON;]
95 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
96 THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`2`[ARITH_RULE`SUC 2=3`];
100 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
101 THEN REPEAT STRIP_TAC
102 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`3`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=3<=> A<=2)`]
103 THEN POP_ASSUM MP_TAC
108 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
109 THEN REPEAT STRIP_TAC
110 THEN POP_ASSUM MP_TAC
111 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i /\ 1<3`)
113 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`i:num`]
114 THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2`)
116 THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
117 THEN ASM_REWRITE_TAC[]
121 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
122 THEN REPEAT STRIP_TAC
123 THEN ASSUME_TAC(ARITH_RULE`1<=3 /\1<3/\ 1<=2`)
124 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`3:num`]
125 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`x:num`][ARITH_RULE`1*3=3`]
126 THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
127 THEN ASM_REWRITE_TAC[]
133 REWRITE_TAC[b_ear0;a_ear0]
135 THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =j MOD 3 \/ ~(i MOD 3 =j MOD 3:num)`);
137 ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`];
140 THEN DISJ_CASES_TAC(SET_RULE`{i MOD 3,j MOD 3} IN {{1,2}} \/ ~({i MOD 3,j MOD 3} IN {{1,2}})`);
142 ASM_REWRITE_TAC[IN_SING]
143 THEN ONCE_REWRITE_TAC[SET_RULE`{i MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i MOD 3}= {1,2}`]
144 THEN POP_ASSUM MP_TAC
145 THEN ASM_REWRITE_TAC[IN_SING;cstab]
147 THEN MATCH_MP_TAC REAL_LE_LSQRT
150 ASM_REWRITE_TAC[IN_SING]
151 THEN ONCE_REWRITE_TAC[SET_RULE`{i MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i MOD 3}= {1,2}`]
152 THEN POP_ASSUM MP_TAC
153 THEN ASM_REWRITE_TAC[IN_SING;h0]
160 THEN MP_TAC(ARITH_RULE`1<= 3 /\ 1<3`)
162 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`j:num`][ARITH_RULE`1*3=3`]
163 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`j:num`;`3:num`]
164 THEN SIMP_TAC[b_ear0;a_ear0;ARITH_RULE`A+0=A`;MOD_MOD_REFL;ARITH_RULE`~(3=0)`];
166 REWRITE_TAC[SUBSET;IN_SING;IN_ELIM_THM;IN_NUMSEG]
167 THEN REPEAT STRIP_TAC
169 THEN ASM_REWRITE_TAC[ARITH_RULE`0<=1 /\ 1<=2/\ (1 +1 ) MOD 3= 2`];
171 REWRITE_TAC[a_ear0;IN_NUMSEG]
172 THEN REPEAT STRIP_TAC
173 THEN MP_TAC(ARITH_RULE`i<= 2/\ j<= 2==> i< 3 /\ j< 3`)
175 THEN MRESA_TAC MOD_LT[`i:num`;`3`]
176 THEN MRESA_TAC MOD_LT[`j:num`;`3`]
177 THEN DISJ_CASES_TAC(SET_RULE`{i,j} IN {{1,2}} \/ ~({i,j} IN {{1,2}})`);
179 THEN MATCH_MP_TAC REAL_LE_RSQRT
184 REWRITE_TAC[b_ear0;a_ear0;MOD_MOD_REFL]
185 THEN REPEAT STRIP_TAC
186 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)`);
187 ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`;cstab]
190 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}})`);
193 ASM_REWRITE_TAC[h0;cstab]
195 REWRITE_TAC[IN_SING;a_ear0;b_ear0]
196 THEN REPEAT STRIP_TAC
197 THEN MP_TAC(SET_RULE`{i,j}={1,2} /\ ~(1=2) ==> ~(i=j) /\ (i =1\/ i=2) /\ (j=1\/ j=2)`)
198 THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=2)`]
200 THEN MP_TAC(ARITH_RULE`(i =1\/ i=2) /\ (j=1\/ j=2)==> i< 3 /\ j< 3`)
202 THEN MRESA_TAC MOD_LT[`i:num`;`3`]
203 THEN MRESA_TAC MOD_LT[`j:num`;`3`]]);;
215 let exist_stable_system=prove_by_refinement(`?s:(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num)). stable_system (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))))))
216 (SND(SND (SND (SND (SND (SND s))))))`,
217 [EXISTS_TAC`3, (#0.11), (0..2), (a_ear0 {{1,2}}), (b_ear0 {{1,2}}), ({{1,2}}),(\i. (1 + i) MOD 3)`
218 THEN REWRITE_TAC[EAR_STABLE_SYSTEM]]);;
221 let stable_sy_tybij = (new_type_definition "stable_sy" ("stable_sy", "tuple_stable_sy")exist_stable_system);;
224 let k_sy = new_definition `k_sy (s:stable_sy) = FST (tuple_stable_sy s)`;;
226 let d_sy = new_definition `d_sy (s:stable_sy) = (FST (SND (tuple_stable_sy s)))`;;
228 let I_SY = new_definition `I_SY (s:stable_sy) = (FST (SND (SND (tuple_stable_sy s))))`;;
230 let a_sy = new_definition `a_sy (s:stable_sy) = (FST (SND (SND (SND (tuple_stable_sy s)))))`;;
232 let b_sy = new_definition `b_sy (s:stable_sy) = (FST(SND (SND (SND (SND (tuple_stable_sy s)))))) `;;
235 let J_SY = new_definition `J_SY (s:stable_sy) = (FST (SND (SND (SND (SND (SND (tuple_stable_sy s))))))) `;;
237 let f_sy = new_definition `f_sy (s:stable_sy) = (SND(SND (SND (SND (SND (SND (tuple_stable_sy s)))))))`;;
241 let stable_sy_lemma=prove(`!s:stable_sy. stable_system (k_sy s) (d_sy s) (I_SY s) (a_sy s) (b_sy s) (J_SY s) (f_sy s)`,
242 ASM_REWRITE_TAC[stable_sy_tybij;k_sy;d_sy;I_SY; a_sy; b_sy; J_SY; f_sy]);;
245 let ear_sy=new_definition `ear_sy (s:stable_sy)<=> CARD(I_SY s)=3 /\ d_sy s= #0.11 /\ CARD (J_SY s)= 1 /\ a_sy (s)= a_ear0 (J_SY s)
246 /\ b_sy (s)= b_ear0 (J_SY s) `;;
249 let sigma_sy=new_definition `sigma_sy (s:stable_sy) = (if ear_sy s then &1 else -- &1) `;;
251 let J1_SY=new_definition `J1_SY (s:stable_sy)= {x| ?i. {i MOD (k_sy s),f_sy s (i MOD (k_sy s))} IN J_SY s /\ i IN 1..(k_sy s) /\ x=i,SUC(i MOD (k_sy s))}`;;
253 let d_fun=new_definition `d_fun (s:stable_sy,l:real^(M,3)finite_product) = (d_sy s) + #0.1 * sigma_sy s * sum (J1_SY s) (\x. cstab -norm (row (FST x) (vecmats l) - row (SND x) (vecmats l) ))`;;
255 let tau_star=new_definition `tau_star (s:stable_sy) (l:real^(M,3)finite_product)= tau_fun (V_SY (vecmats l)) (E_SY (vecmats l)) (F_SY (vecmats l)) - d_fun (s,l)`;;
258 let FINITE_J_SY=prove(`!s:stable_sy .
261 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
262 THEN REMOVE_ASSUM_TAC
263 THEN REMOVE_ASSUM_TAC
264 THEN REMOVE_ASSUM_TAC
265 THEN POP_ASSUM MP_TAC
266 THEN REWRITE_TAC[constraint_system;torsor;HAS_SIZE]
268 THEN REMOVE_ASSUM_TAC
269 THEN MRESA_TAC FINITE_SUBSET[`J_SY (s:stable_sy)`;`{{i, f_sy s i} | i | i IN I_SY (s:stable_sy)}`]
270 THEN POP_ASSUM MATCH_MP_TAC
271 THEN MRESAL_TAC FINITE_IMAGE[`(\i. {i, f_sy (s:stable_sy) i})`;`I_SY (s:stable_sy)`][FINITE_NUMSEG;IMAGE]
272 THEN SUBGOAL_THEN`{y | ?x. x IN I_SY s /\ y = {x,f_sy s x}}={{i, f_sy s i} | i | i IN I_SY (s:stable_sy)}`ASSUME_TAC
273 THENL[REWRITE_TAC[EXTENSION;IN_ELIM_THM];
274 POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])]);;
277 let FINITE_J1_SY=prove(`!s:stable_sy .
280 THEN REWRITE_TAC[J1_SY]
281 THEN MRESAL_TAC FINITE_IMAGE[`(\i. i, SUC(i MOD (k_sy s)))`;`1..k_sy (s:stable_sy)`][FINITE_NUMSEG;IMAGE]
282 THEN MATCH_MP_TAC FINITE_SUBSET
283 THEN EXISTS_TAC`{y | ?x. x IN 1..(k_sy (s:stable_sy)) /\ y = x,SUC(x MOD (k_sy s))}`
284 THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]
286 THEN EXISTS_TAC`i:num`
287 THEN ASM_REWRITE_TAC[]);;
289 let CONTINUOUS_ON_ROW=prove(`!i s:real^(M,N)finite_product->bool. 1<= i/\ i<= dimindex(:M) ==> (\x. row i (vecmats x)) continuous_on s`,
290 REWRITE_TAC[continuous_on;]
291 THEN REPEAT STRIP_TAC
292 THEN EXISTS_TAC`e:real`
294 THEN POP_ASSUM MP_TAC
295 THEN MP_TAC(ARITH_RULE`1<= i/\ i<= dimindex(:M) ==> i-1< dimindex(:M)`)
297 THEN MRESAL_TAC (GEN_ALL VECMAT_ROW)[`i-1:num`;`vecmats(x':real^(M,N)finite_product)`][MATVEC_VECMATS_ID]
298 THEN MRESAL_TAC (GEN_ALL VECMAT_ROW)[`i-1:num`;`vecmats(x:real^(M,N)finite_product)`][MATVEC_VECMATS_ID]
299 THEN MRESA_TAC (GEN_ALL DIST_VECMAT)[`i-1:num`;`x':real^(M,N)finite_product`;`x:real^(M,N)finite_product`]
300 THEN MP_TAC(ARITH_RULE`1<= i/\ i<= dimindex(:M) ==> i= SUC(i-1)`)
301 THEN ASM_REWRITE_TAC[]
303 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
304 THEN POP_ASSUM MP_TAC
305 THEN REAL_ARITH_TAC);;
308 let INDEX_J1_SY=prove(`!s:stable_sy .
309 x IN J1_SY s ==> 1 <= FST x /\ FST x <= k_sy s`,
310 REWRITE_TAC[J1_SY;IN_ELIM_THM;IN_NUMSEG]
311 THEN REPEAT STRIP_TAC
312 THEN ASM_REWRITE_TAC[]);;
316 let CONTINUOUS_ON_D_FUN=prove(`!s:stable_sy .
317 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k))
318 ==> lift o(\l:real^(M,3)finite_product. d_fun(s,l)) continuous_on (B_SY1 (a_sy s) (b_sy s))`,
320 THEN REWRITE_TAC[d_fun;LIFT_ADD;o_DEF;]
321 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
322 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
323 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
324 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
325 THEN ASSUME_TAC FINITE_J1_SY
326 THEN POP_ASSUM(fun th -> MRESA1_TAC th`s:stable_sy`)
327 THEN ASM_SIMP_TAC[LIFT_SUM;o_DEF]
328 THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM
329 THEN ASM_REWRITE_TAC[]
330 THEN REPEAT STRIP_TAC
331 THEN REWRITE_TAC[LIFT_SUB]
332 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
333 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
334 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
335 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
338 MATCH_MP_TAC CONTINUOUS_ON_ROW
339 THEN POP_ASSUM MP_TAC
340 THEN REWRITE_TAC[J1_SY;IN_ELIM_THM;IN_NUMSEG]
341 THEN REPEAT RESA_TAC;
342 MATCH_MP_TAC CONTINUOUS_ON_ROW
343 THEN POP_ASSUM MP_TAC
344 THEN REWRITE_TAC[J1_SY;IN_ELIM_THM;IN_NUMSEG]
346 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
347 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
348 THEN POP_ASSUM MP_TAC
351 let INJ_B_SY=prove(`!s:stable_sy x:real^(M,3)finite_product. x IN (B_SY1 (a_sy s) (b_sy s)) /\ k_sy s =k /\ dimindex(:M) =k /\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
356 row i (vecmats x),row (SUC (i MOD k)) (vecmats x) =
357 row j (vecmats x),row (SUC (j MOD k)) (vecmats x)
359 REWRITE_TAC[PAIR_EQ;IN_NUMSEG]
360 THEN REPEAT STRIP_TAC
361 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`
362 THEN MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d_sy (s:stable_sy)`;`J_SY (s:stable_sy)`;`k_sy (s:stable_sy)`;`i:num`;`j:num`;`a_sy (s:stable_sy)`;`b_sy (s:stable_sy)`;`row i (vecmats (x:real^(M,3)finite_product))`;`row j (vecmats (x:real^(M,3)finite_product))`;`x:real^(M,3)finite_product`]
363 THEN POP_ASSUM MP_TAC
364 THEN DISJ_CASES_TAC(SET_RULE`~(i=j) \/ i=j:num`)
365 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
366 THEN REAL_ARITH_TAC);;
368 let INJ_ROW_B_SY=prove(`!s:stable_sy x:real^(M,3)finite_product. x IN (B_SY1 (a_sy s) (b_sy s)) /\ k_sy s =k /\ dimindex(:M) =k /\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
376 REWRITE_TAC[PAIR_EQ;IN_NUMSEG]
377 THEN REPEAT STRIP_TAC
378 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`
379 THEN MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d_sy (s:stable_sy)`;`J_SY (s:stable_sy)`;`k_sy (s:stable_sy)`;`i:num`;`j:num`;`a_sy (s:stable_sy)`;`b_sy (s:stable_sy)`;`row i (vecmats (x:real^(M,3)finite_product))`;`row j (vecmats (x:real^(M,3)finite_product))`;`x:real^(M,3)finite_product`]
380 THEN POP_ASSUM MP_TAC
381 THEN DISJ_CASES_TAC(SET_RULE`~(i=j) \/ i=j:num`)
382 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
383 THEN REAL_ARITH_TAC);;
387 let CHANGE_SUM_TAU_FUN=prove(`!s:stable_sy x:real^(M,3)finite_product. k_sy s =k /\ dimindex(:M) =k /\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
389 x IN (B_SY1 (a_sy s) (b_sy s))
392 sum (F_SY (vecmats x))
393 (\e. rho_fun (norm (FST e)) * azim_in_fan e (E_SY (vecmats x)))) x
394 = (\x. sum (1..k_sy s)
395 (\i. rho_fun (norm (row i (vecmats x))) * azim_in_fan (row i (vecmats x), row (SUC (i MOD (k_sy s))) (vecmats x)) (E_SY (vecmats x)))) x`,
397 THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM]
401 THEN SUBGOAL_THEN`{y | ?x1. x1 IN 1..dimindex (:M) /\
404 row (SUC (x1 MOD dimindex (:M))) (vecmats x)}
405 ={row i (vecmats x),row (SUC (i MOD dimindex (:M))) (vecmats (x:real^(M,3)finite_product)) | 1 <= i /\
410 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
412 THEN ASM_REWRITE_TAC[GSYM F_SY]
414 THEN MRESAL_TAC SUM_IMAGE[`(\i. (row i (vecmats x), row (SUC (i MOD (k_sy s))) (vecmats (x:real^(M,3)finite_product))))`;`(\e. rho_fun (norm (FST e)) * azim_in_fan e (E_SY (vecmats (x:real^(M,3)finite_product))))`;`1..(k_sy (s:stable_sy))`][o_DEF;IMAGE]
415 THEN POP_ASSUM MATCH_MP_TAC
416 THEN MATCH_MP_TAC INJ_B_SY
417 THEN EXISTS_TAC`s:stable_sy`
418 THEN ASM_REWRITE_TAC[]]);;
422 let CONTINUOUS_ON_SAME_DOMAIN=prove(`!f g s:real^M->bool. (!x. x IN s==> f x= g x) /\ f continuous_on s ==> g continuous_on s`,
423 SIMP_TAC[continuous_on]
424 THEN REPEAT STRIP_TAC
425 THEN POP_ASSUM MP_TAC
426 THEN POP_ASSUM MP_TAC
427 THEN POP_ASSUM MP_TAC
428 THEN POP_ASSUM MP_TAC
429 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
430 THEN DISCH_THEN(LABEL_TAC"THY")
431 THEN REPEAT STRIP_TAC
432 THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th`x:real^M`)
433 THEN POP_ASSUM(fun th-> MRESA1_TAC th`e:real`)
434 THEN POP_ASSUM MP_TAC
435 THEN DISCH_THEN(LABEL_TAC"THY")
436 THEN EXISTS_TAC`d:real`
437 THEN ASM_REWRITE_TAC[]
438 THEN REPEAT STRIP_TAC
439 THEN REMOVE_THEN"THYGIANG"(fun th-> MRESA1_TAC th`x':real^M` THEN MRESA1_TAC th`x:real^M`)
440 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`x':real^M`));;
443 let EDGE_IN_F_SY=prove(`!(l:real^(M,3)finite_product). 1<= i /\ i<= dimindex (:M)
444 /\ u = row i (vecmats l)
445 /\ v= row (SUC (i MOD dimindex (:M))) (vecmats l)
446 ==> u,v IN F_SY (vecmats l)`,
448 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
449 THEN EXISTS_TAC`i:num`
450 THEN ASM_REWRITE_TAC[]);;
454 let JBDNJJB3=prove(`!u:real^3 v:real^3 w:real^3.
455 ~collinear {vec 0, u, v} /\ ~collinear {vec 0, u, w}
457 sin(azim (vec 0) u v w)=inv (sqrt(norm w pow 2 - (inv (norm u) * (u dot w)) pow 2) * norm (u cross v)) *(u cross v) dot w`,
459 THEN MRESA_TAC th3[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
460 THEN MRESA_TAC properties_coordinate[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
461 THEN MRESA_TAC azim[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`(w:real^3)`]
462 THEN POP_ASSUM (fun th->MRESA_TAC th [`e1_fan ((vec 0):real^3) (u:real^3) (v:real^3)`;`e2_fan ((vec 0):real^3) (u:real^3) (v:real^3)`;`e3_fan ((vec 0):real^3) (u:real^3) (v:real^3)`])
463 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
464 THEN DISCH_THEN (LABEL_TAC"YEU EM")
465 THEN DISCH_TAC THEN DISCH_TAC
466 THEN SUBGOAL_THEN`sqrt(norm w pow 2 - (inv (norm u) * (u dot (w:real^3))) pow 2) =r2`ASSUME_TAC
468 MRESA1_TAC NORM_POW_2`w:real^3`
469 THEN POP_ASSUM MP_TAC
470 THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`a=a- vec 0`]
471 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
472 THEN ONCE_REWRITE_TAC[DOT_SYM]
473 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
474 THEN FIND_ASSUM MP_TAC`orthonormal (e1_fan (vec 0) u v) (e2_fan (vec 0) u v)
475 (e3_fan (vec 0) u (v:real^3))`
476 THEN REWRITE_TAC[orthonormal;]
478 THEN ONCE_REWRITE_TAC[DOT_SYM]
479 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &0= &0 /\ A+ &0=A/\ &0 +A=A
480 /\ (r2 * cos (psi + azim (vec 0) u v w)) *
481 (r2 * cos (psi + azim (vec 0) u v w)) *
483 (r2 * sin (psi + azim (vec 0) u v w)) *
484 (r2 * sin (psi + azim (vec 0) u v w)) *
486 h2 * h2 * ((u - vec 0) dot (u - vec 0))
487 = (r2 pow 2) * ( (sin (psi + azim (vec 0) u v w)) pow 2 +(cos (psi + azim (vec 0) u v w)) pow 2 ) +
488 h2 * h2 * ((u - vec 0) dot (u - vec 0))`;Trigonometry.WPMXVYZ]
489 THEN MP_TAC(VECTOR_ARITH`w dot u= (w- vec 0) dot (u- vec 0:real^3)`)
490 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
491 THEN ONCE_REWRITE_TAC[DOT_SYM]
492 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
494 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN MP_TAC(SYM th) THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;GSYM NORM_POW_2])
495 THEN ONCE_REWRITE_TAC[REAL_ARITH`A *B= B*A`]
496 THEN MP_TAC(ISPECL[`u:real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
497 THEN REDUCE_VECTOR_TAC
499 THEN MP_TAC(ISPEC`(norm(u:real^3))`REAL_MUL_LINV)
502 THEN MP_TAC(SET_RULE`norm u pow 2 * h2 = u dot w
503 ==> inv (norm u) * inv (norm u) *(norm u pow 2 * h2) = inv (norm u) *inv (norm u) *(u dot (w:real^3))`)
504 THEN POP_ASSUM( fun th -> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
505 THEN ASM_REWRITE_TAC[REAL_ARITH` inv (norm u) * inv (norm u) * norm u pow 2 * h2 =(inv (norm u) * norm u) pow 2 * h2/\ &1 pow 2 * h2= h2/\ &1 *A=A`]
507 THEN REWRITE_TAC[REAL_ARITH`
508 (u dot w) * inv (norm u) * inv (norm u) * (u dot w) = (inv (norm u) * (u dot w)) pow 2`]
509 THEN ONCE_REWRITE_TAC[REAL_ARITH`
510 norm w pow 2 = r2 pow 2 + (inv (norm u) * (u dot w)) pow 2
511 <=> norm w pow 2 - (inv (norm u) * (u dot w)) pow 2= r2 pow 2 `]
513 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
514 THEN ONCE_REWRITE_TAC[DOT_SYM]
515 THEN ASM_REWRITE_TAC[]
516 THEN MATCH_MP_TAC POW_2_SQRT
517 THEN MATCH_MP_TAC(REAL_ARITH`&0< A==> &0<= A`)
518 THEN ASM_REWRITE_TAC[];
519 MRESA_TAC sincos1_of_u_fan[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`r1:real`; `psi:real`; `h1:real`]
520 THEN REMOVE_THEN "YEU EM" MP_TAC
521 THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;]
522 THEN REDUCE_ARITH_TAC
523 THEN REDUCE_VECTOR_TAC
525 THEN MP_TAC(SET_RULE`w =
526 (r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
527 (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
530 (u cross v) dot ((r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
531 (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
533 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
534 THEN REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF; e2_fan;e1_fan;e3_fan;
535 VECTOR_ARITH`A- vec 0= A`;CROSS_LADD; CROSS_RADD; CROSS_LMUL; CROSS_RMUL;CROSS_REFL;CROSS_RNEG;CROSS_LNEG;]
536 THEN REDUCE_ARITH_TAC
537 THEN REWRITE_TAC[NORM_MUL;REAL_INV_MUL;REAL_ABS_INV;REAL_INV_INV;REAL_ABS_NORM;DOT_SQUARE_NORM
538 ;REAL_ARITH`(r2 * sin (azim (vec 0) u v w)) *
539 (norm u * inv (norm (u cross v))) *
541 norm (u cross v) pow 2 =(r2* norm(u cross v)) * sin (azim (vec 0) u v w) *
542 ( inv (norm u) * norm u)*
543 ( inv (norm (u cross v))* norm (u cross (v:real^3)))`
545 THEN MP_TAC(ISPECL[`u:real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
546 THEN REDUCE_VECTOR_TAC
548 THEN MP_TAC(ISPEC`(norm(u:real^3))`REAL_MUL_LINV)
550 THEN ASSUME_TAC(ISPEC`u:real^3`NORM_POS_LE)
551 THEN MP_TAC(REAL_ARITH`~(&0 =norm(u:real^3)) /\ &0 <= norm(u:real^3)==> &0 <norm(u:real^3)`)
553 THEN SUBGOAL_THEN`~(u cross v = vec 0)` ASSUME_TAC
554 THENL[ASM_REWRITE_TAC[CROSS_EQ_0];
555 MP_TAC(ISPECL[`u cross v :real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
556 THEN REDUCE_VECTOR_TAC
558 THEN MP_TAC(ISPEC`(norm(u cross v:real^3))`REAL_MUL_LINV)
560 THEN ASSUME_TAC(ISPEC`u cross v:real^3`NORM_POS_LE)
561 THEN MP_TAC(REAL_ARITH`~(&0 =norm(u cross v:real^3)) /\ &0 <= norm(u cross v:real^3)==> &0 <norm(u cross v:real^3)`)
563 THEN MRESA_TAC REAL_LT_MUL[`r2:real`;`norm(u cross v:real^3)`]
564 THEN MP_TAC(REAL_ARITH`&0<(r2:real)*norm(u cross v:real^3)==> ~((r2:real)*norm(u cross v:real^3)= &0)`)
565 THEN REDUCE_VECTOR_TAC
567 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_MUL_LINV)
569 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_LT_INV)
571 THEN REDUCE_ARITH_TAC
573 THEN MP_TAC(SET_RULE`(u cross v) dot w = (r2 * norm (u cross v)) * sin (azim (vec 0) u v w) ==>
574 inv (r2 * norm (u cross v))*(r2 * norm (u cross v)) * sin (azim (vec 0) u v w)= inv (r2 * norm (u cross v)) *((u cross v) dot w)`)
575 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
576 THEN ASM_REWRITE_TAC[REAL_ARITH`inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)) *
577 sin (azim (vec 0) u v w)=(inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)))*
578 sin (azim (vec 0) u v w)`]
579 THEN REDUCE_ARITH_TAC
581 THEN ASM_REWRITE_TAC[GSYM REAL_INV_MUL]]]);;
586 let CONTINUOUS_AT_SQRT = prove
587 (`!a. &0 < drop a ==> (lift o sqrt o drop) continuous (at a)`,
588 REPEAT STRIP_TAC THEN REWRITE_TAC[continuous_at; o_THM; DIST_LIFT] THEN
589 X_GEN_TAC `e:real` THEN DISCH_TAC THEN
590 EXISTS_TAC `min (drop a) (e * sqrt(drop a))` THEN
591 ASM_SIMP_TAC[REAL_LT_MIN; SQRT_POS_LT; REAL_LT_MUL; DIST_REAL] THEN
592 X_GEN_TAC `b:real^1` THEN REWRITE_TAC[GSYM drop] THEN STRIP_TAC THEN
593 FIRST_ASSUM(ASSUME_TAC o MATCH_MP (REAL_ARITH
594 `abs(b - a) < a ==> &0 < b`)) THEN
596 `sqrt(drop b) - sqrt(drop a) =
597 (drop b - drop a) / (sqrt(drop a) + sqrt(drop b))`
599 [MATCH_MP_TAC(REAL_FIELD
600 `sa pow 2 = a /\ sb pow 2 = b /\ &0 < sa /\ &0 < sb
601 ==> sb - sa = (b - a) / (sa + sb)`) THEN
602 ASM_SIMP_TAC[SQRT_POS_LT; SQRT_POW_2; REAL_LT_IMP_LE];
603 ASM_SIMP_TAC[REAL_ABS_DIV; SQRT_POS_LT; REAL_LT_ADD; REAL_LT_LDIV_EQ;
604 REAL_ARITH `&0 < x ==> abs x = x`] THEN
605 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
606 REAL_LTE_TRANS)) THEN
607 ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_LE_ADDR; SQRT_POS_LE;
611 let SEQUENTIALLY_DIVH=prove_by_refinement(`!f:num->real^3 g:num->real^3 h:num->real^3.((\n:num. f n) --> a) sequentially /\ ((\n:num. g n) --> b) sequentially /\ ((\n:num. h n) --> c) sequentially /\ ~(collinear {vec 0, a,b:real^3}) /\ ~(collinear {vec 0, a,c}) /\ (!n. ~(collinear {vec 0, f n, g n}) /\ ~(collinear {vec 0, f n, h n}))
612 ==> ((lift o (\n:num. dihV (vec 0) (f(n)) (g(n)) (h n)))--> lift ( dihV (vec 0) a b c)) sequentially`,
614 THEN MRESA_TAC Trigonometry2.FOR_LEMMA19[`vec 0:real^3`;`a:real^3`; `b:real^3`;`c:real^3`]
615 THEN POP_ASSUM MP_TAC
618 THEN ABBREV_TAC`v01n= (\n:num. dist (vec 0:real^3, f n) pow 2)`
619 THEN ABBREV_TAC`v02n= (\n:num. dist (vec 0:real^3, g n) pow 2)`
620 THEN ABBREV_TAC`v03n= (\n:num. dist (vec 0:real^3, h n) pow 2)`
621 THEN ABBREV_TAC`v12n= (\n:num. dist (f n, (g n):real^3) pow 2)`
622 THEN ABBREV_TAC`v13n= (\n:num. dist (f n, (h n):real^3) pow 2)`
623 THEN ABBREV_TAC`v23n= (\n:num. dist (g n, (h n):real^3) pow 2)`
624 THEN SUBGOAL_THEN`(\n. dihV (vec 0) ((f:num->real^3) n) (g n) (h n))
626 (delta_x4 (v01n n) (v02n n) (v03n n) (v23n n) (v13n n) (v12n n) /
627 sqrt (ups_x (v01n n) (v02n n) (v12n n) * ups_x (v01n n) (v03n n) (v13n n)
631 REWRITE_TAC[FUN_EQ_THM]
633 THEN MRESA_TAC Trigonometry2.FOR_LEMMA19[`vec 0:real^3`;`(f (x:num)):real^3`; `(g (x:num)):real^3`;`(h (x:num)):real^3`]
634 THEN POP_ASSUM MP_TAC
637 THEN EXPAND_TAC"v01n"
638 THEN EXPAND_TAC"v02n"
639 THEN EXPAND_TAC"v03n"
640 THEN EXPAND_TAC"v12n"
641 THEN EXPAND_TAC"v23n"
642 THEN EXPAND_TAC"v13n"
644 THEN ASM_REWRITE_TAC[];
646 THEN MRESAL1_TAC REAL_CONTINUOUS_WITHIN_ACS_STRONG`delta_x4 v01 v02 v03 v23 v13 v12 /
647 sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13)`[REAL_CONTINUOUS_CONTINUOUS_WITHINREAL;CONTINUOUS_WITHIN_SEQUENTIALLY]
648 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`lift o(\n:num.
649 (delta_x4 (v01n n) (v02n n) (v03n n) (v23n n) (v13n n) (v12n n) /
651 (ups_x (v01n n) (v02n n) (v12n n) * ups_x (v01n n) (v03n n) (v13n n))))`[o_DEF;LIFT_DROP])
652 THEN POP_ASSUM MATCH_MP_TAC
654 REWRITE_TAC[ IN_ELIM_THM;IMAGE]
656 THEN EXISTS_TAC`delta_x4 (v01n n) (v02n n) (v03n n) (v23n n) (v13n n) (v12n n) /
658 (ups_x (v01n n) (v02n n) (v12n n) * ups_x (v01n n) (v03n n) (v13n (n:num)))`
659 THEN ASM_REWRITE_TAC[]
660 THEN MRESA_TAC (GEN_ALL Trigonometry2.PROVE_DELTA_OVER_SQRT_2UPS)[`(f (n:num)):real^3`;`(h (n:num)):real^3`;`(g (n:num)):real^3`;`vec 0:real^3`;`(v23n (n:num)):real`;`(v02n (n:num)):real` ;`(v12n (n:num)):real`;`(v01n (n:num)):real`;`(v03n (n:num)):real`;`(v13n (n:num)):real`]
661 THEN POP_ASSUM MP_TAC
662 THEN EXPAND_TAC"v01n"
663 THEN EXPAND_TAC"v02n"
664 THEN EXPAND_TAC"v03n"
665 THEN EXPAND_TAC"v12n"
666 THEN EXPAND_TAC"v23n"
667 THEN EXPAND_TAC"v13n"
671 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; NORM_CAUCHY_SCHWARZ_DIV]);
672 REWRITE_TAC[real_div;LIFT_CMUL]
673 THEN MATCH_MP_TAC LIM_MUL
675 REWRITE_TAC[o_DEF;delta_x4;LIFT_SUB;LIFT_ADD;LIFT_CMUL]
676 THEN MATCH_MP_TAC LIM_ADD
681 THEN REWRITE_TAC[o_DEF]
682 THEN EXPAND_TAC"v01n"
683 THEN EXPAND_TAC"v02n"
684 THEN EXPAND_TAC"v03n"
685 THEN EXPAND_TAC"v12n"
686 THEN EXPAND_TAC"v23n"
687 THEN EXPAND_TAC"v13n"
694 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
697 THEN MATCH_MP_TAC LIM_MUL
698 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
699 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
700 THEN POP_ASSUM MP_TAC
701 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
703 THEN POP_ASSUM MATCH_MP_TAC
704 THEN ASM_REWRITE_TAC[]
706 THEN REWRITE_TAC[ETA_AX]
709 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
710 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
711 THEN POP_ASSUM MP_TAC
712 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
714 THEN POP_ASSUM MATCH_MP_TAC
715 THEN ASM_REWRITE_TAC[]
717 THEN REWRITE_TAC[ETA_AX]
720 THEN REWRITE_TAC[o_DEF]
721 THEN EXPAND_TAC"v01n"
722 THEN EXPAND_TAC"v02n"
723 THEN EXPAND_TAC"v03n"
724 THEN EXPAND_TAC"v12n"
725 THEN EXPAND_TAC"v23n"
726 THEN EXPAND_TAC"v13n"
733 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
736 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
737 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
738 THEN POP_ASSUM MP_TAC
739 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
741 THEN POP_ASSUM MATCH_MP_TAC
742 THEN ASM_REWRITE_TAC[]
744 THEN REWRITE_TAC[ETA_AX]
747 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
748 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b-c:real^3`
749 THEN POP_ASSUM MP_TAC
750 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
752 THEN POP_ASSUM MATCH_MP_TAC
753 THEN ASM_REWRITE_TAC[]
754 THEN MATCH_MP_TAC LIM_SUB
756 THEN REWRITE_TAC[ETA_AX]
761 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
762 THEN EXPAND_TAC"v01n"
763 THEN EXPAND_TAC"v02n"
764 THEN EXPAND_TAC"v03n"
765 THEN EXPAND_TAC"v12n"
766 THEN EXPAND_TAC"v23n"
767 THEN EXPAND_TAC"v13n"
774 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
777 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
778 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
779 THEN POP_ASSUM MP_TAC
780 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
782 THEN POP_ASSUM MATCH_MP_TAC
783 THEN ASM_REWRITE_TAC[]
785 THEN REWRITE_TAC[ETA_AX]
788 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
789 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
790 THEN POP_ASSUM MP_TAC
791 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
793 THEN POP_ASSUM MATCH_MP_TAC
794 THEN ASM_REWRITE_TAC[]
795 THEN MATCH_MP_TAC LIM_SUB
797 THEN REWRITE_TAC[ETA_AX]
804 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
805 THEN EXPAND_TAC"v01n"
806 THEN EXPAND_TAC"v02n"
807 THEN EXPAND_TAC"v03n"
808 THEN EXPAND_TAC"v12n"
809 THEN EXPAND_TAC"v23n"
810 THEN EXPAND_TAC"v13n"
817 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
820 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
821 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
822 THEN POP_ASSUM MP_TAC
823 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
825 THEN POP_ASSUM MATCH_MP_TAC
826 THEN ASM_REWRITE_TAC[]
828 THEN REWRITE_TAC[ETA_AX]
831 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
832 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
833 THEN POP_ASSUM MP_TAC
834 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
836 THEN POP_ASSUM MATCH_MP_TAC
837 THEN ASM_REWRITE_TAC[]
838 THEN MATCH_MP_TAC LIM_SUB
840 THEN REWRITE_TAC[ETA_AX]
843 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
844 THEN EXPAND_TAC"v01n"
845 THEN EXPAND_TAC"v02n"
846 THEN EXPAND_TAC"v03n"
847 THEN EXPAND_TAC"v12n"
848 THEN EXPAND_TAC"v23n"
849 THEN EXPAND_TAC"v13n"
856 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
859 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
860 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
861 THEN POP_ASSUM MP_TAC
862 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
864 THEN POP_ASSUM MATCH_MP_TAC
865 THEN ASM_REWRITE_TAC[]
866 THEN MATCH_MP_TAC LIM_SUB
868 THEN REWRITE_TAC[ETA_AX]
871 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
872 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
873 THEN POP_ASSUM MP_TAC
874 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
876 THEN POP_ASSUM MATCH_MP_TAC
877 THEN ASM_REWRITE_TAC[]
878 THEN MATCH_MP_TAC LIM_SUB
880 THEN REWRITE_TAC[ETA_AX]
883 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
884 THEN EXPAND_TAC"v01n"
885 THEN EXPAND_TAC"v02n"
886 THEN EXPAND_TAC"v03n"
887 THEN EXPAND_TAC"v12n"
888 THEN EXPAND_TAC"v23n"
889 THEN EXPAND_TAC"v13n"
896 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
899 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
900 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
901 THEN POP_ASSUM MP_TAC
902 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
904 THEN POP_ASSUM MATCH_MP_TAC
905 THEN ASM_REWRITE_TAC[]
907 THEN REWRITE_TAC[ETA_AX]
912 THEN MATCH_MP_TAC LIM_MUL
913 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
914 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
915 THEN POP_ASSUM MP_TAC
916 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
918 THEN POP_ASSUM MATCH_MP_TAC
919 THEN ASM_REWRITE_TAC[]
921 THEN REWRITE_TAC[ETA_AX]
926 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
927 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
928 THEN POP_ASSUM MP_TAC
929 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
931 THEN POP_ASSUM MATCH_MP_TAC
932 THEN ASM_REWRITE_TAC[]
934 THEN REWRITE_TAC[ETA_AX]
941 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
942 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
943 THEN POP_ASSUM MP_TAC
944 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
946 THEN POP_ASSUM MATCH_MP_TAC
947 THEN ASM_REWRITE_TAC[]
949 THEN REWRITE_TAC[ETA_AX]
952 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
953 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b-c:real^3`
954 THEN POP_ASSUM MP_TAC
955 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
957 THEN POP_ASSUM MATCH_MP_TAC
958 THEN ASM_REWRITE_TAC[]
959 THEN MATCH_MP_TAC LIM_SUB
961 THEN REWRITE_TAC[ETA_AX]
966 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
967 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
968 THEN POP_ASSUM MP_TAC
969 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
971 THEN POP_ASSUM MATCH_MP_TAC
972 THEN ASM_REWRITE_TAC[]
973 THEN MATCH_MP_TAC LIM_SUB
975 THEN REWRITE_TAC[ETA_AX]
978 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
979 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
980 THEN POP_ASSUM MP_TAC
981 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
983 THEN POP_ASSUM MATCH_MP_TAC
984 THEN ASM_REWRITE_TAC[]
985 THEN MATCH_MP_TAC LIM_SUB
987 THEN REWRITE_TAC[ETA_AX]
989 MRESAL_TAC LIM_INV [`sequentially`;`(\x:num.
991 (ups_x (v01n x) (v02n x) (v12n x) * ups_x (v01n x) (v03n x) (v13n x))))`;`sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13)`][o_DEF]
992 THEN POP_ASSUM MATCH_MP_TAC
993 THEN SUBGOAL_THEN `&0< ups_x v01 v02 v12 * ups_x v01 v03 v13` ASSUME_TAC;
994 MATCH_MP_TAC REAL_LT_MUL
995 THEN MRESA_TAC (GEN_ALL Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT)[`b:real^3`;`vec 0 :real^3`;`a:real^3`]
996 THEN POP_ASSUM MP_TAC
998 THEN MRESA_TAC (GEN_ALL Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT)[`c:real^3`;`vec 0 :real^3`;`a:real^3`]
999 THEN POP_ASSUM MP_TAC
1001 THEN REAL_ARITH_TAC;
1002 MRESA1_TAC SQRT_POS_LT`ups_x v01 v02 v12 * ups_x v01 v03 v13`
1003 THEN MP_TAC(REAL_ARITH`
1004 &0< sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13)
1005 ==> ~(sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13) = &0)`)
1007 THEN MRESAL1_TAC CONTINUOUS_AT_SQRT`lift(ups_x v01 v02 v12 * ups_x v01 v03 (v13:real))`[CONTINUOUS_AT_SEQUENTIALLY;o_DEF;LIFT_DROP]
1008 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`(\x:num. lift
1009 ( (ups_x (v01n x) (v02n x) (v12n x) * ups_x (v01n x) (v03n x) (v13n x))))`[LIFT_DROP])
1010 THEN POP_ASSUM MATCH_MP_TAC
1011 THEN REWRITE_TAC[LIFT_CMUL]
1012 THEN MATCH_MP_TAC LIM_MUL
1013 THEN REWRITE_TAC[ups_x;o_DEF;LIFT_ADD;LIFT_SUB;LIFT_CMUL]
1015 MATCH_MP_TAC LIM_ADD
1017 MATCH_MP_TAC LIM_SUB
1019 MATCH_MP_TAC LIM_SUB
1021 MATCH_MP_TAC LIM_MUL
1022 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1023 THEN EXPAND_TAC"v01n"
1024 THEN EXPAND_TAC"v02n"
1025 THEN EXPAND_TAC"v03n"
1026 THEN EXPAND_TAC"v12n"
1027 THEN EXPAND_TAC"v23n"
1028 THEN EXPAND_TAC"v13n"
1029 THEN EXPAND_TAC"v01"
1030 THEN EXPAND_TAC"v02"
1031 THEN EXPAND_TAC"v03"
1032 THEN EXPAND_TAC"v12"
1033 THEN EXPAND_TAC"v23"
1034 THEN EXPAND_TAC"v13"
1035 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1037 MATCH_MP_TAC LIM_NEG
1038 THEN MATCH_MP_TAC LIM_MUL
1039 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1040 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1041 THEN POP_ASSUM MP_TAC
1042 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1044 THEN POP_ASSUM MATCH_MP_TAC
1045 THEN ASM_REWRITE_TAC[]
1047 THEN REWRITE_TAC[ETA_AX]
1049 MATCH_MP_TAC LIM_MUL
1050 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1051 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1052 THEN POP_ASSUM MP_TAC
1053 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1055 THEN POP_ASSUM MATCH_MP_TAC
1056 THEN ASM_REWRITE_TAC[]
1058 THEN REWRITE_TAC[ETA_AX]
1060 MATCH_MP_TAC LIM_MUL
1061 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1062 THEN EXPAND_TAC"v01n"
1063 THEN EXPAND_TAC"v02n"
1064 THEN EXPAND_TAC"v03n"
1065 THEN EXPAND_TAC"v12n"
1066 THEN EXPAND_TAC"v23n"
1067 THEN EXPAND_TAC"v13n"
1068 THEN EXPAND_TAC"v01"
1069 THEN EXPAND_TAC"v02"
1070 THEN EXPAND_TAC"v03"
1071 THEN EXPAND_TAC"v12"
1072 THEN EXPAND_TAC"v23"
1073 THEN EXPAND_TAC"v13"
1074 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1075 THEN MATCH_MP_TAC LIM_MUL
1076 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1077 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
1078 THEN POP_ASSUM MP_TAC
1079 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1081 THEN POP_ASSUM MATCH_MP_TAC
1082 THEN ASM_REWRITE_TAC[]
1084 THEN REWRITE_TAC[ETA_AX]
1086 MATCH_MP_TAC LIM_MUL
1087 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1088 THEN EXPAND_TAC"v01n"
1089 THEN EXPAND_TAC"v02n"
1090 THEN EXPAND_TAC"v03n"
1091 THEN EXPAND_TAC"v12n"
1092 THEN EXPAND_TAC"v23n"
1093 THEN EXPAND_TAC"v13n"
1094 THEN EXPAND_TAC"v01"
1095 THEN EXPAND_TAC"v02"
1096 THEN EXPAND_TAC"v03"
1097 THEN EXPAND_TAC"v12"
1098 THEN EXPAND_TAC"v23"
1099 THEN EXPAND_TAC"v13"
1100 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1101 THEN MATCH_MP_TAC LIM_MUL
1102 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1103 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
1104 THEN POP_ASSUM MP_TAC
1105 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1107 THEN POP_ASSUM MATCH_MP_TAC
1108 THEN ASM_REWRITE_TAC[]
1109 THEN MATCH_MP_TAC LIM_SUB
1111 THEN REWRITE_TAC[ETA_AX]
1113 MATCH_MP_TAC LIM_ADD
1115 MATCH_MP_TAC LIM_CMUL
1116 THEN MATCH_MP_TAC LIM_MUL
1117 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1118 THEN EXPAND_TAC"v01n"
1119 THEN EXPAND_TAC"v02n"
1120 THEN EXPAND_TAC"v03n"
1121 THEN EXPAND_TAC"v12n"
1122 THEN EXPAND_TAC"v23n"
1123 THEN EXPAND_TAC"v13n"
1124 THEN EXPAND_TAC"v01"
1125 THEN EXPAND_TAC"v02"
1126 THEN EXPAND_TAC"v03"
1127 THEN EXPAND_TAC"v12"
1128 THEN EXPAND_TAC"v23"
1129 THEN EXPAND_TAC"v13"
1130 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1132 MATCH_MP_TAC LIM_MUL
1133 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1134 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1135 THEN POP_ASSUM MP_TAC
1136 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1138 THEN POP_ASSUM MATCH_MP_TAC
1139 THEN ASM_REWRITE_TAC[]
1141 THEN REWRITE_TAC[ETA_AX]
1143 MATCH_MP_TAC LIM_MUL
1144 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1145 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
1146 THEN POP_ASSUM MP_TAC
1147 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1149 THEN POP_ASSUM MATCH_MP_TAC
1150 THEN ASM_REWRITE_TAC[]
1151 THEN MATCH_MP_TAC LIM_SUB
1153 THEN REWRITE_TAC[ETA_AX]
1155 MATCH_MP_TAC LIM_ADD
1157 MATCH_MP_TAC LIM_CMUL
1158 THEN MATCH_MP_TAC LIM_MUL
1159 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1160 THEN EXPAND_TAC"v01n"
1161 THEN EXPAND_TAC"v02n"
1162 THEN EXPAND_TAC"v03n"
1163 THEN EXPAND_TAC"v12n"
1164 THEN EXPAND_TAC"v23n"
1165 THEN EXPAND_TAC"v13n"
1166 THEN EXPAND_TAC"v01"
1167 THEN EXPAND_TAC"v02"
1168 THEN EXPAND_TAC"v03"
1169 THEN EXPAND_TAC"v12"
1170 THEN EXPAND_TAC"v23"
1171 THEN EXPAND_TAC"v13"
1172 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1174 MATCH_MP_TAC LIM_MUL
1175 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1176 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1177 THEN POP_ASSUM MP_TAC
1178 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1180 THEN POP_ASSUM MATCH_MP_TAC
1181 THEN ASM_REWRITE_TAC[]
1183 THEN REWRITE_TAC[ETA_AX]
1185 MATCH_MP_TAC LIM_MUL
1186 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1187 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
1188 THEN POP_ASSUM MP_TAC
1189 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1191 THEN POP_ASSUM MATCH_MP_TAC
1192 THEN ASM_REWRITE_TAC[]
1194 THEN REWRITE_TAC[ETA_AX]
1196 MATCH_MP_TAC LIM_CMUL
1197 THEN MATCH_MP_TAC LIM_MUL
1198 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1199 THEN EXPAND_TAC"v01n"
1200 THEN EXPAND_TAC"v02n"
1201 THEN EXPAND_TAC"v03n"
1202 THEN EXPAND_TAC"v12n"
1203 THEN EXPAND_TAC"v23n"
1204 THEN EXPAND_TAC"v13n"
1205 THEN EXPAND_TAC"v01"
1206 THEN EXPAND_TAC"v02"
1207 THEN EXPAND_TAC"v03"
1208 THEN EXPAND_TAC"v12"
1209 THEN EXPAND_TAC"v23"
1210 THEN EXPAND_TAC"v13"
1211 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1213 MATCH_MP_TAC LIM_MUL
1214 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1215 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
1216 THEN POP_ASSUM MP_TAC
1217 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1219 THEN POP_ASSUM MATCH_MP_TAC
1220 THEN ASM_REWRITE_TAC[]
1222 THEN REWRITE_TAC[ETA_AX]
1224 MATCH_MP_TAC LIM_MUL
1225 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1226 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
1227 THEN POP_ASSUM MP_TAC
1228 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1230 THEN POP_ASSUM MATCH_MP_TAC
1231 THEN ASM_REWRITE_TAC[]
1232 THEN MATCH_MP_TAC LIM_SUB
1234 THEN REWRITE_TAC[ETA_AX]
1236 MATCH_MP_TAC LIM_ADD
1238 MATCH_MP_TAC LIM_SUB
1240 MATCH_MP_TAC LIM_SUB
1242 MATCH_MP_TAC LIM_MUL
1243 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1244 THEN EXPAND_TAC"v01n"
1245 THEN EXPAND_TAC"v02n"
1246 THEN EXPAND_TAC"v03n"
1247 THEN EXPAND_TAC"v12n"
1248 THEN EXPAND_TAC"v23n"
1249 THEN EXPAND_TAC"v13n"
1250 THEN EXPAND_TAC"v01"
1251 THEN EXPAND_TAC"v02"
1252 THEN EXPAND_TAC"v03"
1253 THEN EXPAND_TAC"v12"
1254 THEN EXPAND_TAC"v23"
1255 THEN EXPAND_TAC"v13"
1256 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1258 MATCH_MP_TAC LIM_NEG
1259 THEN MATCH_MP_TAC LIM_MUL
1260 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1261 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1262 THEN POP_ASSUM MP_TAC
1263 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1265 THEN POP_ASSUM MATCH_MP_TAC
1266 THEN ASM_REWRITE_TAC[]
1268 THEN REWRITE_TAC[ETA_AX]
1270 MATCH_MP_TAC LIM_MUL
1271 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1272 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1273 THEN POP_ASSUM MP_TAC
1274 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1276 THEN POP_ASSUM MATCH_MP_TAC
1277 THEN ASM_REWRITE_TAC[]
1279 THEN REWRITE_TAC[ETA_AX]
1281 MATCH_MP_TAC LIM_MUL
1282 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1283 THEN EXPAND_TAC"v01n"
1284 THEN EXPAND_TAC"v02n"
1285 THEN EXPAND_TAC"v03n"
1286 THEN EXPAND_TAC"v12n"
1287 THEN EXPAND_TAC"v23n"
1288 THEN EXPAND_TAC"v13n"
1289 THEN EXPAND_TAC"v01"
1290 THEN EXPAND_TAC"v02"
1291 THEN EXPAND_TAC"v03"
1292 THEN EXPAND_TAC"v12"
1293 THEN EXPAND_TAC"v23"
1294 THEN EXPAND_TAC"v13"
1295 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1296 THEN MATCH_MP_TAC LIM_MUL
1297 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1298 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
1299 THEN POP_ASSUM MP_TAC
1300 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1302 THEN POP_ASSUM MATCH_MP_TAC
1303 THEN ASM_REWRITE_TAC[]
1305 THEN REWRITE_TAC[ETA_AX]
1307 MATCH_MP_TAC LIM_MUL
1308 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1309 THEN EXPAND_TAC"v01n"
1310 THEN EXPAND_TAC"v02n"
1311 THEN EXPAND_TAC"v03n"
1312 THEN EXPAND_TAC"v12n"
1313 THEN EXPAND_TAC"v23n"
1314 THEN EXPAND_TAC"v13n"
1315 THEN EXPAND_TAC"v01"
1316 THEN EXPAND_TAC"v02"
1317 THEN EXPAND_TAC"v03"
1318 THEN EXPAND_TAC"v12"
1319 THEN EXPAND_TAC"v23"
1320 THEN EXPAND_TAC"v13"
1321 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1322 THEN MATCH_MP_TAC LIM_MUL
1323 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1324 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
1325 THEN POP_ASSUM MP_TAC
1326 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1328 THEN POP_ASSUM MATCH_MP_TAC
1329 THEN ASM_REWRITE_TAC[]
1330 THEN MATCH_MP_TAC LIM_SUB
1332 THEN REWRITE_TAC[ETA_AX]
1334 MATCH_MP_TAC LIM_ADD
1336 MATCH_MP_TAC LIM_CMUL
1337 THEN MATCH_MP_TAC LIM_MUL
1338 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1339 THEN EXPAND_TAC"v01n"
1340 THEN EXPAND_TAC"v02n"
1341 THEN EXPAND_TAC"v03n"
1342 THEN EXPAND_TAC"v12n"
1343 THEN EXPAND_TAC"v23n"
1344 THEN EXPAND_TAC"v13n"
1345 THEN EXPAND_TAC"v01"
1346 THEN EXPAND_TAC"v02"
1347 THEN EXPAND_TAC"v03"
1348 THEN EXPAND_TAC"v12"
1349 THEN EXPAND_TAC"v23"
1350 THEN EXPAND_TAC"v13"
1351 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1353 MATCH_MP_TAC LIM_MUL
1354 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1355 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1356 THEN POP_ASSUM MP_TAC
1357 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1359 THEN POP_ASSUM MATCH_MP_TAC
1360 THEN ASM_REWRITE_TAC[]
1362 THEN REWRITE_TAC[ETA_AX]
1364 MATCH_MP_TAC LIM_MUL
1365 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1366 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
1367 THEN POP_ASSUM MP_TAC
1368 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1370 THEN POP_ASSUM MATCH_MP_TAC
1371 THEN ASM_REWRITE_TAC[]
1372 THEN MATCH_MP_TAC LIM_SUB
1374 THEN REWRITE_TAC[ETA_AX]
1376 MATCH_MP_TAC LIM_ADD
1378 MATCH_MP_TAC LIM_CMUL
1379 THEN MATCH_MP_TAC LIM_MUL
1380 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1381 THEN EXPAND_TAC"v01n"
1382 THEN EXPAND_TAC"v02n"
1383 THEN EXPAND_TAC"v03n"
1384 THEN EXPAND_TAC"v12n"
1385 THEN EXPAND_TAC"v23n"
1386 THEN EXPAND_TAC"v13n"
1387 THEN EXPAND_TAC"v01"
1388 THEN EXPAND_TAC"v02"
1389 THEN EXPAND_TAC"v03"
1390 THEN EXPAND_TAC"v12"
1391 THEN EXPAND_TAC"v23"
1392 THEN EXPAND_TAC"v13"
1393 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1395 MATCH_MP_TAC LIM_MUL
1396 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1397 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1398 THEN POP_ASSUM MP_TAC
1399 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1401 THEN POP_ASSUM MATCH_MP_TAC
1402 THEN ASM_REWRITE_TAC[]
1404 THEN REWRITE_TAC[ETA_AX]
1406 MATCH_MP_TAC LIM_MUL
1407 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1408 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
1409 THEN POP_ASSUM MP_TAC
1410 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1412 THEN POP_ASSUM MATCH_MP_TAC
1413 THEN ASM_REWRITE_TAC[]
1415 THEN REWRITE_TAC[ETA_AX]
1417 MATCH_MP_TAC LIM_CMUL
1418 THEN MATCH_MP_TAC LIM_MUL
1419 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1420 THEN EXPAND_TAC"v01n"
1421 THEN EXPAND_TAC"v02n"
1422 THEN EXPAND_TAC"v03n"
1423 THEN EXPAND_TAC"v12n"
1424 THEN EXPAND_TAC"v23n"
1425 THEN EXPAND_TAC"v13n"
1426 THEN EXPAND_TAC"v01"
1427 THEN EXPAND_TAC"v02"
1428 THEN EXPAND_TAC"v03"
1429 THEN EXPAND_TAC"v12"
1430 THEN EXPAND_TAC"v23"
1431 THEN EXPAND_TAC"v13"
1432 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1434 MATCH_MP_TAC LIM_MUL
1435 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1436 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
1437 THEN POP_ASSUM MP_TAC
1438 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1440 THEN POP_ASSUM MATCH_MP_TAC
1441 THEN ASM_REWRITE_TAC[]
1443 THEN REWRITE_TAC[ETA_AX]
1445 MATCH_MP_TAC LIM_MUL
1446 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1447 THEN MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
1448 THEN POP_ASSUM MP_TAC
1449 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1451 THEN POP_ASSUM MATCH_MP_TAC
1452 THEN ASM_REWRITE_TAC[]
1453 THEN MATCH_MP_TAC LIM_SUB
1455 THEN REWRITE_TAC[ETA_AX]
1458 let COLLINEAR_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
1459 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1460 /\ l IN B_SY1 (a_sy s) (b_sy s)
1462 ==> ~collinear{vec 0, row i (vecmats l),row (SUC (i MOD k_sy s)) (vecmats l)}`,
1463 REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;convex_local_fan;local_fan]
1465 THEN REPEAT STRIP_TAC
1466 THEN POP_ASSUM MP_TAC
1467 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`]
1468 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`]
1469 THEN POP_ASSUM MP_TAC
1470 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1475 let COLLINEAR_AZIM_CYCLE_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
1476 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1477 /\ l IN B_SY1 (a_sy s) (b_sy s)
1479 ==> ~collinear{vec 0, row i (vecmats l),
1480 azim_cycle (EE (row i (vecmats l)) (E_SY (vecmats l)))
1483 (row (SUC (i MOD k_sy s)) (vecmats l))}`,
1484 REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;convex_local_fan;local_fan]
1486 THEN REPEAT STRIP_TAC
1487 THEN POP_ASSUM MP_TAC
1488 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`]
1489 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`]
1490 THEN POP_ASSUM MP_TAC
1491 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1493 THEN MRESAL_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`][VECMATS_MATVEC_ID]
1494 THEN MRESAL_TAC Fan.sigma_fan_in_set_of_edge[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`][VECMATS_MATVEC_ID]
1495 THEN MRESAL_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY v') (E_SY v') (row i v')
1496 (row (SUC (i MOD k)) (v':real^3^M))`;`row i (vecmats (l:real^(M,3)finite_product))`][VECMATS_MATVEC_ID]
1497 THEN POP_ASSUM MP_TAC
1501 let AZIM_EQ_DIHV_IN_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product i.
1502 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1504 /\ (row i (vecmats l))= u
1505 /\ row (SUC (i MOD k_sy s)) (vecmats l)=v
1506 /\ azim_cycle (EE u (E_SY (vecmats l))) (vec 0) u v=w
1507 /\ l IN B_SY1 (a_sy s) (b_sy s)
1508 ==> azim (vec 0) u v w= dihV (vec 0) u v w`,
1511 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
1512 THEN REPEAT STRIP_TAC
1513 THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;CONDITION1_SY] THEN STRIP_TAC)
1514 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v':real^3^M`
1515 THEN POP_ASSUM MP_TAC
1516 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1517 THEN POP_ASSUM MP_TAC
1518 THEN POP_ASSUM MP_TAC
1519 THEN POP_ASSUM MP_TAC
1520 THEN DISCH_THEN(LABEL_TAC"THY")
1521 THEN DISCH_THEN(LABEL_TAC"THY2")
1523 THEN POP_ASSUM(fun th-> MP_TAC th
1524 THEN REWRITE_TAC[convex_local_fan]
1526 THEN POP_ASSUM MP_TAC
1527 THEN POP_ASSUM(fun th1-> MP_TAC th1
1528 THEN REWRITE_TAC[local_fan]
1531 THEN POP_ASSUM MP_TAC
1532 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
1534 THEN ASSUME_TAC th1)
1535 THEN DISCH_THEN(LABEL_TAC"THY1")
1538 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1539 THEN REMOVE_THEN"THYGIANG"(fun th-> SUBST_ALL_TAC(th) THEN ASSUME_TAC th)
1540 THEN MRESA_TAC (GEN_ALL EDGE_IN_F_SY)[`i:num`;`u:real^3`;`v:real^3`;`l:real^(M,3)finite_product`]
1541 THEN REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`u:real^3,v:real^3`)
1542 THEN REMOVE_ASSUM_TAC
1543 THEN POP_ASSUM MP_TAC
1544 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((u,v):real^3#real^3)`]
1545 THEN MRESA_TAC( GEN_ALL COLLINEAR_B_SY)[`k:num`;`i:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
1546 THEN MRESA_TAC( GEN_ALL COLLINEAR_AZIM_CYCLE_B_SY)[`k:num`;`i:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
1547 THEN MATCH_MP_TAC Local_lemmas.AZIM_LE_PI_EQ_DIHV
1548 THEN ASM_REWRITE_TAC[]);;
1551 let CONTINUOUS_ON_RHO_FUN_AND_AZIM=prove_by_refinement(`!s:stable_sy .
1552 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1553 ==> lift o(\x:real^(M,3)finite_product. sum (1..k_sy s)
1554 (\i. rho_fun (norm (row i (vecmats x))) * azim_in_fan (row i (vecmats x), row (SUC (i MOD (k_sy s))) (vecmats x)) (E_SY (vecmats x))))
1556 B_SY1 (a_sy s) (b_sy s)`,
1558 THEN SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG]
1559 THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM
1560 THEN SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
1561 THEN REPEAT STRIP_TAC
1562 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
1564 REWRITE_TAC[rho_fun;o_DEF;LIFT_ADD]
1565 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1566 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB]
1567 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1568 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1569 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1570 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1571 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;]
1572 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
1573 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
1574 THEN POP_ASSUM MP_TAC
1575 THEN ASM_REWRITE_TAC[IN_NUMSEG];
1576 MATCH_MP_TAC CONTINUOUS_ON_SAME_DOMAIN
1577 THEN EXISTS_TAC`(\y:real^(M,3)finite_product. lift(azim (vec 0) (row x (vecmats y)) (row (SUC (x MOD k_sy s)) (vecmats y))
1578 (azim_cycle (EE (row x (vecmats y)) (E_SY(vecmats y))) (vec 0) (row x (vecmats y)) (row (SUC (x MOD k_sy s)) (vecmats y)))))`
1581 THEN ASM_REWRITE_TAC[IN_NUMSEG;IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan]
1582 THEN REPEAT STRIP_TAC
1583 THEN MRESAL_TAC (GEN_ALL EDGE_IN_F_SY)[`x:num`;`row x (v:real^3^M)`;`row (SUC (x MOD k)) (v:real^3^M)`;`(matvec v):real^(M,3)finite_product`][VECMATS_MATVEC_ID]
1584 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY ((v:real^3^M) )`;`F_SY ((v:real^3^M))`;`E_SY ( (v:real^3^M))`;`row x (v:real^3^M),
1585 row (SUC (x MOD dimindex (:M))) v`][VECMATS_MATVEC_ID;];
1586 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
1587 THEN REPEAT STRIP_TAC
1588 THEN POP_ASSUM MP_TAC
1589 THEN POP_ASSUM MP_TAC
1590 THEN POP_ASSUM MP_TAC
1591 THEN DISCH_THEN(LABEL_TAC"THYGIANG1")
1592 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
1594 THEN ABBREV_TAC`u=(azim_cycle (EE (row x (vecmats a)) (E_SY (vecmats a))) (vec 0)
1596 (row (SUC (x MOD k_sy s)) (vecmats (a:real^(M,3)finite_product))))`
1597 THEN ABBREV_TAC`v= row x (vecmats (a:real^(M,3)finite_product))`
1598 THEN ABBREV_TAC`w=row (SUC (x MOD k_sy s)) (vecmats (a:real^(M,3)finite_product))`
1599 THEN ABBREV_TAC`wn=(\n:num. row (SUC (x MOD k_sy s)) (vecmats ((x':num->real^(M,3)finite_product) n)))`
1600 THEN ABBREV_TAC`vn=(\n. row x (vecmats ((x':num->real^(M,3)finite_product)n)))`
1601 THEN ABBREV_TAC`un=(\n. azim_cycle (EE (row x (vecmats ((x':num->real^(M,3)finite_product)n)))(E_SY (vecmats ((x':num->real^(M,3)finite_product)n)))) (vec 0) (row x (vecmats ((x':num->real^(M,3)finite_product)n))) (row (SUC (x MOD k_sy s)) (vecmats ((x':num->real^(M,3)finite_product) n))))`
1602 THEN SUBGOAL_THEN`!n:num. ~collinear{vec 0:real^3, vn n, wn n} /\ ~collinear{vec 0, vn n, un n}` ASSUME_TAC;
1608 THEN FIND_ASSUM MP_TAC`x IN 1..k_sy (s:stable_sy)`
1609 THEN REWRITE_TAC[IN_NUMSEG]
1611 THEN MRESA_TAC( GEN_ALL COLLINEAR_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) n`]
1612 THEN MRESA_TAC( GEN_ALL COLLINEAR_AZIM_CYCLE_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) n`];
1619 SUBGOAL_THEN`(\x1. lift
1620 (azim (vec 0) (row x (vecmats (x' x1)))
1621 (row (SUC (x MOD k_sy s)) (vecmats (x' x1)))
1622 (azim_cycle (EE (row x (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1624 (row x (vecmats (x' x1)))
1625 (row (SUC (x MOD k_sy s)) (vecmats (x' x1))))))
1627 (dihV (vec 0) (row x (vecmats (x' x1)))
1628 (row (SUC (x MOD k_sy s)) (vecmats (x' x1)))
1629 (azim_cycle (EE (row x (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1631 (row x (vecmats (x' x1)))
1632 (row (SUC (x MOD k_sy s)) (vecmats ((x':num->real^(M,3)finite_product) x1))))))
1634 REWRITE_TAC[FUN_EQ_THM;LIFT_EQ; o_DEF]
1636 THEN MATCH_MP_TAC AZIM_EQ_DIHV_IN_B_SY
1637 THEN EXISTS_TAC`s:stable_sy`
1638 THEN EXISTS_TAC`(x':num->real^(M,3)finite_product)x''`
1639 THEN EXISTS_TAC`x:num`
1640 THEN ASM_REWRITE_TAC[]
1641 THEN FIND_ASSUM MP_TAC`x IN 1..k_sy (s:stable_sy)`
1642 THEN REWRITE_TAC[IN_NUMSEG]
1644 POP_ASSUM(fun th-> REWRITE_TAC[th])
1645 THEN FIND_ASSUM MP_TAC`x IN 1..k_sy (s:stable_sy)`
1646 THEN REWRITE_TAC[IN_NUMSEG]
1648 THEN MRESA_TAC (GEN_ALL AZIM_EQ_DIHV_IN_B_SY)[`k:num`;`v:real^3`;`w:real^3`;`u:real^3`;`s:stable_sy`;`a:real^(M,3)finite_product`;`x:num`]
1650 THEN MATCH_MP_TAC SEQUENTIALLY_DIVH
1651 THEN ASM_REWRITE_TAC[]
1652 THEN MRESA_TAC( GEN_ALL COLLINEAR_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`a:real^(M,3)finite_product`]
1653 THEN MRESA_TAC( GEN_ALL COLLINEAR_AZIM_CYCLE_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`a:real^(M,3)finite_product`]
1654 THEN SUBGOAL_THEN`1 <= SUC (x MOD dimindex (:M)) /\
1655 SUC (x MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
1656 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1657 THEN MRESAL_TAC DIVISION[`x:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1658 THEN POP_ASSUM MP_TAC
1662 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x':num->real^(M,3)finite_product) n))`;`vecmats(a:real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
1663 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:num` THEN MRESA1_TAC th`(SUC (x MOD k))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"THY"))
1665 THEN FIND_ASSUM (fun th-> REWRITE_TAC[th])`k_sy (s:stable_sy)=k`
1666 THEN ASM_REWRITE_TAC[]
1667 THEN MP_TAC(ARITH_RULE`1<= x ==> x=1 \/ 1<x:num`)
1669 SUBGOAL_THEN`(\x1. azim_cycle (EE (row 1 (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1671 (row 1 (vecmats (x' x1)))
1672 (row (SUC (1 MOD k)) (vecmats (x' x1))))
1673 = (\x1. row k (vecmats ((x':num->real^(M,3)finite_product) x1)))` ASSUME_TAC;
1674 REWRITE_TAC[FUN_EQ_THM]
1676 THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
1677 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
1678 THEN MP_TAC(ARITH_RULE`2<k==> 1< k /\ 1<=k`)
1680 THEN MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`(row 1 (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`(row (SUC (1 MOD k)) (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`row k (vecmats ((x':num->real^(M,3)finite_product) x''))`;`(x':num->real^(M,3)finite_product) x''`][ARITH_RULE`SUC 0=1`]
1681 THEN POP_ASSUM MATCH_MP_TAC
1682 THEN REMOVE_THEN "THYGIANG"(fun th-> MRESA1_TAC th`x'':num` )
1683 THEN POP_ASSUM (fun th-> MP_TAC th
1684 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1687 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1691 MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) x''`][IN_NUMSEG;VECMATS_MATVEC_ID]
1692 THEN POP_ASSUM MP_TAC
1694 POP_ASSUM(fun th-> REWRITE_TAC[th])
1698 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
1699 THEN SUBGOAL_THEN`azim_cycle (EE (row 1 (vecmats a)) (E_SY (vecmats a)))
1702 (row (SUC (1 MOD k)) (vecmats a))
1703 = row k (vecmats ((a:real^(M,3)finite_product) ))` ASSUME_TAC;
1704 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
1705 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
1706 THEN MP_TAC(ARITH_RULE`2<k==> 1< k /\ 1<=k`)
1708 THEN MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`(row 1 (vecmats ((a:real^(M,3)finite_product) )))`;`(row (SUC (1 MOD k)) (vecmats ((a:real^(M,3)finite_product))))`;`row k (vecmats ((a:real^(M,3)finite_product) ))`;`(a:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1`]
1709 THEN POP_ASSUM MATCH_MP_TAC
1710 THEN REMOVE_THEN "THYGIANG1"(fun th-> MP_TAC th
1711 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1714 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1718 MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(a:real^(M,3)finite_product) `][IN_NUMSEG;VECMATS_MATVEC_ID]
1719 THEN POP_ASSUM MP_TAC
1721 POP_ASSUM(fun th-> ASM_REWRITE_TAC[th])
1722 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`k:num`)
1723 THEN POP_ASSUM MATCH_MP_TAC
1724 THEN MP_TAC(ARITH_RULE`2<k==> 1< k /\ 1<=k`)
1727 SUBGOAL_THEN`(\x1. azim_cycle (EE (row x (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1729 (row x (vecmats (x' x1)))
1730 (row (SUC (x MOD k)) (vecmats (x' x1))))
1731 = (\x1. row (x-1) (vecmats ((x':num->real^(M,3)finite_product) x1)))` ASSUME_TAC;
1732 REWRITE_TAC[FUN_EQ_THM]
1734 THEN MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`x-1:num`;`(row x (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`(row (SUC (x MOD k)) (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`row (x-1) (vecmats ((x':num->real^(M,3)finite_product) x''))`;`(x':num->real^(M,3)finite_product) x''`][ARITH_RULE`SUC 0=1`]
1735 THEN POP_ASSUM MATCH_MP_TAC
1736 THEN MP_TAC(ARITH_RULE`2<k /\ 1< x/\ x<= k ==> 1< k /\ 1<=k /\ 1<= x-1 /\ x-1<= k/\ x-1< k`)
1738 THEN MRESAL_TAC MOD_LT[`x-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
1739 THEN MP_TAC(ARITH_RULE`1<= x /\ x<= dimindex (:M) ==> SUC (x-1)=x`)
1741 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1742 THEN ASM_REWRITE_TAC[]
1743 THEN REMOVE_THEN "THYGIANG"(fun th-> MRESA1_TAC th`x'':num` )
1744 THEN POP_ASSUM (fun th-> MP_TAC th
1745 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1748 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1750 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) x''`][IN_NUMSEG;VECMATS_MATVEC_ID]
1751 THEN POP_ASSUM MP_TAC
1753 POP_ASSUM(fun th-> REWRITE_TAC[th])
1757 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
1758 THEN SUBGOAL_THEN`azim_cycle (EE (row x (vecmats a)) (E_SY (vecmats a)))
1761 (row (SUC (x MOD k)) (vecmats a))
1762 = row (x-1) (vecmats ((a:real^(M,3)finite_product) ))` ASSUME_TAC;
1763 MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`x-1:num`;`(row x (vecmats ((a:real^(M,3)finite_product) )))`;`(row (SUC (x MOD k)) (vecmats ((a:real^(M,3)finite_product))))`;`row (x-1) (vecmats ((a:real^(M,3)finite_product) ))`;`(a:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1`]
1764 THEN POP_ASSUM MATCH_MP_TAC
1765 THEN MP_TAC(ARITH_RULE`2<k /\ 1< x/\ x<= k ==> 1< k /\ 1<=k /\ 1<= x-1 /\ x-1<= k/\ x-1< k`)
1767 THEN MRESAL_TAC MOD_LT[`x-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
1768 THEN MP_TAC(ARITH_RULE`1<= x /\ x<= dimindex (:M) ==> SUC (x-1)=x`)
1770 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1771 THEN ASM_REWRITE_TAC[]
1772 THEN REMOVE_THEN "THYGIANG1"(fun th-> MP_TAC th
1773 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1776 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1778 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(a:real^(M,3)finite_product) `][IN_NUMSEG;VECMATS_MATVEC_ID]
1779 THEN POP_ASSUM MP_TAC
1781 FIND_ASSUM(fun th-> REWRITE_TAC[th])`k_sy (s:stable_sy)= k`
1782 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[th])
1783 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`x-1:num`)
1784 THEN POP_ASSUM MATCH_MP_TAC
1785 THEN MP_TAC(ARITH_RULE`1< x /\ x<= dimindex (:M) ==> 1<= x-1 /\ x-1<=dimindex (:M)`)
1788 let CONTINUOUS_ON_TAU_FUN=prove(`!s:stable_sy .
1789 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1790 ==> lift o(\l:real^(M,3)finite_product. tau_fun (V_SY (vecmats l)) (E_SY (vecmats l)) (F_SY (vecmats l))) continuous_on (B_SY1 (a_sy s) (b_sy s))`,
1791 REWRITE_TAC[tau_fun; o_DEF;LIFT_SUB]
1792 THEN REPEAT STRIP_TAC
1793 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1794 THEN MRESAL_TAC (GEN_ALL CONTINUOUS_ON_RHO_FUN_AND_AZIM)[`k:num`;`s:stable_sy`][o_DEF]
1797 MATCH_MP_TAC CONTINUOUS_ON_SAME_DOMAIN
1798 THEN EXISTS_TAC`(\x:real^(M,3)finite_product. lift
1800 (\i. rho_fun (norm (row i (vecmats x))) *
1802 (row i (vecmats x),row (SUC (i MOD k)) (vecmats x))
1803 (E_SY (vecmats x)))))`
1804 THEN ASM_REWRITE_TAC[]
1805 THEN REPEAT STRIP_TAC
1806 THEN MRESA_TAC (GEN_ALL CHANGE_SUM_TAU_FUN)[`k:num`;`s:stable_sy`;`x:real^(M,3)finite_product`];
1807 MATCH_MP_TAC CONTINUOUS_ON_SAME_DOMAIN
1808 THEN EXISTS_TAC`(\x:real^(M,3)finite_product. lift ((pi + sol0) * &(k-2 )))`
1809 THEN REWRITE_TAC[CONTINUOUS_ON_CONST]
1810 THEN REPEAT STRIP_TAC
1811 THEN MP_TAC(ARITH_RULE`2<k==> 1<k`)
1813 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`x:real^(M,3)finite_product`][IN_NUMSEG;VECMATS_MATVEC_ID;SET_RULE`(1 <= i /\ i <= k) /\
1814 (1 <= j /\ j <= k) /\
1815 row i (vecmats x) = row j (vecmats x)
1816 <=> 1 <= i /\ i <= k /\
1818 row i (vecmats x) = row j (vecmats x)`]
1819 THEN MRESA1_TAC (GEN_ALL CARD_F_SY_EQ)`x:real^(M,3)finite_product`]);;
1822 let CONTINUOUS_ON_TAU_STAR=prove(`!s:stable_sy .
1823 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1824 ==> lift o(\l:real^(M,3)finite_product. tau_star s l) continuous_on (B_SY1 (a_sy s) (b_sy s))`,
1825 REWRITE_TAC[tau_star;o_DEF;LIFT_SUB]
1826 THEN REPEAT STRIP_TAC
1827 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1828 THEN MRESAL_TAC (GEN_ALL CONTINUOUS_ON_D_FUN)[`k:num`;`s:stable_sy`][o_DEF]
1829 THEN MRESAL_TAC (GEN_ALL CONTINUOUS_ON_TAU_FUN)[`k:num`;`s:stable_sy`][o_DEF]);;
1831 let MINIMUM_IN_B_SY=prove(`!s:stable_sy .
1832 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1833 /\ ~(B_SY1 (a_sy s) (b_sy s) = {}:real^(M,3)finite_product->bool)
1834 ==> ?x:real^(M,3)finite_product. x IN (B_SY1 (a_sy s) (b_sy s))
1835 /\ (!y:real^(M,3)finite_product. y IN (B_SY1 (a_sy s) (b_sy s))
1836 ==> tau_star s x <= tau_star s y)`,
1838 THEN MRESA_TAC CONTINUOUS_ATTAINS_INF[`(\l:real^(M,3)finite_product. tau_star (s:stable_sy) l)`;`(B_SY1 (a_sy s) (b_sy (s:stable_sy))):real^(M,3)finite_product->bool`]
1839 THEN POP_ASSUM MATCH_MP_TAC
1843 THEN MRESA_TAC(GEN_ALL WJSCPRO) [`d_sy (s:stable_sy)`;`J_SY(s:stable_sy)`;`k:num`;`a_sy(s:stable_sy)`;`b_sy(s:stable_sy)`;]
1844 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`;
1845 MRESA_TAC (GEN_ALL CONTINUOUS_ON_TAU_STAR)[`k:num`;`s:stable_sy`]]);;
1848 let HDPLYGY=prove(`!s:stable_sy .
1849 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1850 /\ ~(B_SY1 (a_sy s) (b_sy s) = {}:real^(M,3)finite_product->bool)
1852 lift o(\l:real^(M,3)finite_product. tau_star s l) continuous_on (B_SY1 (a_sy s) (b_sy s))
1853 /\(?x:real^(M,3)finite_product. x IN (B_SY1 (a_sy s) (b_sy s))
1854 /\ (!y:real^(M,3)finite_product. y IN (B_SY1 (a_sy s) (b_sy s))
1855 ==> tau_star s x <= tau_star s y))`,
1858 MRESA_TAC(GEN_ALL CONTINUOUS_ON_TAU_STAR)[`k:num`;`s:stable_sy`];
1859 MRESA_TAC (GEN_ALL MINIMUM_IN_B_SY)[`k:num`;`s:stable_sy`]]);;