diff -r 972f0aa7091b -r 5dadc93ff3df src/HOL/NthRoot.thy --- 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 \ sqrt (x\<^sup>2 + y\<^sup>2)" - by simp (* TODO: delete *) +lemma sum_squares_bound: + fixes x:: "'a::linordered_field" + shows "2*x*y \ x^2 + y^2" +proof - + have "(x-y)^2 = x*x - 2*x*y + y*y" + by algebra + then have "0 \ x^2 - 2*x*y + y^2" + by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square) + 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\0" "y\0" shows "u \ (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\0" "y\0" shows "sqrt(x*y) \ (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 \ sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))" - by (simp add: zero_le_mult_iff) + by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero) lemma real_sqrt_sum_squares_mult_squared_eq [simp]: "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)"