src/HOL/Analysis/L2_Norm.thy
changeset 67143 db609ac2c307
parent 67006 b1278ed3cd46
child 67144 cef9a1514ed0
     1.1 --- a/src/HOL/Analysis/L2_Norm.thy	Wed Dec 06 09:11:27 2017 +0100
     1.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Wed Dec 06 15:17:05 2017 +0100
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Brian Huffman, Portland State University
     1.5  *)
     1.6  
     1.7 -section \<open>Square root of sum of squares\<close>
     1.8 +section \<open>L2 Norm\<close>
     1.9  
    1.10  theory L2_Norm
    1.11  imports Complex_Main
    1.12  begin
    1.13  
    1.14 -definition
    1.15 +definition %important
    1.16    "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
    1.17  
    1.18  lemma setL2_cong:
    1.19 @@ -74,9 +74,9 @@
    1.20    unfolding setL2_def
    1.21    by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
    1.22  
    1.23 -lemma setL2_triangle_ineq:
    1.24 +lemma %important setL2_triangle_ineq:
    1.25    shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
    1.26 -proof (cases "finite A")
    1.27 +proof %unimportant (cases "finite A")
    1.28    case False
    1.29    thus ?thesis by simp
    1.30  next