author nipkow Thu Dec 07 18:04:52 2017 +0100 (17 months ago) changeset 67156 3a9966b88a50 parent 67155 9e5b05d54f9d child 67158 a14b83897c90
"important" annotations
```     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
```