Update from HH
[Flyspeck/.git] / legacy / oldvolume / ch_volume / volume.hl
1 (* summary of the volume chapter *)
2
3 (*
4 Known issues:
5
6 -- TXIWYHI has quantifiers in the wrong order. It should be ?C. !r.
7
8 -- JJFHOIW_t not formalized.
9
10 -- ATOAPUN missing the additivity of volumes
11
12 -- PUACSHX (Project Issue 5), mismatch between volume_prop vol and volume_props.
13   This affects all theorems with assumption `volume_prop vol`
14
15 -- NULLSET and vol are pretty printed versions of negligible and measure, specialized to R^3,
16     so searches don't show all the general theorems
17 *)
18
19
20
21 let OWCZKJR = NULLSET_RULES;;
22
23 (* more NULLSET props *)
24 let NULLSET_INTER = prove(`!s t. NULLSET s /\ NULLSET t ==>
25    NULLSET (s INTER t)`,
26   SIMP_TAC[NEGLIGIBLE_INTER]);;
27  
28 let NULLSET_SUBSET = prove(`!s t. NULLSET s /\ t SUBSET s ==> NULLSET t`,
29   MESON_TAC[NEGLIGIBLE_SUBSET]);;
30
31 let NULLSET_DIFF = prove(`!s t. NULLSET s ==> NULLSET(s DIFF t)`,
32   SIMP_TAC[NEGLIGIBLE_DIFF]);;
33
34 let NUKRQDI = MEASURABLE_RULES;;
35
36 (* Background in Measure *)
37
38
39 let ATOAPUN = volume_props;;  
40
41 (* volume_props doesn't give additivity of measure.  Here it is. *)
42
43 let VOL_DISJOINT_UNION = prove(` !s t. 
44            measurable s /\ measurable t /\ DISJOINT s t
45            ==> vol (s UNION t) = vol s + vol t`,
46         SIMP_TAC[MEASURE_DISJOINT_UNION]                      );;
47
48 let VOL_NULLSET_UNION= prove(` !s t.
49            measurable s /\ measurable t /\ NULLSET (s INTER t)
50            ==> vol (s UNION t) = vol s + vol t`,
51       SIMP_TAC[MEASURE_NEGLIGIBLE_UNION]                               );;
52
53 let VOL_UNION_LE=prove(` !s t.
54            measurable s /\ measurable t
55            ==> vol (s UNION t) <= vol s + vol t`,
56                 SIMP_TAC[MEASURE_UNION_LE]      );;
57
58 (* unwedged versions *)
59
60 let ATOAPUN1 = VOLUME_CONIC_CAP;;
61 let ATOAPUN2 = VOLUME_CONIC_CAP_STRONG;;
62 let ATOAPUN3 = VOLUME_BALL;;
63 let ATOAPUN4 = VOLUME_FRUSTT;;
64 let ATOAPUN5 = VOLUME_FRUSTT_STRONG;;
65
66 (* Primitive Volume *)
67
68 (* radial set *)
69
70 let VSPMVNR1 = ball;;
71 let VSPMVNR2 = cball;;
72 let VSPMVNR = [VSPMVNR1;VSPMVNR2];;
73
74 (* duplicate definition : normball = ball *)
75
76 let QPHVSMZ1 = radial;;
77 let QPHVSMZ2 = eventually_radial;;
78 let QPHVSMZ3 = radial_norm;;
79 let QPHVSMZ4 = eventually_radial_norm;;
80 let QPHVSMZ5 = NORMBALL_BALL;;
81 let  QPHVSMZ = [ QPHVSMZ1; QPHVSMZ2; QPHVSMZ3;QPHVSMZ4;QPHVSMZ5];;
82
83  let KODOBRF = inter_radial;;
84
85  let LBWOPAH = "not found";;
86
87 let PUACSHX = lemma_r_r'_fix;;   
88
89 let MASYUQQ = sol;;  
90
91
92 (* to here *)
93 (* 2.2.1 wedge *)
94 let wedge = wedge;;
95
96 (* Lemma 2.4 [VICUATE] need to check - found in Multivariate/flyspeck.ml *)
97 let VICUATE = WEDGE_LUNE;;
98
99 (* Definition 2.4 Solid Triangle *)
100 let solid_triangle = solid_triangle;;
101
102 (* Definition 2.5 Conic Cap *)
103 let conic_cap = conic_cap;;
104
105 (* Definition 2.6 rcone label{def:p:rcone}
106    - a collection of different rcones  label{def:p:rcone} *)
107 let rcone_gt = rcone_gt;;
108 let rcone_ge = rcone_ge;;
109 (* < version from the definition wasn't found in flyspeck.ml *)
110 let rcone_eq = rcone_eq;;
111
112 (* Definition 2.7 frustum *)
113 let frustum = frustum;;
114
115 (* Definition 2.8 tetrahedron *)
116 let tetrahedron = conv0;;
117
118 (* Definition 2.9 Primitive label{def:primitive} *)
119 let primitive = primitive;;
120
121 (* volume calculations *)
122
123 (* Lemma 2.5 [PAZNHPZ] label{lemma:prim-volume} - found in Multivariate/flyspeck.ml*)
124 (* 
125
126 VOLUME_SOLID_TRIANGLE, VOLUME_CONIC_CAP, VOLUME_FRUSTT, VOLUME_OF_TETRAHEDRON, vol_rect, VOLUME_BALL_WEDGE combine to 
127  form the lemma *)
128
129 (* Lemma 2.6 [DFNVMFM] label{lemma:wedge-vol} need to check - found in Multivariate/flyspeck.ml *)
130 let DFNVMFM = VOLUME_BALL_WEDGE;;
131
132 (* Lemma 2.7 [FMSWMVO] label{lemma:wedge-sol}*)
133 (* not found *)
134
135 (* Lemma 2.8 [FUPXNLC] label{lemma:prim-sol} *)
136 (* not found *)
137
138 (* Lemma 2.9 [WFFVGVF] *)
139 (* not found *)
140  
141 (* Lemma 2.10 [CZOQFNL] label{lemma:wedge:sol}  not sure if this one is correct...found in Multivariate/flyspeck.ml *)
142 let CZOQFNL = WEDGE_LUNE_GT;;
143
144 (* Lemma 2.11 [OXQZBJG] *)
145 (* not formalized *)
146
147 (* Definition 2.10 (orthosimplex, orth)  label{def:ortho} *)
148 (*found in sphere.hl *)
149  let ortho0 = ortho0;;
150
151 (* Definition 2.11 (Rogers simplex, rog) label{def:rog} *)
152 (*both found in sphere.hl *)
153 (*
154  let rogers0 = rogers0;;
155  let rogers = rogers;;  
156 *)
157
158 (* Lemma 2.12 [XQBOVQF] *)
159 (* not formalized *)
160
161 (* Definition 2.12 (circumradius) label{def:etaV} *)
162 (* found in sphere.hl*)
163  let radV = radV;;
164
165 (* Definition 2.13 (abc parameter) label{def:abc} *)
166 (*found in sphere.hl *)
167  let abc_parameter = abc_param;; 
168
169
170 (* Lemma 2.13 [JJFHOIW] label{lemma:rog:abc} *)
171 (* didn't find an actual lemma for this, but I found the equations from the lemma in sphere.hl *)
172  let JJFHOIW1 = volR;;
173  let JJFHOIW2 = solR;;
174  let JJFHOIW3 = dihR;;
175  let JJFHOIW = "not found";;
176
177  let orthosimplex = define `orthosimplex (v0:real^N) e1 e2 e3 a b c = 
178    let v1 = v0 + a % e1 in
179    let v2 = v1 + sqrt(b pow 2 - a pow 2) % e2 in
180    let v3 = v2 + sqrt(c pow 2 - b pow 2) % e3 in
181    conv0 {v0, v1, v2, v3}`;;
182
183  let JJFHOIW_t = `!v0 e1 e2 e3 a b c.
184    (orthonormal e1 e2 e3 /\ &0 < a /\ a <= b /\ b <= c) ==>
185
186    (vol(orthosimplex v0 e1 e2 e3 a b c) = volR a b c)/\
187    (sol (orthosimplex v0 e1 e2 e3 a b c) v0 = solR a b c) /\
188    (dih(orthosimplex v0 e1 e2 e3 a b c) = dihR a b c)`;;
189
190 (* Finiteness and Volume *)
191  type_of `orthosimplex`;;
192  type_of `orthonormal`;;
193  type_of `sol`;;
194
195 let  WQZISRI =  WQZISRI;;   
196
197 let PWVIIOL = PWVIIOL;;  
198
199 (* lattice shell *)
200 let TXIWYHI = TXIWYHI;;   
201