1 (* summary of the volume chapter *)
6 -- TXIWYHI has quantifiers in the wrong order. It should be ?C. !r.
8 -- JJFHOIW_t not formalized.
10 -- ATOAPUN missing the additivity of volumes
12 -- PUACSHX (Project Issue 5), mismatch between volume_prop vol and volume_props.
13 This affects all theorems with assumption `volume_prop vol`
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
21 let OWCZKJR = NULLSET_RULES;;
23 (* more NULLSET props *)
24 let NULLSET_INTER = prove(`!s t. NULLSET s /\ NULLSET t ==>
26 SIMP_TAC[NEGLIGIBLE_INTER]);;
28 let NULLSET_SUBSET = prove(`!s t. NULLSET s /\ t SUBSET s ==> NULLSET t`,
29 MESON_TAC[NEGLIGIBLE_SUBSET]);;
31 let NULLSET_DIFF = prove(`!s t. NULLSET s ==> NULLSET(s DIFF t)`,
32 SIMP_TAC[NEGLIGIBLE_DIFF]);;
34 let NUKRQDI = MEASURABLE_RULES;;
36 (* Background in Measure *)
39 let ATOAPUN = volume_props;;
41 (* volume_props doesn't give additivity of measure. Here it is. *)
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] );;
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] );;
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] );;
58 (* unwedged versions *)
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;;
66 (* Primitive Volume *)
71 let VSPMVNR2 = cball;;
72 let VSPMVNR = [VSPMVNR1;VSPMVNR2];;
74 (* duplicate definition : normball = ball *)
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];;
83 let KODOBRF = inter_radial;;
85 let LBWOPAH = "not found";;
87 let PUACSHX = lemma_r_r'_fix;;
96 (* Lemma 2.4 [VICUATE] need to check - found in Multivariate/flyspeck.ml *)
97 let VICUATE = WEDGE_LUNE;;
99 (* Definition 2.4 Solid Triangle *)
100 let solid_triangle = solid_triangle;;
102 (* Definition 2.5 Conic Cap *)
103 let conic_cap = conic_cap;;
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;;
112 (* Definition 2.7 frustum *)
113 let frustum = frustum;;
115 (* Definition 2.8 tetrahedron *)
116 let tetrahedron = conv0;;
118 (* Definition 2.9 Primitive label{def:primitive} *)
119 let primitive = primitive;;
121 (* volume calculations *)
123 (* Lemma 2.5 [PAZNHPZ] label{lemma:prim-volume} - found in Multivariate/flyspeck.ml*)
126 VOLUME_SOLID_TRIANGLE, VOLUME_CONIC_CAP, VOLUME_FRUSTT, VOLUME_OF_TETRAHEDRON, vol_rect, VOLUME_BALL_WEDGE combine to
129 (* Lemma 2.6 [DFNVMFM] label{lemma:wedge-vol} need to check - found in Multivariate/flyspeck.ml *)
130 let DFNVMFM = VOLUME_BALL_WEDGE;;
132 (* Lemma 2.7 [FMSWMVO] label{lemma:wedge-sol}*)
135 (* Lemma 2.8 [FUPXNLC] label{lemma:prim-sol} *)
138 (* Lemma 2.9 [WFFVGVF] *)
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;;
144 (* Lemma 2.11 [OXQZBJG] *)
147 (* Definition 2.10 (orthosimplex, orth) label{def:ortho} *)
148 (*found in sphere.hl *)
149 let ortho0 = ortho0;;
151 (* Definition 2.11 (Rogers simplex, rog) label{def:rog} *)
152 (*both found in sphere.hl *)
154 let rogers0 = rogers0;;
155 let rogers = rogers;;
158 (* Lemma 2.12 [XQBOVQF] *)
161 (* Definition 2.12 (circumradius) label{def:etaV} *)
162 (* found in sphere.hl*)
165 (* Definition 2.13 (abc parameter) label{def:abc} *)
166 (*found in sphere.hl *)
167 let abc_parameter = abc_param;;
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";;
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}`;;
183 let JJFHOIW_t = `!v0 e1 e2 e3 a b c.
184 (orthonormal e1 e2 e3 /\ &0 < a /\ a <= b /\ b <= c) ==>
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)`;;
190 (* Finiteness and Volume *)
191 type_of `orthosimplex`;;
192 type_of `orthonormal`;;
195 let WQZISRI = WQZISRI;;
197 let PWVIIOL = PWVIIOL;;
200 let TXIWYHI = TXIWYHI;;