equal
deleted
inserted
replaced
451 text {* TODO: move to NthRoot *} |
451 text {* TODO: move to NthRoot *} |
452 lemma sqrt_add_le_add_sqrt: |
452 lemma sqrt_add_le_add_sqrt: |
453 assumes x: "0 \<le> x" and y: "0 \<le> y" |
453 assumes x: "0 \<le> x" and y: "0 \<le> y" |
454 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
454 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
455 apply (rule power2_le_imp_le) |
455 apply (rule power2_le_imp_le) |
456 apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y) |
456 apply (simp add: real_sum_squared_expand x y) |
457 apply (simp add: mult_nonneg_nonneg x y) |
457 apply (simp add: mult_nonneg_nonneg x y) |
458 apply (simp add: add_nonneg_nonneg x y) |
458 apply (simp add: x y) |
459 done |
459 done |
460 |
460 |
461 lemma bounded_linear_Pair: |
461 lemma bounded_linear_Pair: |
462 assumes f: "bounded_linear f" |
462 assumes f: "bounded_linear f" |
463 assumes g: "bounded_linear g" |
463 assumes g: "bounded_linear g" |