1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Definition: enclosed *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
14 The function of 9 variables defined on page 37 of the Kepler Conjecture, DCG vol 36(1), July 2006
15 It is generally typeset as a calligraphic E.
17 It is a quadratic with nonnegative leading coefficient.
22 module type Enclosed_def_type = sig
24 val quad_cross_diag2_x : thm
28 flyspeck_needs "leg/muR_def.hl";;
31 flyspeck_needs "leg/abc_of_quadratic_def.hl";;
32 flyspeck_needs "leg/quadratic_root_plus_def.hl";;
36 module Enclosed : Enclosed_def_type = struct
38 let quadratic_root_plus = Sphere.quadratic_root_plus;;
39 let abc_of_quadratic = Sphere.abc_of_quadratic;;
43 new_definition `enclosed y1 y2 y3 y4 y5 y6 y7 y8 y9 = sqrt
44 (quadratic_root_plus (abc_of_quadratic (muR y1 y2 y3 y4 y5 y6 y7 y8 y9)))`;;
46 let quad_cross_diag2_x = new_definition
47 `quad_cross_diag2_x x1 x2 x3 x4 x5 x6 x7 x8 x9 =
48 enclosed (sqrt x1) (sqrt x5) (sqrt x6) (sqrt x4) (sqrt x2) (sqrt x3) (sqrt x7) (sqrt x8) (sqrt x9)`;;