1 (* Title: HOL/Multivariate_Analysis/Operator_Norm.thy |
|
2 Author: Amine Chaieb, University of Cambridge |
|
3 Author: Brian Huffman |
|
4 *) |
|
5 |
|
6 section \<open>Operator Norm\<close> |
|
7 |
|
8 theory Operator_Norm |
|
9 imports Complex_Main |
|
10 begin |
|
11 |
|
12 text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close> |
|
13 |
|
14 definition onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" |
|
15 where "onorm f = (SUP x. norm (f x) / norm x)" |
|
16 |
|
17 lemma onorm_bound: |
|
18 assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x" |
|
19 shows "onorm f \<le> b" |
|
20 unfolding onorm_def |
|
21 proof (rule cSUP_least) |
|
22 fix x |
|
23 show "norm (f x) / norm x \<le> b" |
|
24 using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq) |
|
25 qed simp |
|
26 |
|
27 text \<open>In non-trivial vector spaces, the first assumption is redundant.\<close> |
|
28 |
|
29 lemma onorm_le: |
|
30 fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector" |
|
31 assumes "\<And>x. norm (f x) \<le> b * norm x" |
|
32 shows "onorm f \<le> b" |
|
33 proof (rule onorm_bound [OF _ assms]) |
|
34 have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV) |
|
35 then obtain a :: 'a where "a \<noteq> 0" by fast |
|
36 have "0 \<le> b * norm a" |
|
37 by (rule order_trans [OF norm_ge_zero assms]) |
|
38 with \<open>a \<noteq> 0\<close> show "0 \<le> b" |
|
39 by (simp add: zero_le_mult_iff) |
|
40 qed |
|
41 |
|
42 lemma le_onorm: |
|
43 assumes "bounded_linear f" |
|
44 shows "norm (f x) / norm x \<le> onorm f" |
|
45 proof - |
|
46 interpret f: bounded_linear f by fact |
|
47 obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b" |
|
48 using f.nonneg_bounded by auto |
|
49 then have "\<forall>x. norm (f x) / norm x \<le> b" |
|
50 by (clarify, case_tac "x = 0", |
|
51 simp_all add: f.zero pos_divide_le_eq mult.commute) |
|
52 then have "bdd_above (range (\<lambda>x. norm (f x) / norm x))" |
|
53 unfolding bdd_above_def by fast |
|
54 with UNIV_I show ?thesis |
|
55 unfolding onorm_def by (rule cSUP_upper) |
|
56 qed |
|
57 |
|
58 lemma onorm: |
|
59 assumes "bounded_linear f" |
|
60 shows "norm (f x) \<le> onorm f * norm x" |
|
61 proof - |
|
62 interpret f: bounded_linear f by fact |
|
63 show ?thesis |
|
64 proof (cases) |
|
65 assume "x = 0" |
|
66 then show ?thesis by (simp add: f.zero) |
|
67 next |
|
68 assume "x \<noteq> 0" |
|
69 have "norm (f x) / norm x \<le> onorm f" |
|
70 by (rule le_onorm [OF assms]) |
|
71 then show "norm (f x) \<le> onorm f * norm x" |
|
72 by (simp add: pos_divide_le_eq \<open>x \<noteq> 0\<close>) |
|
73 qed |
|
74 qed |
|
75 |
|
76 lemma onorm_pos_le: |
|
77 assumes f: "bounded_linear f" |
|
78 shows "0 \<le> onorm f" |
|
79 using le_onorm [OF f, where x=0] by simp |
|
80 |
|
81 lemma onorm_zero: "onorm (\<lambda>x. 0) = 0" |
|
82 proof (rule order_antisym) |
|
83 show "onorm (\<lambda>x. 0) \<le> 0" |
|
84 by (simp add: onorm_bound) |
|
85 show "0 \<le> onorm (\<lambda>x. 0)" |
|
86 using bounded_linear_zero by (rule onorm_pos_le) |
|
87 qed |
|
88 |
|
89 lemma onorm_eq_0: |
|
90 assumes f: "bounded_linear f" |
|
91 shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)" |
|
92 using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero) |
|
93 |
|
94 lemma onorm_pos_lt: |
|
95 assumes f: "bounded_linear f" |
|
96 shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)" |
|
97 by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f]) |
|
98 |
|
99 lemma onorm_id_le: "onorm (\<lambda>x. x) \<le> 1" |
|
100 by (rule onorm_bound) simp_all |
|
101 |
|
102 lemma onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1" |
|
103 proof (rule antisym[OF onorm_id_le]) |
|
104 have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV) |
|
105 then obtain x :: 'a where "x \<noteq> 0" by fast |
|
106 hence "1 \<le> norm x / norm x" |
|
107 by simp |
|
108 also have "\<dots> \<le> onorm (\<lambda>x::'a. x)" |
|
109 by (rule le_onorm) (rule bounded_linear_ident) |
|
110 finally show "1 \<le> onorm (\<lambda>x::'a. x)" . |
|
111 qed |
|
112 |
|
113 lemma onorm_compose: |
|
114 assumes f: "bounded_linear f" |
|
115 assumes g: "bounded_linear g" |
|
116 shows "onorm (f \<circ> g) \<le> onorm f * onorm g" |
|
117 proof (rule onorm_bound) |
|
118 show "0 \<le> onorm f * onorm g" |
|
119 by (intro mult_nonneg_nonneg onorm_pos_le f g) |
|
120 next |
|
121 fix x |
|
122 have "norm (f (g x)) \<le> onorm f * norm (g x)" |
|
123 by (rule onorm [OF f]) |
|
124 also have "onorm f * norm (g x) \<le> onorm f * (onorm g * norm x)" |
|
125 by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]]) |
|
126 finally show "norm ((f \<circ> g) x) \<le> onorm f * onorm g * norm x" |
|
127 by (simp add: mult.assoc) |
|
128 qed |
|
129 |
|
130 lemma onorm_scaleR_lemma: |
|
131 assumes f: "bounded_linear f" |
|
132 shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f" |
|
133 proof (rule onorm_bound) |
|
134 show "0 \<le> \<bar>r\<bar> * onorm f" |
|
135 by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f) |
|
136 next |
|
137 fix x |
|
138 have "\<bar>r\<bar> * norm (f x) \<le> \<bar>r\<bar> * (onorm f * norm x)" |
|
139 by (intro mult_left_mono onorm abs_ge_zero f) |
|
140 then show "norm (r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f * norm x" |
|
141 by (simp only: norm_scaleR mult.assoc) |
|
142 qed |
|
143 |
|
144 lemma onorm_scaleR: |
|
145 assumes f: "bounded_linear f" |
|
146 shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f" |
|
147 proof (cases "r = 0") |
|
148 assume "r \<noteq> 0" |
|
149 show ?thesis |
|
150 proof (rule order_antisym) |
|
151 show "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f" |
|
152 using f by (rule onorm_scaleR_lemma) |
|
153 next |
|
154 have "bounded_linear (\<lambda>x. r *\<^sub>R f x)" |
|
155 using bounded_linear_scaleR_right f by (rule bounded_linear_compose) |
|
156 then have "onorm (\<lambda>x. inverse r *\<^sub>R r *\<^sub>R f x) \<le> \<bar>inverse r\<bar> * onorm (\<lambda>x. r *\<^sub>R f x)" |
|
157 by (rule onorm_scaleR_lemma) |
|
158 with \<open>r \<noteq> 0\<close> show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)" |
|
159 by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute) |
|
160 qed |
|
161 qed (simp add: onorm_zero) |
|
162 |
|
163 lemma onorm_scaleR_left_lemma: |
|
164 assumes r: "bounded_linear r" |
|
165 shows "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f" |
|
166 proof (rule onorm_bound) |
|
167 fix x |
|
168 have "norm (r x *\<^sub>R f) = norm (r x) * norm f" |
|
169 by simp |
|
170 also have "\<dots> \<le> onorm r * norm x * norm f" |
|
171 by (intro mult_right_mono onorm r norm_ge_zero) |
|
172 finally show "norm (r x *\<^sub>R f) \<le> onorm r * norm f * norm x" |
|
173 by (simp add: ac_simps) |
|
174 qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r) |
|
175 |
|
176 lemma onorm_scaleR_left: |
|
177 assumes f: "bounded_linear r" |
|
178 shows "onorm (\<lambda>x. r x *\<^sub>R f) = onorm r * norm f" |
|
179 proof (cases "f = 0") |
|
180 assume "f \<noteq> 0" |
|
181 show ?thesis |
|
182 proof (rule order_antisym) |
|
183 show "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f" |
|
184 using f by (rule onorm_scaleR_left_lemma) |
|
185 next |
|
186 have bl1: "bounded_linear (\<lambda>x. r x *\<^sub>R f)" |
|
187 by (metis bounded_linear_scaleR_const f) |
|
188 have "bounded_linear (\<lambda>x. r x * norm f)" |
|
189 by (metis bounded_linear_mult_const f) |
|
190 from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"] |
|
191 have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)" |
|
192 using \<open>f \<noteq> 0\<close> |
|
193 by (simp add: inverse_eq_divide) |
|
194 also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)" |
|
195 by (rule onorm_bound) |
|
196 (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm]) |
|
197 finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)" |
|
198 using \<open>f \<noteq> 0\<close> |
|
199 by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute) |
|
200 qed |
|
201 qed (simp add: onorm_zero) |
|
202 |
|
203 lemma onorm_neg: |
|
204 shows "onorm (\<lambda>x. - f x) = onorm f" |
|
205 unfolding onorm_def by simp |
|
206 |
|
207 lemma onorm_triangle: |
|
208 assumes f: "bounded_linear f" |
|
209 assumes g: "bounded_linear g" |
|
210 shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g" |
|
211 proof (rule onorm_bound) |
|
212 show "0 \<le> onorm f + onorm g" |
|
213 by (intro add_nonneg_nonneg onorm_pos_le f g) |
|
214 next |
|
215 fix x |
|
216 have "norm (f x + g x) \<le> norm (f x) + norm (g x)" |
|
217 by (rule norm_triangle_ineq) |
|
218 also have "norm (f x) + norm (g x) \<le> onorm f * norm x + onorm g * norm x" |
|
219 by (intro add_mono onorm f g) |
|
220 finally show "norm (f x + g x) \<le> (onorm f + onorm g) * norm x" |
|
221 by (simp only: distrib_right) |
|
222 qed |
|
223 |
|
224 lemma onorm_triangle_le: |
|
225 assumes "bounded_linear f" |
|
226 assumes "bounded_linear g" |
|
227 assumes "onorm f + onorm g \<le> e" |
|
228 shows "onorm (\<lambda>x. f x + g x) \<le> e" |
|
229 using assms by (rule onorm_triangle [THEN order_trans]) |
|
230 |
|
231 lemma onorm_triangle_lt: |
|
232 assumes "bounded_linear f" |
|
233 assumes "bounded_linear g" |
|
234 assumes "onorm f + onorm g < e" |
|
235 shows "onorm (\<lambda>x. f x + g x) < e" |
|
236 using assms by (rule onorm_triangle [THEN order_le_less_trans]) |
|
237 |
|
238 end |
|