author | wenzelm |
Mon, 07 Dec 2015 20:19:59 +0100 | |
changeset 61808 | fc1556774cfe |
parent 60420 | 884f54e01427 |
child 61915 | e9812a95d108 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Multivariate_Analysis/Operator_Norm.thy |
36581 | 2 |
Author: Amine Chaieb, University of Cambridge |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
3 |
Author: Brian Huffman |
36581 | 4 |
*) |
5 |
||
60420 | 6 |
section \<open>Operator Norm\<close> |
36581 | 7 |
|
8 |
theory Operator_Norm |
|
56319 | 9 |
imports Complex_Main |
36581 | 10 |
begin |
11 |
||
61808 | 12 |
text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close> |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
13 |
|
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
14 |
definition onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
15 |
where "onorm f = (SUP x. norm (f x) / norm x)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
16 |
|
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
17 |
lemma onorm_bound: |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
18 |
assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
19 |
shows "onorm f \<le> b" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
20 |
unfolding onorm_def |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
21 |
proof (rule cSUP_least) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
22 |
fix x |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
23 |
show "norm (f x) / norm x \<le> b" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
24 |
using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
25 |
qed simp |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
26 |
|
60420 | 27 |
text \<open>In non-trivial vector spaces, the first assumption is redundant.\<close> |
36581 | 28 |
|
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
29 |
lemma onorm_le: |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
30 |
fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
31 |
assumes "\<And>x. norm (f x) \<le> b * norm x" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
32 |
shows "onorm f \<le> b" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
33 |
proof (rule onorm_bound [OF _ assms]) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
34 |
have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
35 |
then obtain a :: 'a where "a \<noteq> 0" by fast |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
36 |
have "0 \<le> b * norm a" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
37 |
by (rule order_trans [OF norm_ge_zero assms]) |
60420 | 38 |
with \<open>a \<noteq> 0\<close> show "0 \<le> b" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
39 |
by (simp add: zero_le_mult_iff) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
40 |
qed |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
41 |
|
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
42 |
lemma le_onorm: |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
43 |
assumes "bounded_linear f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
44 |
shows "norm (f x) / norm x \<le> onorm f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
45 |
proof - |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
46 |
interpret f: bounded_linear f by fact |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
47 |
obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
48 |
using f.nonneg_bounded by auto |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
49 |
then have "\<forall>x. norm (f x) / norm x \<le> b" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
50 |
by (clarify, case_tac "x = 0", |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56319
diff
changeset
|
51 |
simp_all add: f.zero pos_divide_le_eq mult.commute) |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
52 |
then have "bdd_above (range (\<lambda>x. norm (f x) / norm x))" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
53 |
unfolding bdd_above_def by fast |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
54 |
with UNIV_I show ?thesis |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
55 |
unfolding onorm_def by (rule cSUP_upper) |
53253 | 56 |
qed |
36581 | 57 |
|
58 |
lemma onorm: |
|
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
59 |
assumes "bounded_linear f" |
53253 | 60 |
shows "norm (f x) \<le> onorm f * norm x" |
61 |
proof - |
|
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
62 |
interpret f: bounded_linear f by fact |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
63 |
show ?thesis |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
64 |
proof (cases) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
65 |
assume "x = 0" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
66 |
then show ?thesis by (simp add: f.zero) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
67 |
next |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
68 |
assume "x \<noteq> 0" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
69 |
have "norm (f x) / norm x \<le> onorm f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
70 |
by (rule le_onorm [OF assms]) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
71 |
then show "norm (f x) \<le> onorm f * norm x" |
60420 | 72 |
by (simp add: pos_divide_le_eq \<open>x \<noteq> 0\<close>) |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
73 |
qed |
36581 | 74 |
qed |
75 |
||
53253 | 76 |
lemma onorm_pos_le: |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
77 |
assumes f: "bounded_linear f" |
53253 | 78 |
shows "0 \<le> onorm f" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
79 |
using le_onorm [OF f, where x=0] by simp |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
80 |
|
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
81 |
lemma onorm_zero: "onorm (\<lambda>x. 0) = 0" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
82 |
proof (rule order_antisym) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
83 |
show "onorm (\<lambda>x. 0) \<le> 0" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
84 |
by (simp add: onorm_bound) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
85 |
show "0 \<le> onorm (\<lambda>x. 0)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
86 |
using bounded_linear_zero by (rule onorm_pos_le) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
87 |
qed |
36581 | 88 |
|
53253 | 89 |
lemma onorm_eq_0: |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
90 |
assumes f: "bounded_linear f" |
36581 | 91 |
shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
92 |
using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero) |
36581 | 93 |
|
53253 | 94 |
lemma onorm_pos_lt: |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
95 |
assumes f: "bounded_linear f" |
53688 | 96 |
shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
97 |
by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f]) |
36581 | 98 |
|
99 |
lemma onorm_compose: |
|
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
100 |
assumes f: "bounded_linear f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
101 |
assumes g: "bounded_linear g" |
53688 | 102 |
shows "onorm (f \<circ> g) \<le> onorm f * onorm g" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
103 |
proof (rule onorm_bound) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
104 |
show "0 \<le> onorm f * onorm g" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
105 |
by (intro mult_nonneg_nonneg onorm_pos_le f g) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
106 |
next |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
107 |
fix x |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
108 |
have "norm (f (g x)) \<le> onorm f * norm (g x)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
109 |
by (rule onorm [OF f]) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
110 |
also have "onorm f * norm (g x) \<le> onorm f * (onorm g * norm x)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
111 |
by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]]) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
112 |
finally show "norm ((f \<circ> g) x) \<le> onorm f * onorm g * norm x" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56319
diff
changeset
|
113 |
by (simp add: mult.assoc) |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
114 |
qed |
36581 | 115 |
|
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
116 |
lemma onorm_scaleR_lemma: |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
117 |
assumes f: "bounded_linear f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
118 |
shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
119 |
proof (rule onorm_bound) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
120 |
show "0 \<le> \<bar>r\<bar> * onorm f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
121 |
by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
122 |
next |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
123 |
fix x |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
124 |
have "\<bar>r\<bar> * norm (f x) \<le> \<bar>r\<bar> * (onorm f * norm x)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
125 |
by (intro mult_left_mono onorm abs_ge_zero f) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
126 |
then show "norm (r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f * norm x" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56319
diff
changeset
|
127 |
by (simp only: norm_scaleR mult.assoc) |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
128 |
qed |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
129 |
|
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
130 |
lemma onorm_scaleR: |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
131 |
assumes f: "bounded_linear f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
132 |
shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
133 |
proof (cases "r = 0") |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
134 |
assume "r \<noteq> 0" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
135 |
show ?thesis |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
136 |
proof (rule order_antisym) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
137 |
show "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
138 |
using f by (rule onorm_scaleR_lemma) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
139 |
next |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
140 |
have "bounded_linear (\<lambda>x. r *\<^sub>R f x)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
141 |
using bounded_linear_scaleR_right f by (rule bounded_linear_compose) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
142 |
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)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
143 |
by (rule onorm_scaleR_lemma) |
60420 | 144 |
with \<open>r \<noteq> 0\<close> show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56319
diff
changeset
|
145 |
by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute) |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
146 |
qed |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
147 |
qed (simp add: onorm_zero) |
36581 | 148 |
|
53253 | 149 |
lemma onorm_neg: |
36581 | 150 |
shows "onorm (\<lambda>x. - f x) = onorm f" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
151 |
unfolding onorm_def by simp |
36581 | 152 |
|
153 |
lemma onorm_triangle: |
|
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
154 |
assumes f: "bounded_linear f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
155 |
assumes g: "bounded_linear g" |
53253 | 156 |
shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
157 |
proof (rule onorm_bound) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
158 |
show "0 \<le> onorm f + onorm g" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
159 |
by (intro add_nonneg_nonneg onorm_pos_le f g) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
160 |
next |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
161 |
fix x |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
162 |
have "norm (f x + g x) \<le> norm (f x) + norm (g x)" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
163 |
by (rule norm_triangle_ineq) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
164 |
also have "norm (f x) + norm (g x) \<le> onorm f * norm x + onorm g * norm x" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
165 |
by (intro add_mono onorm f g) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
166 |
finally show "norm (f x + g x) \<le> (onorm f + onorm g) * norm x" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
167 |
by (simp only: distrib_right) |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
168 |
qed |
36581 | 169 |
|
53253 | 170 |
lemma onorm_triangle_le: |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
171 |
assumes "bounded_linear f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
172 |
assumes "bounded_linear g" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
173 |
assumes "onorm f + onorm g \<le> e" |
53688 | 174 |
shows "onorm (\<lambda>x. f x + g x) \<le> e" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
175 |
using assms by (rule onorm_triangle [THEN order_trans]) |
36581 | 176 |
|
53253 | 177 |
lemma onorm_triangle_lt: |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
178 |
assumes "bounded_linear f" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
179 |
assumes "bounded_linear g" |
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
180 |
assumes "onorm f + onorm g < e" |
53688 | 181 |
shows "onorm (\<lambda>x. f x + g x) < e" |
56223
7696903b9e61
generalize theory of operator norms to work with class real_normed_vector
huffman
parents:
54263
diff
changeset
|
182 |
using assms by (rule onorm_triangle [THEN order_le_less_trans]) |
36581 | 183 |
|
184 |
end |