|
1 (* Title: Multivariate_Analysis/L2_Norm.thy |
|
2 Author: Brian Huffman, Portland State University |
|
3 *) |
|
4 |
|
5 header {* Square root of sum of squares *} |
|
6 |
|
7 theory L2_Norm |
|
8 imports NthRoot |
|
9 begin |
|
10 |
|
11 definition |
|
12 "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)" |
|
13 |
|
14 lemma setL2_cong: |
|
15 "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B" |
|
16 unfolding setL2_def by simp |
|
17 |
|
18 lemma strong_setL2_cong: |
|
19 "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B" |
|
20 unfolding setL2_def simp_implies_def by simp |
|
21 |
|
22 lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0" |
|
23 unfolding setL2_def by simp |
|
24 |
|
25 lemma setL2_empty [simp]: "setL2 f {} = 0" |
|
26 unfolding setL2_def by simp |
|
27 |
|
28 lemma setL2_insert [simp]: |
|
29 "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow> |
|
30 setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)" |
|
31 unfolding setL2_def by (simp add: setsum_nonneg) |
|
32 |
|
33 lemma setL2_nonneg [simp]: "0 \<le> setL2 f A" |
|
34 unfolding setL2_def by (simp add: setsum_nonneg) |
|
35 |
|
36 lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0" |
|
37 unfolding setL2_def by simp |
|
38 |
|
39 lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>" |
|
40 unfolding setL2_def by (simp add: real_sqrt_mult) |
|
41 |
|
42 lemma setL2_mono: |
|
43 assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i" |
|
44 assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i" |
|
45 shows "setL2 f K \<le> setL2 g K" |
|
46 unfolding setL2_def |
|
47 by (simp add: setsum_nonneg setsum_mono power_mono prems) |
|
48 |
|
49 lemma setL2_strict_mono: |
|
50 assumes "finite K" and "K \<noteq> {}" |
|
51 assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i" |
|
52 assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i" |
|
53 shows "setL2 f K < setL2 g K" |
|
54 unfolding setL2_def |
|
55 by (simp add: setsum_strict_mono power_strict_mono assms) |
|
56 |
|
57 lemma setL2_right_distrib: |
|
58 "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A" |
|
59 unfolding setL2_def |
|
60 apply (simp add: power_mult_distrib) |
|
61 apply (simp add: setsum_right_distrib [symmetric]) |
|
62 apply (simp add: real_sqrt_mult setsum_nonneg) |
|
63 done |
|
64 |
|
65 lemma setL2_left_distrib: |
|
66 "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A" |
|
67 unfolding setL2_def |
|
68 apply (simp add: power_mult_distrib) |
|
69 apply (simp add: setsum_left_distrib [symmetric]) |
|
70 apply (simp add: real_sqrt_mult setsum_nonneg) |
|
71 done |
|
72 |
|
73 lemma setsum_nonneg_eq_0_iff: |
|
74 fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add" |
|
75 shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
|
76 apply (induct set: finite, simp) |
|
77 apply (simp add: add_nonneg_eq_0_iff setsum_nonneg) |
|
78 done |
|
79 |
|
80 lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
|
81 unfolding setL2_def |
|
82 by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff) |
|
83 |
|
84 lemma setL2_triangle_ineq: |
|
85 shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A" |
|
86 proof (cases "finite A") |
|
87 case False |
|
88 thus ?thesis by simp |
|
89 next |
|
90 case True |
|
91 thus ?thesis |
|
92 proof (induct set: finite) |
|
93 case empty |
|
94 show ?case by simp |
|
95 next |
|
96 case (insert x F) |
|
97 hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le> |
|
98 sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)" |
|
99 by (intro real_sqrt_le_mono add_left_mono power_mono insert |
|
100 setL2_nonneg add_increasing zero_le_power2) |
|
101 also have |
|
102 "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)" |
|
103 by (rule real_sqrt_sum_squares_triangle_ineq) |
|
104 finally show ?case |
|
105 using insert by simp |
|
106 qed |
|
107 qed |
|
108 |
|
109 lemma sqrt_sum_squares_le_sum: |
|
110 "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y" |
|
111 apply (rule power2_le_imp_le) |
|
112 apply (simp add: power2_sum) |
|
113 apply (simp add: mult_nonneg_nonneg) |
|
114 apply (simp add: add_nonneg_nonneg) |
|
115 done |
|
116 |
|
117 lemma setL2_le_setsum [rule_format]: |
|
118 "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A" |
|
119 apply (cases "finite A") |
|
120 apply (induct set: finite) |
|
121 apply simp |
|
122 apply clarsimp |
|
123 apply (erule order_trans [OF sqrt_sum_squares_le_sum]) |
|
124 apply simp |
|
125 apply simp |
|
126 apply simp |
|
127 done |
|
128 |
|
129 lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>" |
|
130 apply (rule power2_le_imp_le) |
|
131 apply (simp add: power2_sum) |
|
132 apply (simp add: mult_nonneg_nonneg) |
|
133 apply (simp add: add_nonneg_nonneg) |
|
134 done |
|
135 |
|
136 lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" |
|
137 apply (cases "finite A") |
|
138 apply (induct set: finite) |
|
139 apply simp |
|
140 apply simp |
|
141 apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) |
|
142 apply simp |
|
143 apply simp |
|
144 done |
|
145 |
|
146 lemma setL2_mult_ineq_lemma: |
|
147 fixes a b c d :: real |
|
148 shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>" |
|
149 proof - |
|
150 have "0 \<le> (a * d - b * c)\<twosuperior>" by simp |
|
151 also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)" |
|
152 by (simp only: power2_diff power_mult_distrib) |
|
153 also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)" |
|
154 by simp |
|
155 finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>" |
|
156 by simp |
|
157 qed |
|
158 |
|
159 lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A" |
|
160 apply (cases "finite A") |
|
161 apply (induct set: finite) |
|
162 apply simp |
|
163 apply (rule power2_le_imp_le, simp) |
|
164 apply (rule order_trans) |
|
165 apply (rule power_mono) |
|
166 apply (erule add_left_mono) |
|
167 apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg) |
|
168 apply (simp add: power2_sum) |
|
169 apply (simp add: power_mult_distrib) |
|
170 apply (simp add: right_distrib left_distrib) |
|
171 apply (rule ord_le_eq_trans) |
|
172 apply (rule setL2_mult_ineq_lemma) |
|
173 apply simp |
|
174 apply (intro mult_nonneg_nonneg setL2_nonneg) |
|
175 apply simp |
|
176 done |
|
177 |
|
178 lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A" |
|
179 apply (rule_tac s="insert i (A - {i})" and t="A" in subst) |
|
180 apply fast |
|
181 apply (subst setL2_insert) |
|
182 apply simp |
|
183 apply simp |
|
184 apply simp |
|
185 done |
|
186 |
|
187 end |