2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Local Fan *)
6 (* Author: Hoang Le Truong *)
8 (* ========================================================================= *)
13 module Pcrttid= struct
28 open Wrgcvdr_cizmrrh;;
36 open Flyspeck_constants;;
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
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)`;;
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)`,
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;]
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`];
63 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
65 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`3`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=3<=> A<=2)`]
69 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
72 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i /\ 1<3`)
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`)
77 THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
78 THEN ASM_REWRITE_TAC[]
81 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
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[]
91 REWRITE_TAC[b_ear0;a_ear0]
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`];
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}`]
100 THEN ASM_REWRITE_TAC[IN_SING;cstab]
102 THEN MATCH_MP_TAC REAL_LE_LSQRT
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]
112 THEN MP_TAC(ARITH_RULE`1<= 3 /\ 1<3`)
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
120 THEN ASM_REWRITE_TAC[ARITH_RULE`0<=1 /\ 1<=2/\ (1 +1 ) MOD 3= 2`];
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`)
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}})`);
130 THEN MATCH_MP_TAC REAL_LE_RSQRT
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]
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]
144 ASM_REWRITE_TAC[h0;cstab]
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)`]
151 THEN MP_TAC(ARITH_RULE`(i =1\/ i=2) /\ (j=1\/ j=2)==> i< 3 /\ j< 3`)
153 THEN MRESA_TAC MOD_LT[`i:num`;`3`]
154 THEN MRESA_TAC MOD_LT[`j:num`;`3`]]);;
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]]);;
165 let tri_sy_tybij = (new_type_definition "tri_sy" ("tri_sy", "tuple_tri_sy")exist_tri_stable);;
168 let k_ts = new_definition `k_ts (s:tri_sy) = FST (tuple_tri_sy s)`;;
170 let d_ts = new_definition `d_ts (s:tri_sy) = (FST (SND (tuple_tri_sy s)))`;;
172 let I_TS = new_definition `I_TS (s:tri_sy) = (FST (SND (SND (tuple_tri_sy s))))`;;
174 let a_ts = new_definition `a_ts (s:tri_sy) = (FST (SND (SND (SND (tuple_tri_sy s)))))`;;
176 let b_ts = new_definition `b_ts (s:tri_sy) = (FST(SND (SND (SND (SND (tuple_tri_sy s)))))) `;;
179 let J_TS = new_definition `J_TS (s:tri_sy) = (FST (SND (SND (SND (SND (SND (tuple_tri_sy s))))))) `;;
181 let f_ts = new_definition `f_ts (s:tri_sy) = (SND(SND (SND (SND (SND (SND (tuple_tri_sy s)))))))`;;
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]);;
193 let augmented_constraint_system1=new_definition
194 `augmented_constraint_system1 (s:stable_sy) I_lo I_str a b m <=>
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
198 /\ (!i j. i IN I_SY s /\ j IN I_SY s ==>
199 a_sy s (i,j)<= a (i,j)
201 /\ b (i,j)<= b_sy s (i,j))`;;
205 let augmented_constraint_system2=new_definition
206 `augmented_constraint_system3 (s:tri_sy) I_lo I_str a b m <=>
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
210 /\ (!i j. i IN I_TS s /\ j IN I_TS s ==>
211 a_ts s (i,j)<= a (i,j)
213 /\ b (i,j)<= b_ts s (i,j))`;;
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)
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
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]
237 THEN POP_ASSUM MP_TAC
238 THEN DISCH_THEN(LABEL_TAC"THY1")
239 THEN DISCH_THEN(LABEL_TAC"THY2")
241 !i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M)
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`)
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`)
258 THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\ SUC(j-1)=j`)
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]
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]
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
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`)
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`)
303 THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\ SUC(j-1)=j`)
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]
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
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;
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];
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]
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[]]);;
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)
353 bounded {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v}`,
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]
360 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
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)
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`)
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`;]]);;
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)
385 compact {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v })
387 stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
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 })`,
393 THEN MESON_TAC[COMPACT_TRI_STABLE;WJSCPRO]);;