src/HOL/NthRoot.thy
 changeset 55967 5dadc93ff3df parent 54413 88a036a95967 child 56371 fb9ae0727548
equal inserted replaced
`   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 `