equal
deleted
inserted
replaced
448 text {* TODO: move to NthRoot *} |
448 text {* TODO: move to NthRoot *} |
449 lemma sqrt_add_le_add_sqrt: |
449 lemma sqrt_add_le_add_sqrt: |
450 assumes x: "0 \<le> x" and y: "0 \<le> y" |
450 assumes x: "0 \<le> x" and y: "0 \<le> y" |
451 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
451 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
452 apply (rule power2_le_imp_le) |
452 apply (rule power2_le_imp_le) |
453 apply (simp add: real_sum_squared_expand x y) |
453 apply (simp add: power2_sum x y) |
454 apply (simp add: mult_nonneg_nonneg x y) |
454 apply (simp add: mult_nonneg_nonneg x y) |
455 apply (simp add: x y) |
455 apply (simp add: x y) |
456 done |
456 done |
457 |
457 |
458 lemma bounded_linear_Pair: |
458 lemma bounded_linear_Pair: |