src/HOL/NthRoot.thy
 changeset 55967 5dadc93ff3df parent 54413 88a036a95967 child 56371 fb9ae0727548
```--- a/src/HOL/NthRoot.thy	Fri Mar 07 01:02:21 2014 +0100
+++ b/src/HOL/NthRoot.thy	Fri Mar 07 12:35:06 2014 +0000
@@ -534,14 +534,35 @@

subsection {* Square Root of Sum of Squares *}

-lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
-  by simp (* TODO: delete *)
+lemma sum_squares_bound:
+  fixes x:: "'a::linordered_field"
+  shows "2*x*y \<le> x^2 + y^2"
+proof -
+  have "(x-y)^2 = x*x - 2*x*y + y*y"
+    by algebra
+  then have "0 \<le> x^2 - 2*x*y + y^2"
+  then show ?thesis
+    by arith
+qed

-declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
+lemma arith_geo_mean:
+  fixes u:: "'a::linordered_field" assumes "u\<^sup>2 = x*y" "x\<ge>0" "y\<ge>0" shows "u \<le> (x + y)/2"
+    apply (rule power2_le_imp_le)
+    using sum_squares_bound assms
+    apply (auto simp: zero_le_mult_iff)
+    by (auto simp: algebra_simps power2_eq_square)
+
+lemma arith_geo_mean_sqrt:
+  fixes x::real assumes "x\<ge>0" "y\<ge>0" shows "sqrt(x*y) \<le> (x + y)/2"
+  apply (rule arith_geo_mean)
+  using assms
+  apply (auto simp: zero_le_mult_iff)
+  done

lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
"0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"