src/HOL/NthRoot.thy
changeset 55967 5dadc93ff3df
parent 54413 88a036a95967
child 56371 fb9ae0727548
equal deleted inserted replaced
55966:972f0aa7091b 55967:5dadc93ff3df
   532   shows "4 * x\<^sup>2 = (2 * x)\<^sup>2"
   532   shows "4 * x\<^sup>2 = (2 * x)\<^sup>2"
   533 by (simp add: power2_eq_square)
   533 by (simp add: power2_eq_square)
   534 
   534 
   535 subsection {* Square Root of Sum of Squares *}
   535 subsection {* Square Root of Sum of Squares *}
   536 
   536 
   537 lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
   537 lemma sum_squares_bound: 
   538   by simp (* TODO: delete *)
   538   fixes x:: "'a::linordered_field"
   539 
   539   shows "2*x*y \<le> x^2 + y^2"
   540 declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
   540 proof -
       
   541   have "(x-y)^2 = x*x - 2*x*y + y*y"
       
   542     by algebra
       
   543   then have "0 \<le> x^2 - 2*x*y + y^2"
       
   544     by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square)
       
   545   then show ?thesis
       
   546     by arith
       
   547 qed
       
   548 
       
   549 lemma arith_geo_mean: 
       
   550   fixes u:: "'a::linordered_field" assumes "u\<^sup>2 = x*y" "x\<ge>0" "y\<ge>0" shows "u \<le> (x + y)/2"
       
   551     apply (rule power2_le_imp_le)
       
   552     using sum_squares_bound assms
       
   553     apply (auto simp: zero_le_mult_iff)
       
   554     by (auto simp: algebra_simps power2_eq_square)
       
   555 
       
   556 lemma arith_geo_mean_sqrt: 
       
   557   fixes x::real assumes "x\<ge>0" "y\<ge>0" shows "sqrt(x*y) \<le> (x + y)/2"
       
   558   apply (rule arith_geo_mean)
       
   559   using assms
       
   560   apply (auto simp: zero_le_mult_iff)
       
   561   done
   541 
   562 
   542 lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
   563 lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
   543      "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"
   564      "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"
   544   by (simp add: zero_le_mult_iff)
   565   by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero)
   545 
   566 
   546 lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
   567 lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
   547      "(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)"
   568      "(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)"
   548   by (simp add: zero_le_mult_iff)
   569   by (simp add: zero_le_mult_iff)
   549 
   570