7 |
7 |
8 theory SOS_Cert |
8 theory SOS_Cert |
9 imports "~~/src/HOL/Library/Sum_of_Squares" |
9 imports "~~/src/HOL/Library/Sum_of_Squares" |
10 begin |
10 begin |
11 |
11 |
12 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" |
12 lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<Longrightarrow> a < 0" |
13 by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") |
13 by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") |
14 |
14 |
15 lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" |
15 lemma "a1 \<ge> 0 \<and> a2 \<ge> 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (a1 * b1 + a2 * b2 = 0) \<longrightarrow> |
|
16 a1 * a2 - b1 * b2 \<ge> (0::real)" |
16 by (sos "(((A<0 * R<1) + (([~1/2*a1*b2 + ~1/2*a2*b1] * A=0) + (([~1/2*a1*a2 + 1/2*b1*b2] * A=1) + (((A<0 * R<1) * ((R<1/2 * [b2]^2) + (R<1/2 * [b1]^2))) + ((A<=0 * (A<=1 * R<1)) * ((R<1/2 * [b2]^2) + ((R<1/2 * [b1]^2) + ((R<1/2 * [a2]^2) + (R<1/2 * [a1]^2))))))))))") |
17 by (sos "(((A<0 * R<1) + (([~1/2*a1*b2 + ~1/2*a2*b1] * A=0) + (([~1/2*a1*a2 + 1/2*b1*b2] * A=1) + (((A<0 * R<1) * ((R<1/2 * [b2]^2) + (R<1/2 * [b1]^2))) + ((A<=0 * (A<=1 * R<1)) * ((R<1/2 * [b2]^2) + ((R<1/2 * [b1]^2) + ((R<1/2 * [a2]^2) + (R<1/2 * [a1]^2))))))))))") |
17 |
18 |
18 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" |
19 lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0" |
19 by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") |
20 by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") |
20 |
21 |
21 lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" |
22 lemma "(0::real) \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> |
|
23 x\<^sup>2 + y\<^sup>2 < 1 \<or> (x - 1)\<^sup>2 + y\<^sup>2 < 1 \<or> x\<^sup>2 + (y - 1)\<^sup>2 < 1 \<or> (x - 1)\<^sup>2 + (y - 1)\<^sup>2 < 1" |
22 by (sos "((R<1 + (((A<=3 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=7 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=5 * R<1)) * (R<1 * [1]^2)))))))") |
24 by (sos "((R<1 + (((A<=3 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=7 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=5 * R<1)) * (R<1 * [1]^2)))))))") |
23 |
25 |
24 lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" |
26 lemma "(0::real) \<le> x \<and> 0 \<le> y \<and> 0 \<le> z \<and> x + y + z \<le> 3 \<longrightarrow> x * y + x * z + y * z \<ge> 3 * x * y * z" |
25 by (sos "(((A<0 * R<1) + (((A<0 * R<1) * (R<1/2 * [1]^2)) + (((A<=2 * R<1) * (R<1/2 * [~1*x + y]^2)) + (((A<=1 * R<1) * (R<1/2 * [~1*x + z]^2)) + (((A<=1 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + (((A<=0 * R<1) * (R<1/2 * [~1*y + z]^2)) + (((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=1 * (A<=3 * R<1))) * (R<1/2 * [1]^2))))))))))") |
27 by (sos "(((A<0 * R<1) + (((A<0 * R<1) * (R<1/2 * [1]^2)) + (((A<=2 * R<1) * (R<1/2 * [~1*x + y]^2)) + (((A<=1 * R<1) * (R<1/2 * [~1*x + z]^2)) + (((A<=1 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + (((A<=0 * R<1) * (R<1/2 * [~1*y + z]^2)) + (((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=1 * (A<=3 * R<1))) * (R<1/2 * [1]^2))))))))))") |
26 |
28 |
27 lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" |
29 lemma "(x::real)\<^sup>2 + y\<^sup>2 + z\<^sup>2 = 1 \<longrightarrow> (x + y + z)\<^sup>2 \<le> 3" |
28 by (sos "(((A<0 * R<1) + (([~3] * A=0) + (R<1 * ((R<2 * [~1/2*x + ~1/2*y + z]^2) + (R<3/2 * [~1*x + y]^2))))))") |
30 by (sos "(((A<0 * R<1) + (([~3] * A=0) + (R<1 * ((R<2 * [~1/2*x + ~1/2*y + z]^2) + (R<3/2 * [~1*x + y]^2))))))") |
29 |
31 |
30 lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" |
32 lemma "w\<^sup>2 + x\<^sup>2 + y\<^sup>2 + z\<^sup>2 = 1 \<longrightarrow> (w + x + y + z)\<^sup>2 \<le> (4::real)" |
31 by (sos "(((A<0 * R<1) + (([~4] * A=0) + (R<1 * ((R<3 * [~1/3*w + ~1/3*x + ~1/3*y + z]^2) + ((R<8/3 * [~1/2*w + ~1/2*x + y]^2) + (R<2 * [~1*w + x]^2)))))))") |
33 by (sos "(((A<0 * R<1) + (([~4] * A=0) + (R<1 * ((R<3 * [~1/3*w + ~1/3*x + ~1/3*y + z]^2) + ((R<8/3 * [~1/2*w + ~1/2*x + y]^2) + (R<2 * [~1*w + x]^2)))))))") |
32 |
34 |
33 lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" |
35 lemma "(x::real) \<ge> 1 \<and> y \<ge> 1 \<longrightarrow> x * y \<ge> x + y - 1" |
34 by (sos "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))") |
36 by (sos "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))") |
35 |
37 |
36 lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" |
38 lemma "(x::real) > 1 \<and> y > 1 \<longrightarrow> x * y > x + y - 1" |
37 by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") |
39 by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") |
38 |
40 |
39 lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" |
41 lemma "\<bar>x\<bar> \<le> 1 \<longrightarrow> \<bar>64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x\<bar> \<le> (1::real)" |
40 by (sos "((((A<0 * R<1) + ((A<=1 * R<1) * (R<1 * [~8*x^3 + ~4*x^2 + 4*x + 1]^2)))) & ((((A<0 * A<1) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [8*x^3 + ~4*x^2 + ~4*x + 1]^2)))))") |
42 by (sos "((((A<0 * R<1) + ((A<=1 * R<1) * (R<1 * [~8*x^3 + ~4*x^2 + 4*x + 1]^2)))) & ((((A<0 * A<1) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [8*x^3 + ~4*x^2 + ~4*x + 1]^2)))))") |
41 |
43 |
42 |
44 |
43 text \<open>One component of denominator in dodecahedral example.\<close> |
45 text \<open>One component of denominator in dodecahedral example.\<close> |
44 |
46 |
45 lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" |
47 lemma "2 \<le> x \<and> x \<le> 125841 / 50000 \<and> 2 \<le> y \<and> y \<le> 125841 / 50000 \<and> 2 \<le> z \<and> z \<le> 125841 / 50000 \<longrightarrow> |
|
48 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) \<ge> (0::real)" |
46 by (sos "(((A<0 * R<1) + ((R<1 * ((R<5749028157/5000000000 * [~25000/222477*x + ~25000/222477*y + ~25000/222477*z + 1]^2) + ((R<864067/1779816 * [419113/864067*x + 419113/864067*y + z]^2) + ((R<320795/864067 * [419113/1283180*x + y]^2) + (R<1702293/5132720 * [x]^2))))) + (((A<=4 * (A<=5 * R<1)) * (R<3/2 * [1]^2)) + (((A<=3 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<3/2 * [1]^2)) + (((A<=1 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1/2 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<3/2 * [1]^2)))))))))))))") |
49 by (sos "(((A<0 * R<1) + ((R<1 * ((R<5749028157/5000000000 * [~25000/222477*x + ~25000/222477*y + ~25000/222477*z + 1]^2) + ((R<864067/1779816 * [419113/864067*x + 419113/864067*y + z]^2) + ((R<320795/864067 * [419113/1283180*x + y]^2) + (R<1702293/5132720 * [x]^2))))) + (((A<=4 * (A<=5 * R<1)) * (R<3/2 * [1]^2)) + (((A<=3 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<3/2 * [1]^2)) + (((A<=1 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1/2 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<3/2 * [1]^2)))))))))))))") |
47 |
50 |
48 |
51 |
49 text \<open>Over a larger but simpler interval.\<close> |
52 text \<open>Over a larger but simpler interval.\<close> |
50 |
53 |
51 lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" |
54 lemma "(2::real) \<le> x \<and> x \<le> 4 \<and> 2 \<le> y \<and> y \<le> 4 \<and> 2 \<le> z \<and> z \<le> 4 \<longrightarrow> |
|
55 0 \<le> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" |
52 by (sos "((R<1 + ((R<1 * ((R<1 * [~1/6*x + ~1/6*y + ~1/6*z + 1]^2) + ((R<1/18 * [~1/2*x + ~1/2*y + z]^2) + (R<1/24 * [~1*x + y]^2)))) + (((A<0 * R<1) * (R<1/12 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1/6 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1/6 * [1]^2)))))))))))") |
56 by (sos "((R<1 + ((R<1 * ((R<1 * [~1/6*x + ~1/6*y + ~1/6*z + 1]^2) + ((R<1/18 * [~1/2*x + ~1/2*y + z]^2) + (R<1/24 * [~1*x + y]^2)))) + (((A<0 * R<1) * (R<1/12 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1/6 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1/6 * [1]^2)))))))))))") |
53 |
57 |
54 |
58 |
55 text \<open>We can do 12. I think 12 is a sharp bound; see PP's certificate.\<close> |
59 text \<open>We can do 12. I think 12 is a sharp bound; see PP's certificate.\<close> |
56 |
60 |
57 lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" |
61 lemma "2 \<le> (x::real) \<and> x \<le> 4 \<and> 2 \<le> y \<and> y \<le> 4 \<and> 2 \<le> z \<and> z \<le> 4 \<longrightarrow> |
|
62 12 \<le> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" |
58 by (sos "(((A<0 * R<1) + (((A<=4 * R<1) * (R<2/3 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1 * [1]^2)) + (((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * R<1) * (R<2/3 * [1]^2)) + (((A<=2 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * R<1) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=0 * (A<=3 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<8/3 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))))))))))))))))") |
63 by (sos "(((A<0 * R<1) + (((A<=4 * R<1) * (R<2/3 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1 * [1]^2)) + (((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * R<1) * (R<2/3 * [1]^2)) + (((A<=2 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * R<1) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=0 * (A<=3 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<8/3 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))))))))))))))))") |
59 |
64 |
60 |
65 |
61 text \<open>Inequality from sci.math (see "Leon-Sotelo, por favor").\<close> |
66 text \<open>Inequality from sci.math (see "Leon-Sotelo, por favor").\<close> |
62 |
67 |
63 lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" |
68 lemma "0 \<le> (x::real) \<and> 0 \<le> y \<and> x * y = 1 \<longrightarrow> x + y \<le> x\<^sup>2 + y\<^sup>2" |
64 by (sos "(((A<0 * R<1) + (([1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") |
69 by (sos "(((A<0 * R<1) + (([1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") |
65 |
70 |
66 lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" |
71 lemma "0 \<le> (x::real) \<and> 0 \<le> y \<and> x * y = 1 \<longrightarrow> x * y * (x + y) \<le> x\<^sup>2 + y\<^sup>2" |
67 by (sos "(((A<0 * R<1) + (([~1*x + ~1*y + 1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") |
72 by (sos "(((A<0 * R<1) + (([~1*x + ~1*y + 1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") |
68 |
73 |
69 lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" |
74 lemma "0 \<le> (x::real) \<and> 0 \<le> y \<longrightarrow> x * y * (x + y)\<^sup>2 \<le> (x\<^sup>2 + y\<^sup>2)\<^sup>2" |
70 by (sos "(((A<0 * R<1) + (R<1 * ((R<1 * [~1/2*x^2 + y^2 + ~1/2*x*y]^2) + (R<3/4 * [~1*x^2 + x*y]^2)))))") |
75 by (sos "(((A<0 * R<1) + (R<1 * ((R<1 * [~1/2*x^2 + y^2 + ~1/2*x*y]^2) + (R<3/4 * [~1*x^2 + x*y]^2)))))") |
71 |
76 |
72 lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \<longrightarrow> c * a^2 * b <= x" |
77 lemma "(0::real) \<le> a \<and> 0 \<le> b \<and> 0 \<le> c \<and> c * (2 * a + b)^3 / 27 \<le> x \<longrightarrow> c * a\<^sup>2 * b \<le> x" |
73 by (sos "(((A<0 * R<1) + (((A<=3 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/27 * [~1*a + b]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<8/27 * [~1*a + b]^2))))))") |
78 by (sos "(((A<0 * R<1) + (((A<=3 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/27 * [~1*a + b]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<8/27 * [~1*a + b]^2))))))") |
74 |
79 |
75 lemma "(0::real) < x --> 0 < 1 + x + x^2" |
80 lemma "(0::real) < x \<longrightarrow> 0 < 1 + x + x\<^sup>2" |
76 by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") |
81 by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") |
77 |
82 |
78 lemma "(0::real) <= x --> 0 < 1 + x + x^2" |
83 lemma "(0::real) \<le> x \<longrightarrow> 0 < 1 + x + x\<^sup>2" |
79 by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") |
84 by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") |
80 |
85 |
81 lemma "(0::real) < 1 + x^2" |
86 lemma "(0::real) < 1 + x\<^sup>2" |
82 by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") |
87 by (sos "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") |
83 |
88 |
84 lemma "(0::real) <= 1 + 2 * x + x^2" |
89 lemma "(0::real) \<le> 1 + 2 * x + x\<^sup>2" |
85 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))") |
90 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))") |
86 |
91 |
87 lemma "(0::real) < 1 + abs x" |
92 lemma "(0::real) < 1 + \<bar>x\<bar>" |
88 by (sos "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))") |
93 by (sos "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))") |
89 |
94 |
90 lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" |
95 lemma "(0::real) < 1 + (1 + x)\<^sup>2 * \<bar>x\<bar>" |
91 by (sos "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") |
96 by (sos "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") |
92 |
97 |
93 |
98 |
94 lemma "abs ((1::real) + x^2) = (1::real) + x^2" |
99 lemma "\<bar>(1::real) + x\<^sup>2\<bar> = (1::real) + x\<^sup>2" |
95 by (sos "(() & (((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<1 * R<1) * (R<1/2 * [1]^2))))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2)))))))") |
100 by (sos "(() & (((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<1 * R<1) * (R<1/2 * [1]^2))))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2)))))))") |
|
101 |
96 lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0" |
102 lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0" |
97 by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") |
103 by (sos "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") |
98 |
104 |
99 lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" |
105 lemma "(0::real) < x \<longrightarrow> 1 < y \<longrightarrow> y * x \<le> z \<longrightarrow> x < z" |
100 by (sos "((((A<0 * A<1) * R<1) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") |
106 by (sos "((((A<0 * A<1) * R<1) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") |
101 lemma "(1::real) < x --> x^2 < y --> 1 < y" |
107 |
|
108 lemma "(1::real) < x \<longrightarrow> x\<^sup>2 < y \<longrightarrow> 1 < y" |
102 by (sos "((((A<0 * A<1) * R<1) + ((R<1 * ((R<1/10 * [~2*x + y + 1]^2) + (R<1/10 * [~1*x + y]^2))) + (((A<1 * R<1) * (R<1/2 * [1]^2)) + (((A<0 * R<1) * (R<1 * [x]^2)) + (((A<=0 * R<1) * ((R<1/10 * [x + 1]^2) + (R<1/10 * [x]^2))) + (((A<=0 * (A<1 * R<1)) * (R<1/5 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/5 * [1]^2)))))))))") |
109 by (sos "((((A<0 * A<1) * R<1) + ((R<1 * ((R<1/10 * [~2*x + y + 1]^2) + (R<1/10 * [~1*x + y]^2))) + (((A<1 * R<1) * (R<1/2 * [1]^2)) + (((A<0 * R<1) * (R<1 * [x]^2)) + (((A<=0 * R<1) * ((R<1/10 * [x + 1]^2) + (R<1/10 * [x]^2))) + (((A<=0 * (A<1 * R<1)) * (R<1/5 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/5 * [1]^2)))))))))") |
103 lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" |
110 |
|
111 lemma "(b::real)\<^sup>2 < 4 * a * c \<longrightarrow> a * x\<^sup>2 + b * x + c \<noteq> 0" |
104 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") |
112 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") |
105 lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" |
113 |
|
114 lemma "(b::real)\<^sup>2 < 4 * a * c \<longrightarrow> a * x^2 + b * x + c \<noteq> 0" |
106 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") |
115 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") |
107 lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" |
116 |
|
117 lemma "(a::real) * x\<^sup>2 + b * x + c = 0 \<longrightarrow> b\<^sup>2 \<ge> 4 * a * c" |
108 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") |
118 by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") |
109 lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" |
119 |
|
120 lemma "(0::real) \<le> b \<and> 0 \<le> c \<and> 0 \<le> x \<and> 0 \<le> y \<and> x\<^sup>2 = c \<and> y\<^sup>2 = a\<^sup>2 * c + b \<longrightarrow> a * c \<le> y * x" |
110 by (sos "(((A<0 * (A<0 * R<1)) + (((A<=2 * (A<=3 * (A<0 * R<1))) * (R<2 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2)))))") |
121 by (sos "(((A<0 * (A<0 * R<1)) + (((A<=2 * (A<=3 * (A<0 * R<1))) * (R<2 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2)))))") |
111 lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)" |
122 |
|
123 lemma "\<bar>x - z\<bar> \<le> e \<and> \<bar>y - z\<bar> \<le> e \<and> 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1 \<longrightarrow> \<bar>(u * x + v * y) - z\<bar> \<le> (e::real)" |
112 by (sos "((((A<0 * R<1) + (((A<=3 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=1 * (A<=5 * R<1)) * (R<1 * [1]^2))))) & ((((A<0 * A<1) * R<1) + (((A<=3 * (A<=5 * (A<0 * R<1))) * (R<1 * [1]^2)) + ((A<=1 * (A<=4 * (A<0 * R<1))) * (R<1 * [1]^2))))))") |
124 by (sos "((((A<0 * R<1) + (((A<=3 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=1 * (A<=5 * R<1)) * (R<1 * [1]^2))))) & ((((A<0 * A<1) * R<1) + (((A<=3 * (A<=5 * (A<0 * R<1))) * (R<1 * [1]^2)) + ((A<=1 * (A<=4 * (A<0 * R<1))) * (R<1 * [1]^2))))))") |
113 |
125 |
114 |
126 |
115 (* lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*) |
127 lemma "(x::real) - y - 2 * x^4 = 0 \<and> 0 \<le> x \<and> x \<le> 2 \<and> 0 \<le> y \<and> y \<le> 3 \<longrightarrow> y\<^sup>2 - 7 * y - 12 * x + 17 \<ge> 0" |
|
128 oops (*Too hard?*) |
116 |
129 |
117 lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x" |
130 lemma "(0::real) \<le> x \<longrightarrow> (1 + x + x\<^sup>2) / (1 + x\<^sup>2) \<le> 1 + x" |
118 by (sos "(((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2))))))") |
131 by (sos "(((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2))))))") |
119 |
132 |
120 lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)" |
133 lemma "(0::real) \<le> x \<longrightarrow> 1 - x \<le> 1 / (1 + x + x\<^sup>2)" |
121 by (sos "(((R<1 + (([~4/3] * A=0) + ((R<1 * ((R<1/3 * [3/2*x + 1]^2) + (R<7/12 * [x]^2))) + ((A<=0 * R<1) * (R<1/3 * [1]^2)))))) & (((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))))") |
134 by (sos "(((R<1 + (([~4/3] * A=0) + ((R<1 * ((R<1/3 * [3/2*x + 1]^2) + (R<7/12 * [x]^2))) + ((A<=0 * R<1) * (R<1/3 * [1]^2)))))) & (((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))))") |
122 |
135 |
123 lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)" |
136 lemma "(x::real) \<le> 1 / 2 \<longrightarrow> - x - 2 * x\<^sup>2 \<le> - x / (1 - x)" |
124 by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))") |
137 by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))") |
125 |
138 |
126 lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" |
139 lemma "4 * r\<^sup>2 = p\<^sup>2 - 4 * q \<and> r \<ge> (0::real) \<and> x\<^sup>2 + p * x + q = 0 \<longrightarrow> 2 * (x::real) = - p + 2 * r \<or> 2 * x = - p - 2 * r" |
127 by (sos "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))") |
140 by (sos "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))") |
128 |
141 |
129 end |
142 end |
130 |
|