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