src/HOL/Library/Euclidean_Space.thy
changeset 31399 d9769f093160
parent 31398 b67a3ac4882d
child 31406 e23dd3aac0fb
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 19:42:44 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 20:10:56 2009 -0700
     1.3 @@ -2746,17 +2746,19 @@
     1.4  lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"
     1.5    by (simp add: dot_def setsum_UNIV_sum pastecart_def)
     1.6  
     1.7 -lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ 'm::finite) + norm(y::real^'n::finite)"
     1.8 -  unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
     1.9 -  apply (rule power2_le_imp_le)
    1.10 -  apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])
    1.11 -  apply (auto simp add: power2_eq_square ring_simps)
    1.12 -  apply (simp add: power2_eq_square[symmetric])
    1.13 -  apply (rule mult_nonneg_nonneg)
    1.14 -  apply (simp_all add: real_sqrt_pow2[OF dot_pos_le])
    1.15 -  apply (rule add_nonneg_nonneg)
    1.16 -  apply (simp_all add: real_sqrt_pow2[OF dot_pos_le])
    1.17 -  done
    1.18 +text {* TODO: move to NthRoot *}
    1.19 +lemma sqrt_add_le_add_sqrt:
    1.20 +  assumes x: "0 \<le> x" and y: "0 \<le> y"
    1.21 +  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
    1.22 +apply (rule power2_le_imp_le)
    1.23 +apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
    1.24 +apply (simp add: mult_nonneg_nonneg x y)
    1.25 +apply (simp add: add_nonneg_nonneg x y)
    1.26 +done
    1.27 +
    1.28 +lemma norm_pastecart: "norm (pastecart x y) <= norm x + norm y"
    1.29 +  unfolding vector_norm_def setL2_def setsum_UNIV_sum
    1.30 +  by (simp add: sqrt_add_le_add_sqrt setsum_nonneg)
    1.31  
    1.32  subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
    1.33