1.1 --- a/src/HOL/Analysis/L2_Norm.thy Thu Dec 07 15:48:50 2017 +0100
1.2 +++ b/src/HOL/Analysis/L2_Norm.thy Thu Dec 07 18:04:52 2017 +0100
1.3 @@ -8,7 +8,7 @@
1.4 imports Complex_Main
1.5 begin
1.6
1.7 -definition "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
1.8 +definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
1.9
1.10 lemma L2_set_cong:
1.11 "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
1.12 @@ -73,9 +73,9 @@
1.13 unfolding L2_set_def
1.14 by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
1.15
1.16 -lemma L2_set_triangle_ineq:
1.17 - shows "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
1.18 -proof (cases "finite A")
1.19 +lemma %important L2_set_triangle_ineq:
1.20 + "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
1.21 +proof %unimportant (cases "finite A")
1.22 case False
1.23 thus ?thesis by simp
1.24 next