6 |
6 |
7 theory Operator_Norm |
7 theory Operator_Norm |
8 imports Linear_Algebra |
8 imports Linear_Algebra |
9 begin |
9 begin |
10 |
10 |
11 definition "onorm f = Sup {norm (f x)| x. norm x = 1}" |
11 definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))" |
12 |
12 |
13 lemma norm_bound_generalize: |
13 lemma norm_bound_generalize: |
14 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
14 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
15 assumes lf: "linear f" |
15 assumes lf: "linear f" |
16 shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" |
16 shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" |
65 fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
65 fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
66 assumes lf: "linear f" |
66 assumes lf: "linear f" |
67 shows "norm (f x) \<le> onorm f * norm x" |
67 shows "norm (f x) \<le> onorm f * norm x" |
68 and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b" |
68 and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b" |
69 proof - |
69 proof - |
70 let ?S = "{norm (f x) |x. norm x = 1}" |
70 let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}" |
71 have "norm (f (SOME i. i \<in> Basis)) \<in> ?S" |
71 have "norm (f (SOME i. i \<in> Basis)) \<in> ?S" |
72 by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis) |
72 by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis) |
73 then have Se: "?S \<noteq> {}" |
73 then have Se: "?S \<noteq> {}" |
74 by auto |
74 by auto |
75 from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b" |
75 from linear_bounded[OF lf] have b: "bdd_above ?S" |
76 unfolding norm_bound_generalize[OF lf, symmetric] |
76 unfolding norm_bound_generalize[OF lf, symmetric] by auto |
77 by (auto simp add: setle_def) |
77 then show "norm (f x) \<le> onorm f * norm x" |
78 from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] |
|
79 show "norm (f x) \<le> onorm f * norm x" |
|
80 apply - |
78 apply - |
81 apply (rule spec[where x = x]) |
79 apply (rule spec[where x = x]) |
82 unfolding norm_bound_generalize[OF lf, symmetric] |
80 unfolding norm_bound_generalize[OF lf, symmetric] |
83 apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) |
81 apply (auto simp: onorm_def intro!: cSUP_upper) |
84 done |
82 done |
85 show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b" |
83 show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b" |
86 using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] |
|
87 unfolding norm_bound_generalize[OF lf, symmetric] |
84 unfolding norm_bound_generalize[OF lf, symmetric] |
88 by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) |
85 using Se by (auto simp: onorm_def intro!: cSUP_least b) |
89 qed |
86 qed |
90 |
87 |
91 lemma onorm_pos_le: |
88 lemma onorm_pos_le: |
92 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
89 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
93 assumes lf: "linear f" |
90 assumes lf: "linear f" |
105 apply (erule allE[where x="0::real"]) |
102 apply (erule allE[where x="0::real"]) |
106 using onorm_pos_le[OF lf] |
103 using onorm_pos_le[OF lf] |
107 apply arith |
104 apply arith |
108 done |
105 done |
109 |
106 |
110 lemma onorm_const: |
107 lemma onorm_const: "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y" |
111 "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y" |
108 using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis) |
112 proof - |
|
113 let ?f = "\<lambda>x::'a. y::'b" |
|
114 have th: "{norm (?f x)| x. norm x = 1} = {norm y}" |
|
115 by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"]) |
|
116 show ?thesis |
|
117 unfolding onorm_def th |
|
118 apply (rule cSup_unique) |
|
119 apply (simp_all add: setle_def) |
|
120 done |
|
121 qed |
|
122 |
109 |
123 lemma onorm_pos_lt: |
110 lemma onorm_pos_lt: |
124 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
111 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
125 assumes lf: "linear f" |
112 assumes lf: "linear f" |
126 shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)" |
113 shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)" |