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.11 Sekunden
(vorverarbeitet)
¤
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.
