2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Local Fan *)
6 (* Author: Hoang Le Truong *)
8 (* ========================================================================= *)
13 module Gbycpxs = struct
31 open Prove_by_refinement;;
33 open Wrgcvdr_cizmrrh;;
40 open Flyspeck_constants;;
43 let CARD_F_SY_IN_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
44 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
45 /\ l IN B_SY1 (a_sy s) (b_sy s)
46 ==> CARD (F_SY (vecmats l))=k`,
48 THEN MP_TAC(ARITH_RULE`2<k==> 1<k`)
50 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`][IN_NUMSEG;VECMATS_MATVEC_ID;SET_RULE`(1 <= i /\ i <= k) /\
52 row i (vecmats x) = row j (vecmats x)
53 <=> 1 <= i /\ i <= k /\
55 row i (vecmats x) = row j (vecmats x)`]
56 THEN MRESA1_TAC (GEN_ALL CARD_F_SY_EQ)`l:real^(M,3)finite_product`);;
59 let SOL0_POS=prove(`&0< sol0`,
60 REWRITE_TAC[sol0; REAL_ARITH`&0 < &3 * acs (&1 / &3) - pi
61 <=> pi/ &3 < acs (&1 / &3) `]
62 THEN MRESAL1_TAC Trigonometry2.ACS`&1/ &3`[REAL_ARITH`-- &1 <= &1 / &3 /\ &1 / &3 <= &1`]
63 THEN MP_TAC(REAL_ARITH`&0< pi==> &0 <= pi / &3 /\ pi / &3 <= pi`)
64 THEN ASM_REWRITE_TAC[PI_WORKS]
66 THEN MRESAL1_TAC COS_ACS`&1/ &3`[REAL_ARITH`-- &1 <= &1 / &3 /\ &1 / &3 <= &1`]
67 THEN MRESA_TAC COS_MONO_LT_EQ[`acs (&1 / &3)`;`pi/ &3`]
68 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
69 THEN REWRITE_TAC[ARITH_RULE`pi/ &3= pi/ &2- pi/ &6`;Trigonometry.SCEZKRH2;SIN_PI6]
70 THEN REAL_ARITH_TAC);;
72 let SIGMA_SY_LE1=prove(`!s:stable_sy. sigma_sy s<= &1`,
74 THEN REWRITE_TAC[sigma_sy]
75 THEN DISJ_CASES_TAC(SET_RULE`(ear_sy s) \/ ~(ear_sy (s:stable_sy))`)
76 THEN ASM_REWRITE_TAC[]
77 THEN REAL_ARITH_TAC);;
80 let B_SY_LE_CSTAB=prove(`!s:stable_sy l:real^(M,3)finite_product.
81 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
83 /\ l IN B_SY1 (a_sy s) (b_sy s)
84 ==> norm (row i (vecmats l) - row (SUC (i MOD k)) (vecmats l))<= cstab`,
87 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
89 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)
90 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
92 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
96 THEN DISCH_THEN(LABEL_TAC"THY")
97 THEN DISCH_THEN(LABEL_TAC"THY2")
99 THEN POP_ASSUM(fun th-> MP_TAC th
100 THEN REWRITE_TAC[convex_local_fan]
102 THEN POP_ASSUM MP_TAC
103 THEN POP_ASSUM(fun th1-> MP_TAC th1
104 THEN REWRITE_TAC[local_fan]
107 THEN POP_ASSUM MP_TAC
108 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
111 THEN DISCH_THEN(LABEL_TAC"THY1")
114 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
115 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
116 SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
118 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
119 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
120 THEN POP_ASSUM MP_TAC
124 THEN REMOVE_THEN"THY2"(fun th-> MRESA_TAC th[`i:num`;`SUC(i MOD k)`])
125 THEN POP_ASSUM MP_TAC
126 THEN MP_TAC(ARITH_RULE`i<=k==> i<= k-1 \/ i=k`)
129 MP_TAC(ARITH_RULE`2<k ==> 1<=k /\ 1<k`)
131 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i+1`][ARITH_RULE`1*A=A`]
132 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`i+1:num`;`k:num`]
133 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
134 THEN REMOVE_ASSUM_TAC
135 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
136 THEN POP_ASSUM MP_TAC
137 THEN REMOVE_ASSUM_TAC
138 THEN REMOVE_ASSUM_TAC
139 THEN POP_ASSUM MP_TAC
140 THEN REWRITE_TAC[constraint_system]
142 THEN REMOVE_ASSUM_TAC
143 THEN REMOVE_ASSUM_TAC
144 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`i+1:num`][ARITH_RULE`A+0=A`])
145 THEN ONCE_REWRITE_TAC[ARITH_RULE`1+A=A+1`]
146 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
147 THEN MP_TAC(ARITH_RULE`i <= k-1 /\ 1<=i ==> i< k`)
149 THEN MRESA_TAC MOD_LT[`i:num`;`k:num`]
150 THEN REWRITE_TAC[ADD1]
152 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
153 THEN MP_TAC(ARITH_RULE`2<k ==> 0<= k-1/\ 1<k`)
155 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
156 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
157 THEN REMOVE_ASSUM_TAC
158 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0+1=1`])
159 THEN POP_ASSUM MP_TAC
160 THEN REMOVE_ASSUM_TAC
161 THEN REMOVE_ASSUM_TAC
162 THEN POP_ASSUM MP_TAC
163 THEN REWRITE_TAC[constraint_system]
165 THEN REMOVE_ASSUM_TAC
166 THEN REMOVE_ASSUM_TAC
167 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1:num`;`k:num`][ARITH_RULE`A+0=A`])
168 THEN MP_TAC(ARITH_RULE`2<k ==> 1<= k/\ 1<k /\ ~(k=0)`)
170 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
171 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ k+k=k *2`]
172 THEN REAL_ARITH_TAC]]);;
178 let PROPERTIES_EAR_SY=prove(`!s:stable_sy. ear_sy s ==> ?i. J_SY s={{i,f_sy s i}} /\ i IN I_SY s`,
180 THEN REWRITE_TAC[ear_sy]
182 THEN MRESA1_TAC FINITE_J_SY`s:stable_sy`
183 THEN MRESA1_TAC (GEN_ALL Local_lemmas.FINITE_CARD1_IMP_SINGLETON)`J_SY(s:stable_sy)`
184 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
185 THEN REMOVE_ASSUM_TAC
186 THEN REMOVE_ASSUM_TAC
187 THEN REMOVE_ASSUM_TAC
188 THEN POP_ASSUM MP_TAC
189 THEN ASM_REWRITE_TAC[constraint_system;SUBSET;IN_SING;IN_ELIM_THM;]
191 THEN REMOVE_ASSUM_TAC
192 THEN ONCE_REWRITE_TAC[EXTENSION]
193 THEN REWRITE_TAC[IN_SING]
194 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:(num->bool)`)
195 THEN EXISTS_TAC`i:num`
196 THEN ASM_REWRITE_TAC[]);;
202 let SING_J1_SY=prove_by_refinement(`!s:stable_sy. ear_sy s /\ I_SY s=0.. k_sy s -1 /\ f_sy s=(\i. ((1+i):num MOD k))/\ k_sy s =k /\ 2<k ==> ?i. J1_SY s= {(i,SUC(i MOD k_sy s))} /\ J_SY s= {{i MOD k,f_sy s i}} /\ i<=k /\ 1<=i`,
204 THEN MRESAL1_TAC PROPERTIES_EAR_SY`s:stable_sy`[IN_NUMSEG]
205 THEN DISJ_CASES_TAC(ARITH_RULE`i=0 \/ 1<= i`);
206 EXISTS_TAC`k_sy(s:stable_sy):num`
207 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ k<=k /\ 1<=k`)
209 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
210 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
211 THEN MRESA_TAC MOD_ADD_MOD[`1:num`;`k:num`;`k:num`]
212 THEN REMOVE_ASSUM_TAC
213 THEN REMOVE_ASSUM_TAC
214 THEN REMOVE_ASSUM_TAC
215 THEN REMOVE_ASSUM_TAC
216 THEN REMOVE_ASSUM_TAC
217 THEN REMOVE_ASSUM_TAC
218 THEN REMOVE_ASSUM_TAC
219 THEN ASM_REWRITE_TAC[J1_SY;IN_SING;]
220 THEN ONCE_REWRITE_TAC[EXTENSION]
221 THEN REWRITE_TAC[IN_ELIM_THM;IN_SING;IN_NUMSEG]
225 THEN REWRITE_TAC[PAIR_EQ]
226 THEN MP_TAC(ARITH_RULE`i' <= k_sy s==> i' < k_sy s \/ i' = k_sy (s:stable_sy)`)
228 MRESA_TAC MOD_LT[`i':num`;`k_sy(s:stable_sy)`]
229 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th])
230 THEN REPEAT DISCH_TAC
231 THEN MP_TAC(ARITH_RULE`i' < k_sy s==> 1+i' < k_sy s \/ 1+i' = k_sy (s:stable_sy)`)
233 MRESA_TAC MOD_LT[`1+i':num`;`k_sy(s:stable_sy)`]
234 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th])
235 THEN REPEAT DISCH_TAC
236 THEN MP_TAC(ARITH_RULE`1<= i' ==> ~(i'= 0) /\ ~(1+i'=0)`)
238 THEN MP_TAC(SET_RULE`~(i'= 0) /\ ~(1+i'=0) ==> ~({i', 1+i'} = {0, (1+ 0) MOD k})`)
239 THEN ASM_REWRITE_TAC[];
240 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
241 THEN REPEAT DISCH_TAC
242 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
244 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
245 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
246 THEN REPEAT DISCH_TAC
247 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
248 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`])
249 THEN REPEAT DISCH_TAC
250 THEN MP_TAC(SET_RULE`{i', 0} = {0, 1} /\ ~(0=1)==> i'=1`)
252 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
253 THEN REPEAT DISCH_TAC
254 THEN POP_ASSUM MP_TAC
256 MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
258 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO];
260 THEN EXISTS_TAC`k:num`
261 THEN ASM_REWRITE_TAC[]
262 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<=k/\ ~(0=1) /\ ~(1+1=k)`)
264 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
267 THEN MP_TAC(ARITH_RULE`i<= k-1/\ 2<k==> i<k/\ i<=k`)
269 THEN MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`]
270 THEN REMOVE_ASSUM_TAC
271 THEN REMOVE_ASSUM_TAC
272 THEN REMOVE_ASSUM_TAC
273 THEN ASM_REWRITE_TAC[J1_SY;IN_SING;]
274 THEN ONCE_REWRITE_TAC[EXTENSION]
275 THEN REWRITE_TAC[IN_ELIM_THM;IN_SING;IN_NUMSEG]
279 THEN REWRITE_TAC[PAIR_EQ]
280 THEN MP_TAC(ARITH_RULE`i' <= k_sy s==> i' = k_sy (s:stable_sy) \/ i' < k_sy s `)
282 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
283 THEN REPEAT DISCH_TAC
284 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
286 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
287 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
288 THEN REPEAT DISCH_TAC
289 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
290 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`])
291 THEN REPEAT DISCH_TAC
292 THEN MP_TAC(ARITH_RULE`1<= i==> ~(i=0)/\ ~(0=2)`)
294 THEN MP_TAC(SET_RULE`{0, 1} = {i, (1+i ) MOD k} /\ ~(i=0)==> i=1`)
296 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+1=2`] )
297 THEN REPEAT DISCH_TAC
298 THEN MRESA_TAC MOD_LT[`2:num`;`k_sy(s:stable_sy)`]
299 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+1=2`] )
300 THEN REPEAT DISCH_TAC
301 THEN SUBGOAL_THEN`~({0,1}={1,2})` MP_TAC;
302 REWRITE_TAC[EXTENSION;SET_RULE`x IN {A,B}<=> x= A \/ x=B`;]
303 THEN POP_ASSUM MP_TAC
306 MRESA_TAC MOD_LT[`i':num`;`k_sy(s:stable_sy)`]
307 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th])
308 THEN REPEAT DISCH_TAC
309 THEN MP_TAC(ARITH_RULE`i' < k_sy s==> 1+i' = k_sy (s:stable_sy) \/ 1+ i' < k_sy s `)
311 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
312 THEN REPEAT DISCH_TAC
313 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
315 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
316 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
317 THEN REPEAT DISCH_TAC
318 THEN MP_TAC(ARITH_RULE`1<= i==> ~(i=0)/\ ~(0=2)`)
320 THEN MP_TAC(SET_RULE`{i', 0} = {i, (1+i) MOD k} /\ ~(i=0)==> i=i'`)
322 THEN MRESA_TAC MOD_LT[`i':num`;`k_sy(s:stable_sy)`];
323 MP_TAC(ARITH_RULE`i <= k-1 /\ 2< k==> 1+i = k \/ 1+i < k `)
325 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
326 THEN REPEAT DISCH_TAC
327 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
329 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
330 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
331 THEN REPEAT DISCH_TAC
332 THEN MRESA_TAC MOD_LT[`1+i':num`;`k_sy(s:stable_sy)`]
333 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
334 THEN REPEAT DISCH_TAC
335 THEN MP_TAC(ARITH_RULE`1<= i' ==> ~(i'= 0) /\ ~(1+i'=0)`)
337 THEN MP_TAC(SET_RULE`~(i'= 0) /\ ~(1+i'=0) ==> ~({i', 1+i' } = {i, 0})`)
339 MRESA_TAC MOD_LT[`1+i':num`;`k_sy(s:stable_sy)`]
340 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
341 THEN REPEAT DISCH_TAC
342 THEN MRESA_TAC MOD_LT[`1+i:num`;`k_sy(s:stable_sy)`]
343 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
344 THEN REPEAT DISCH_TAC
345 THEN MP_TAC(SET_RULE`{i',1+ i'} = {i,1+ i} ==> i= 1+i' \/ i=i'`)
347 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+(1+i)=2+i`] )
348 THEN REPEAT DISCH_TAC
349 THEN MP_TAC(ARITH_RULE`~(i'= 2+i')`)
351 THEN SUBGOAL_THEN`~({i', 1+i'} = {1+i', 2+i'})` MP_TAC;
353 THEN MP_TAC(ARITH_RULE`~(i'= 1+i') /\ ~(1+i'= 2+i')`)
356 MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`];
358 THEN EXISTS_TAC`i:num`
359 THEN ASM_REWRITE_TAC[]
360 THEN MP_TAC(ARITH_RULE`i<=k-1 /\ 2<k==> i<= k/\ i<k`)
362 THEN MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`]]);;
365 let D_FUN_LE=prove_by_refinement(`!s:stable_sy l:real^(M,3)finite_product.
366 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
368 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
369 /\ l IN B_SY1 (a_sy s) (b_sy s)
370 ==> d_fun (s,l) <= #0.92`,
372 THEN SUBGOAL_THEN `d_fun(s:stable_sy,(l:real^(M,3)finite_product))<= d_sy s+ #0.1 *(cstab- sqrt(&8)) `
374 REWRITE_TAC[d_fun;sigma_sy]
375 THEN MATCH_MP_TAC(REAL_ARITH`b<=c==> a+ #0.1 * b<=a+ #0.1* c`)
376 THEN DISJ_CASES_TAC(SET_RULE`~(ear_sy s) \/ (ear_sy (s:stable_sy))`)
377 THEN ASM_REWRITE_TAC[];
378 MATCH_MP_TAC(REAL_ARITH`&0<= a/\ &0<= b==> -- &1 *a<=b`);
380 MATCH_MP_TAC SUM_POS_LE
381 THEN REWRITE_TAC[FINITE_J1_SY]
382 THEN REWRITE_TAC[J1_SY;IN_ELIM_THM]
383 THEN REPEAT STRIP_TAC
384 THEN ASM_REWRITE_TAC[]
385 THEN POP_ASSUM MP_TAC
386 THEN POP_ASSUM MP_TAC
387 THEN ASM_REWRITE_TAC[IN_NUMSEG]
389 THEN MRESA_TAC (GEN_ALL B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
390 THEN POP_ASSUM MP_TAC
392 REWRITE_TAC[REAL_ARITH`&0<= a-b<=> b<=a`;cstab]
393 THEN MATCH_MP_TAC REAL_LE_LSQRT
395 MRESAL_TAC(GEN_ALL SING_J1_SY)[`k:num`;`s:stable_sy`][SUM_SING;REAL_ARITH`&1 *A=A`;REAL_ARITH`A-B<= A-C<=> C<=B`]
396 THEN MP_TAC(ARITH_RULE`i<=k==> i=k \/ i< k:num`)
398 MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ 1<=k/\ k<=k `)
400 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
401 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ k+k=k *2`]
402 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
403 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
404 THEN MRESA_TAC MOD_ADD_MOD[`1:num`;`k:num`;`k:num`]
405 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
406 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num/\ 1+0=1`;IN_SING]
407 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`1`])
408 THEN REMOVE_ASSUM_TAC
409 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
410 THEN REMOVE_ASSUM_TAC
411 THEN REMOVE_ASSUM_TAC
412 THEN POP_ASSUM MP_TAC
413 THEN REWRITE_TAC[constraint_system]
415 THEN REMOVE_ASSUM_TAC
416 THEN REMOVE_ASSUM_TAC
417 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1`;`k:num`][ARITH_RULE`A+0=A/\ k+k= k* 2`])
418 THEN REMOVE_ASSUM_TAC
419 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
420 THEN FIND_ASSUM MP_TAC`(l:real^(M,3)finite_product) IN B_SY1 (a_sy s) (b_sy (s:stable_sy))`
421 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION1_SY]
423 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
424 THEN REMOVE_ASSUM_TAC
425 THEN REMOVE_ASSUM_TAC
426 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k:num`;`1:num`][ARITH_RULE`1<=1`]);
427 MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`]
428 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ 1<=k/\ k<=k `)
430 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`1+i:num`;`k:num`]
431 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ k+k=k *2`]
432 THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`1+i:num`][ARITH_RULE`1*A=A`]
433 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num/\ 0+1=1`;IN_SING]
434 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`;`(1+i) MOD k`])
435 THEN REMOVE_ASSUM_TAC
436 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
437 THEN REMOVE_ASSUM_TAC
438 THEN REMOVE_ASSUM_TAC
439 THEN POP_ASSUM MP_TAC
440 THEN REWRITE_TAC[constraint_system]
442 THEN REMOVE_ASSUM_TAC
443 THEN REMOVE_ASSUM_TAC
444 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`1+i:num`][ARITH_RULE`A+0=A`])
445 THEN REMOVE_ASSUM_TAC
446 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
447 THEN MP_TAC(ARITH_RULE`i<k==> 1<= 1+i /\ 1+i<=k`)
449 THEN FIND_ASSUM MP_TAC`(l:real^(M,3)finite_product) IN B_SY1 (a_sy s) (b_sy (s:stable_sy))`
450 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION1_SY]
452 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID;ADD1]
453 THEN REMOVE_ASSUM_TAC
454 THEN REMOVE_ASSUM_TAC
455 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`1+i:num`][ARITH_RULE`1<=1`])
456 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1/\ 1+i= SUC i`;ADD1]
457 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+1=1+i`]
458 THEN ASM_REWRITE_TAC[];
459 MATCH_MP_TAC(REAL_ARITH`d_fun (s,l) <= d_sy s + #0.1 * (cstab - sqrt (&8))
460 /\ d_sy s <= #0.9 /\ cstab - sqrt (&8)<= #0.2
461 ==> d_fun (s,l) <= #0.92`)
462 THEN ASM_REWRITE_TAC[cstab;REAL_ARITH`#3.01 - sqrt (&8) <= #0.2 <=> #2.81 <= sqrt (&8) `]
463 THEN MATCH_MP_TAC REAL_LE_RSQRT
464 THEN REAL_ARITH_TAC]);;
467 let TAU_FUN_LE=prove_by_refinement(`!s:stable_sy l:real^(M,3)finite_product.
468 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
469 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
470 /\ l IN B_SY1 (a_sy s) (b_sy s)
471 ==> #0.92< tau_fun (V_SY(vecmats l)) (E_SY(vecmats l)) (F_SY(vecmats l))`,
473 THEN ASM_SIMP_TAC[tau_fun;rho_fun]
474 THEN MRESA_TAC (GEN_ALL CARD_F_SY_IN_B_SY)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
475 THEN MRESA1_TAC (GEN_ALL FINITE_F_SY)`l:real^(M,3)finite_product`
476 THEN ASM_SIMP_TAC[REAL_ARITH`(&1+B)*C=C+B*C`;SUM_ADD]
477 THEN SUBGOAL_THEN`&0<= sum (F_SY (vecmats l))
478 (\x. (inv (&2 * h0 - &2) * inv pi * sol0 * (norm (FST x) - &2)) *
479 azim_in_fan x (E_SY (vecmats (l:real^(M,3)finite_product))))`ASSUME_TAC;
480 MATCH_MP_TAC SUM_POS_LE
481 THEN ASM_REWRITE_TAC[]
482 THEN REPEAT STRIP_TAC
483 THEN MATCH_MP_TAC REAL_LE_MUL
485 MATCH_MP_TAC REAL_LE_MUL
487 REWRITE_TAC[REAL_LE_INV_EQ;h0]
489 MATCH_MP_TAC REAL_LE_MUL
491 REWRITE_TAC[REAL_LE_INV_EQ;]
492 THEN MATCH_MP_TAC(REAL_ARITH`&0<a==> &0 <= a`)
493 THEN REWRITE_TAC[PI_WORKS];
494 MATCH_MP_TAC REAL_LE_MUL
496 MATCH_MP_TAC(REAL_ARITH`&0<a==> &0 <= a`)
497 THEN REWRITE_TAC[SOL0_POS];
499 THEN REMOVE_ASSUM_TAC
500 THEN REMOVE_ASSUM_TAC
501 THEN POP_ASSUM MP_TAC
502 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM]
504 THEN POP_ASSUM MP_TAC
505 THEN REMOVE_ASSUM_TAC
506 THEN REMOVE_ASSUM_TAC
507 THEN POP_ASSUM MP_TAC
508 THEN DISCH_THEN(LABEL_TAC"THY")
510 THEN ASM_REWRITE_TAC[IN_ELIM_THM;F_SY]
512 THEN REMOVE_THEN"THY"(fun th-> MRESAL1_TAC th `i:num`[VECMATS_MATVEC_ID;ball_annulus;IN_ELIM_THM;DIFF;ball;dist;VECTOR_ARITH`vec 0-A = --A`;NORM_NEG])
513 THEN POP_ASSUM MP_TAC
516 THEN REMOVE_ASSUM_TAC
517 THEN REMOVE_ASSUM_TAC
518 THEN POP_ASSUM MP_TAC
519 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;convex_local_fan]
522 THEN ASM_SIMP_TAC[azim;VECMATS_MATVEC_ID]
523 THEN MRESAL_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))`;`x:real^3#real^3`][VECMATS_MATVEC_ID;azim];
524 MATCH_MP_TAC(REAL_ARITH`
525 &0<= sum (F_SY (vecmats l))
526 (\x. (inv (&2 * h0 - &2) * inv pi * sol0 * (norm (FST x) - &2)) *
527 azim_in_fan x (E_SY (vecmats (l:real^(M,3)finite_product))))
530 sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l))) -
533 (sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l))) +
534 sum (F_SY (vecmats l))
535 (\x. (inv (&2 * h0 - &2) * inv pi * sol0 * (norm (FST x) - &2)) *
536 azim_in_fan x (E_SY (vecmats l)))) -
537 (pi + sol0) * &(k-2)`)
538 THEN ASM_REWRITE_TAC[]
539 THEN ONCE_REWRITE_TAC[ARITH_RULE`azim_in_fan x (E_SY (vecmats l))
540 =(azim_in_fan x (E_SY (vecmats l)) -pi)+pi`]
541 THEN ASM_SIMP_TAC[SUM_ADD;SUM_CONST;]
542 THEN MP_TAC(ARITH_RULE`2< k==> 2<=k `)
544 THEN MRESA_TAC REAL_OF_NUM_SUB[`2`;`k:num`]
545 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
546 THEN REWRITE_TAC[REAL_ARITH`(sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l)) - pi) +
548 (pi + sol0) * (&k - &2)
549 =(&2 *pi+ sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l)) - pi)) +
550 sol0 * &2 - sol0 * &k`;GSYM sol_local]
551 THEN MATCH_MP_TAC(REAL_ARITH`
552 pi<= sol_local (E_SY (vecmats l)) (F_SY (vecmats (l:real^(M,3)finite_product)))
555 pi + sol0 * &2 - sol0 * &k
558 sol_local (E_SY (vecmats l)) (F_SY (vecmats l)) + sol0 * &2 - sol0 * &k`)
559 THEN ASM_REWRITE_TAC[]
560 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`
561 THEN POP_ASSUM MP_TAC
562 THEN REWRITE_TAC[stable_system;constraint_system]
564 THEN MRESA_TAC REAL_OF_NUM_LE[`k:num`;`6:num`]
565 THEN MATCH_MP_TAC(REAL_ARITH`
566 sol0 * &k<= sol0 * &6
567 /\ #0.92 < pi + sol0 * &2 - sol0 * &6
568 ==> #0.92 < pi + sol0 * &2 - sol0 * &k`)
570 MATCH_MP_TAC REAL_LE_LMUL
571 THEN ASM_REWRITE_TAC[]
572 THEN MATCH_MP_TAC(REAL_ARITH`&0< a==> &0<= a`)
573 THEN REWRITE_TAC[SOL0_POS];
574 REWRITE_TAC[REAL_ARITH`pi + sol0 * &2 - sol0 * &6= pi - sol0 * &4`;]
575 THEN MATCH_MP_TAC(REAL_ARITH`sol0 < #0.551286 /\ #3.14159 < pi ==> #0.92 < pi - sol0 * &4`)
576 THEN REWRITE_TAC[Flyspeck_constants.bounds]]);;
578 let TAU_STAR_POS=prove(`!s:stable_sy l:real^(M,3)finite_product.
579 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
581 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
582 /\ l IN B_SY1 (a_sy s) (b_sy s)
583 ==> &0< tau_star s l`,
584 REWRITE_TAC[tau_star;]
585 THEN REPEAT STRIP_TAC
586 THEN MRESA_TAC (GEN_ALL TAU_FUN_LE)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
587 THEN MRESA_TAC (GEN_ALL D_FUN_LE)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
588 THEN POP_ASSUM MP_TAC
589 THEN POP_ASSUM MP_TAC
590 THEN REAL_ARITH_TAC);;
592 let CIRCULAR_SOL_EQ_2PI=prove(`convex_local_fan (V,E,FF) /\ circular V E
593 ==> sol_local E FF= &2 *pi`,
595 THEN POP_ASSUM MP_TAC
596 THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[convex_local_fan] THEN STRIP_TAC THEN ASSUME_TAC th)
598 THEN REWRITE_TAC[sol_local;REAL_ARITH`A+B=A<=> B= &0`]
599 THEN MATCH_MP_TAC SUM_EQ_0
600 THEN REPEAT STRIP_TAC
601 THEN REWRITE_TAC[REAL_ARITH`A-B= &0<=> A=B`]
602 THEN POP_ASSUM MP_TAC
603 THEN DISCH_THEN(LABEL_TAC "THY")
604 THEN MRESA_TAC (GEN_ALL LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;]
605 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:real^3#real^3`)
606 THEN REMOVE_THEN "THY"MP_TAC
607 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
609 THEN MRESA_TAC(GEN_ALL LOCAL_FAN_IMP_IN_V)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 (FF:real^3#real^3->bool) (FST (x:real^3#real^3))`;`V:real^3->bool`]
610 THEN MRESA_TAC (GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`E:(real^3->bool)->bool`]
611 THEN POP_ASSUM(fun th-> MRESA1_TAC th`FST (x:real^3#real^3)`)
612 THEN MRESA_TAC (GEN_ALL Local_lemmas.KCHMAMG)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;]
613 THEN REMOVE_ASSUM_TAC
614 THEN REMOVE_ASSUM_TAC
615 THEN REMOVE_ASSUM_TAC
616 THEN REMOVE_ASSUM_TAC
617 THEN REMOVE_ASSUM_TAC
618 THEN REMOVE_ASSUM_TAC
619 THEN POP_ASSUM(fun th-> MRESA1_TAC th`FST (x:real^3#real^3)`));;
621 let NOT_CIRCULAR_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
622 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
624 /\ tau_star s l <= &0
625 /\ l IN B_SY1 (a_sy s) (b_sy s)
626 ==> ~(circular (V_SY(vecmats l)) (E_SY(vecmats l)))`,
629 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
630 THEN REPEAT STRIP_TAC
631 THEN POP_ASSUM MP_TAC
632 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)
633 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
634 THEN POP_ASSUM MP_TAC
635 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
636 THEN POP_ASSUM MP_TAC
637 THEN POP_ASSUM MP_TAC
638 THEN POP_ASSUM MP_TAC
639 THEN DISCH_THEN(LABEL_TAC"THY")
640 THEN DISCH_THEN(LABEL_TAC"THY2")
642 THEN POP_ASSUM(fun th-> MP_TAC th
643 THEN REWRITE_TAC[convex_local_fan]
645 THEN POP_ASSUM MP_TAC
646 THEN POP_ASSUM(fun th1-> MP_TAC th1
647 THEN REWRITE_TAC[local_fan]
650 THEN POP_ASSUM MP_TAC
651 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
654 THEN DISCH_THEN(LABEL_TAC"THY1")
657 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
659 THEN MRESA_TAC(GEN_ALL CIRCULAR_SOL_EQ_2PI)[`V_SY(vecmats (l:real^(M,3)finite_product))`;`E_SY(vecmats (l:real^(M,3)finite_product))`;`F_SY(vecmats (l:real^(M,3)finite_product))`]
660 THEN MP_TAC(REAL_ARITH`&0< pi ==> pi <= &2 * pi`)
661 THEN REWRITE_TAC[PI_WORKS]
663 THEN MRESA_TAC (GEN_ALL TAU_STAR_POS)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
664 THEN POP_ASSUM MP_TAC
665 THEN ASM_REWRITE_TAC[REAL_ARITH`~(&0< A) <=> A <= &0`]);;
669 = prove(`!s:stable_sy l:real^(M,3)finite_product.
670 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
671 /\ l IN B_SY1 (a_sy s) (b_sy s)
674 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
675 /\ l IN B_SY1 (a_sy s) (b_sy s)
676 ==> &0< tau_star s l)
678 /\ tau_star s l <= &0
679 ==> ~(circular (V_SY(vecmats l)) (E_SY(vecmats l))))`,
681 THEN MRESA_TAC (GEN_ALL TAU_STAR_POS)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
682 THEN MRESA_TAC (GEN_ALL NOT_CIRCULAR_SY)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]);;