src/HOL/Multivariate_Analysis/L2_Norm.thy
changeset 44142 8e27e0177518
parent 41959 b460124855b8
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 10 17:02:03 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 10 18:02:16 2011 -0700
     1.3 @@ -109,9 +109,8 @@
     1.4  lemma sqrt_sum_squares_le_sum:
     1.5    "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
     1.6    apply (rule power2_le_imp_le)
     1.7 -  apply (simp add: power2_sum)
     1.8 -  apply (simp add: mult_nonneg_nonneg)
     1.9 -  apply (simp add: add_nonneg_nonneg)
    1.10 +  apply (simp add: power2_sum mult_nonneg_nonneg)
    1.11 +  apply simp
    1.12    done
    1.13  
    1.14  lemma setL2_le_setsum [rule_format]:
    1.15 @@ -128,9 +127,8 @@
    1.16  
    1.17  lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
    1.18    apply (rule power2_le_imp_le)
    1.19 -  apply (simp add: power2_sum)
    1.20 -  apply (simp add: mult_nonneg_nonneg)
    1.21 -  apply (simp add: add_nonneg_nonneg)
    1.22 +  apply (simp add: power2_sum mult_nonneg_nonneg)
    1.23 +  apply simp
    1.24    done
    1.25  
    1.26  lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
    1.27 @@ -164,7 +162,7 @@
    1.28    apply (rule order_trans)
    1.29    apply (rule power_mono)
    1.30    apply (erule add_left_mono)
    1.31 -  apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
    1.32 +  apply (simp add: mult_nonneg_nonneg setsum_nonneg)
    1.33    apply (simp add: power2_sum)
    1.34    apply (simp add: power_mult_distrib)
    1.35    apply (simp add: right_distrib left_distrib)