src/HOL/NthRoot.thy
changeset 55967 5dadc93ff3df
parent 54413 88a036a95967
child 56371 fb9ae0727548
     1.1 --- a/src/HOL/NthRoot.thy	Fri Mar 07 01:02:21 2014 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Mar 07 12:35:06 2014 +0000
     1.3 @@ -534,14 +534,35 @@
     1.4  
     1.5  subsection {* Square Root of Sum of Squares *}
     1.6  
     1.7 -lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
     1.8 -  by simp (* TODO: delete *)
     1.9 +lemma sum_squares_bound: 
    1.10 +  fixes x:: "'a::linordered_field"
    1.11 +  shows "2*x*y \<le> x^2 + y^2"
    1.12 +proof -
    1.13 +  have "(x-y)^2 = x*x - 2*x*y + y*y"
    1.14 +    by algebra
    1.15 +  then have "0 \<le> x^2 - 2*x*y + y^2"
    1.16 +    by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square)
    1.17 +  then show ?thesis
    1.18 +    by arith
    1.19 +qed
    1.20  
    1.21 -declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
    1.22 +lemma arith_geo_mean: 
    1.23 +  fixes u:: "'a::linordered_field" assumes "u\<^sup>2 = x*y" "x\<ge>0" "y\<ge>0" shows "u \<le> (x + y)/2"
    1.24 +    apply (rule power2_le_imp_le)
    1.25 +    using sum_squares_bound assms
    1.26 +    apply (auto simp: zero_le_mult_iff)
    1.27 +    by (auto simp: algebra_simps power2_eq_square)
    1.28 +
    1.29 +lemma arith_geo_mean_sqrt: 
    1.30 +  fixes x::real assumes "x\<ge>0" "y\<ge>0" shows "sqrt(x*y) \<le> (x + y)/2"
    1.31 +  apply (rule arith_geo_mean)
    1.32 +  using assms
    1.33 +  apply (auto simp: zero_le_mult_iff)
    1.34 +  done
    1.35  
    1.36  lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
    1.37       "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"
    1.38 -  by (simp add: zero_le_mult_iff)
    1.39 +  by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero)
    1.40  
    1.41  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
    1.42       "(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)"