equal
deleted
inserted
replaced
71 |
71 |
72 lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
72 lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
73 unfolding L2_set_def |
73 unfolding L2_set_def |
74 by (simp add: sum_nonneg sum_nonneg_eq_0_iff) |
74 by (simp add: sum_nonneg sum_nonneg_eq_0_iff) |
75 |
75 |
76 lemma %important L2_set_triangle_ineq: |
76 proposition L2_set_triangle_ineq: |
77 "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A" |
77 "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A" |
78 proof %unimportant (cases "finite A") |
78 proof (cases "finite A") |
79 case False |
79 case False |
80 thus ?thesis by simp |
80 thus ?thesis by simp |
81 next |
81 next |
82 case True |
82 case True |
83 thus ?thesis |
83 thus ?thesis |