(* Title: HOL/ex/SOS.thy
Author: Amine Chaieb, University of Cambridge
Author: Philipp Meyer, TU Muenchen
Examples for Sum_of_Squares.
*)
theory SOS
imports "HOL-Library.Sum_of_Squares"
begin
lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0"
by sos
lemma "a1 \ 0 \ a2 \ 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) \
a1 * a2 - b1 * b2 \<ge> (0::real)"
by sos
lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0"
by sos
lemma "(0::real) \ x \ x \ 1 \ 0 \ y \ y \ 1 \
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"
by sos
lemma "(0::real) \ x \ 0 \ y \ 0 \ z \ x + y + z \ 3 \ x * y + x * z + y * z \ 3 * x * y * z"
by sos
lemma "(x::real)\<^sup>2 + y\<^sup>2 + z\<^sup>2 = 1 \ (x + y + z)\<^sup>2 \ 3"
by sos
lemma "w\<^sup>2 + x\<^sup>2 + y\<^sup>2 + z\<^sup>2 = 1 \ (w + x + y + z)\<^sup>2 \ (4::real)"
by sos
lemma "(x::real) \ 1 \ y \ 1 \ x * y \ x + y - 1"
by sos
lemma "(x::real) > 1 \ y > 1 \ x * y > x + y - 1"
by sos
lemma "\x\ \ 1 \ \64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x\ \ (1::real)"
by sos
text \<open>One component of denominator in dodecahedral example.\<close>
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) \<ge> (0::real)"
by sos
text \<open>Over a larger but simpler interval.\<close>
lemma "(2::real) \ x \ x \ 4 \ 2 \ y \ y \ 4 \ 2 \ z \ z \ 4 \
0 \<le> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)"
by sos
text \<open>We can do 12. I think 12 is a sharp bound; see PP's certificate.\<close>
lemma "2 \ (x::real) \ x \ 4 \ 2 \ y \ y \ 4 \ 2 \ z \ z \ 4 \
12 \<le> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)"
by sos
text \<open>Inequality from sci.math (see "Leon-Sotelo, por favor").\<close>
lemma "0 \ (x::real) \ 0 \ y \ x * y = 1 \ x + y \ x\<^sup>2 + y\<^sup>2"
by sos
lemma "0 \ (x::real) \ 0 \ y \ x * y = 1 \ x * y * (x + y) \ x\<^sup>2 + y\<^sup>2"
by sos
lemma "0 \ (x::real) \ 0 \ y \ x * y * (x + y)\<^sup>2 \ (x\<^sup>2 + y\<^sup>2)\<^sup>2"
by sos
lemma "(0::real) \ a \ 0 \ b \ 0 \ c \ c * (2 * a + b)^3 / 27 \ x \ c * a\<^sup>2 * b \ x"
by sos
lemma "(0::real) < x \ 0 < 1 + x + x\<^sup>2"
by sos
lemma "(0::real) \ x \ 0 < 1 + x + x\<^sup>2"
by sos
lemma "(0::real) < 1 + x\<^sup>2"
by sos
lemma "(0::real) \ 1 + 2 * x + x\<^sup>2"
by sos
lemma "(0::real) < 1 + \x\"
by sos
lemma "(0::real) < 1 + (1 + x)\<^sup>2 * \x\"
by sos
lemma "\(1::real) + x\<^sup>2\ = (1::real) + x\<^sup>2"
by sos
lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0"
by sos
lemma "(0::real) < x \ 1 < y \ y * x \ z \ x < z"
by sos
lemma "(1::real) < x \ x\<^sup>2 < y \ 1 < y"
by sos
lemma "(b::real)\<^sup>2 < 4 * a * c \ a * x\<^sup>2 + b * x + c \ 0"
by sos
lemma "(b::real)\<^sup>2 < 4 * a * c \ a * x\<^sup>2 + b * x + c \ 0"
by sos
lemma "(a::real) * x\<^sup>2 + b * x + c = 0 \ b\<^sup>2 \ 4 * a * c"
by sos
lemma "(0::real) \ b \ 0 \ c \ 0 \ x \ 0 \ y \ x\<^sup>2 = c \ y\<^sup>2 = a\<^sup>2 * c + b \ a * c \ y * x"
by sos
lemma "\x - z\ \ e \ \y - z\ \ e \ 0 \ u \ 0 \ v \ u + v = 1 \ \(u * x + v * y) - z\ \ (e::real)"
by sos
lemma "(x::real) - y - 2 * x^4 = 0 \ 0 \ x \ x \ 2 \ 0 \ y \ y \ 3 \ y\<^sup>2 - 7 * y - 12 * x + 17 \ 0"
oops (*Too hard; left it running for 80 minutes -- LCP*)
lemma "(0::real) \ x \ (1 + x + x\<^sup>2) / (1 + x\<^sup>2) \ 1 + x"
by sos
lemma "(0::real) \ x \ 1 - x \ 1 / (1 + x + x\<^sup>2)"
by sos
lemma "(x::real) \ 1 / 2 \ - x - 2 * x\<^sup>2 \ - x / (1 - x)"
by sos
lemma "4 * r\<^sup>2 = p\<^sup>2 - 4 * q \ r \ (0::real) \ x\<^sup>2 + p * x + q = 0 \
2 * (x::real) = - p + 2 * r \<or> 2 * x = - p - 2 * r"
by sos
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
