author | paulson <lp15@cam.ac.uk> |
Tue, 31 Mar 2015 16:48:48 +0100 | |
changeset 59865 | 8a20dd967385 |
parent 59554 | 4044f53326c9 |
child 60017 | b785d6d06430 |
permissions | -rw-r--r-- |
59453 | 1 |
section {* Bounded Continuous Functions *} |
2 |
theory Bounded_Continuous_Function |
|
3 |
imports Integration |
|
4 |
begin |
|
5 |
||
6 |
subsection{* Definition *} |
|
7 |
||
8 |
definition "bcontfun = {f :: 'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}" |
|
9 |
||
10 |
typedef ('a, 'b) bcontfun = |
|
11 |
"bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set" |
|
12 |
by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def) |
|
13 |
||
14 |
lemma bcontfunE: |
|
15 |
assumes "f \<in> bcontfun" |
|
16 |
obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y" |
|
17 |
using assms unfolding bcontfun_def |
|
18 |
by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI) |
|
19 |
||
20 |
lemma bcontfunE': |
|
21 |
assumes "f \<in> bcontfun" |
|
22 |
obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y" |
|
23 |
using assms bcontfunE |
|
24 |
by metis |
|
25 |
||
26 |
lemma bcontfunI: |
|
27 |
"continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun" |
|
28 |
unfolding bcontfun_def |
|
29 |
by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE) |
|
30 |
||
31 |
lemma bcontfunI': |
|
32 |
"continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun" |
|
33 |
using bcontfunI by metis |
|
34 |
||
35 |
lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)" |
|
36 |
using Rep_bcontfun[of x] |
|
37 |
by (auto simp: bcontfun_def intro: continuous_on_subset) |
|
38 |
||
39 |
instantiation bcontfun :: (topological_space, metric_space) metric_space |
|
40 |
begin |
|
41 |
||
42 |
definition dist_bcontfun::"('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real" where |
|
43 |
"dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))" |
|
44 |
||
45 |
definition |
|
46 |
open_bcontfun::"('a, 'b) bcontfun set \<Rightarrow> bool" where |
|
47 |
"open_bcontfun S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
|
48 |
||
49 |
lemma dist_bounded: |
|
50 |
fixes f ::"('a, 'b) bcontfun" |
|
51 |
shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g" |
|
52 |
proof - |
|
53 |
have "Rep_bcontfun f \<in> bcontfun" using Rep_bcontfun . |
|
54 |
from bcontfunE'[OF this] obtain y where y: |
|
55 |
"continuous_on UNIV (Rep_bcontfun f)" |
|
56 |
"\<And>x. dist (Rep_bcontfun f x) undefined \<le> y" |
|
57 |
by auto |
|
58 |
have "Rep_bcontfun g \<in> bcontfun" using Rep_bcontfun . |
|
59 |
from bcontfunE'[OF this] obtain z where z: |
|
60 |
"continuous_on UNIV (Rep_bcontfun g)" |
|
61 |
"\<And>x. dist (Rep_bcontfun g x) undefined \<le> z" |
|
62 |
by auto |
|
63 |
show ?thesis unfolding dist_bcontfun_def |
|
64 |
proof (intro cSUP_upper bdd_aboveI2) |
|
65 |
fix x |
|
66 |
have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined" |
|
67 |
by (rule dist_triangle2) |
|
68 |
also have "\<dots> \<le> y + z" using y(2)[of x] z(2)[of x] by (rule add_mono) |
|
69 |
finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" . |
|
70 |
qed simp |
|
71 |
qed |
|
72 |
||
73 |
lemma dist_bound: |
|
74 |
fixes f ::"('a, 'b) bcontfun" |
|
75 |
assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b" |
|
76 |
shows "dist f g \<le> b" |
|
77 |
using assms by (auto simp: dist_bcontfun_def intro: cSUP_least) |
|
78 |
||
79 |
lemma dist_bounded_Abs: |
|
80 |
fixes f g ::"'a \<Rightarrow> 'b" |
|
81 |
assumes "f \<in> bcontfun" "g \<in> bcontfun" |
|
82 |
shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)" |
|
83 |
by (metis Abs_bcontfun_inverse assms dist_bounded) |
|
84 |
||
85 |
lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun" |
|
86 |
by (auto intro: bcontfunI continuous_on_const) |
|
87 |
||
88 |
lemma dist_fun_lt_imp_dist_val_lt: |
|
89 |
assumes "dist f g < e" |
|
90 |
shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e" |
|
91 |
using dist_bounded assms by (rule le_less_trans) |
|
92 |
||
93 |
lemma dist_val_lt_imp_dist_fun_le: |
|
94 |
assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e" |
|
95 |
shows "dist f g \<le> e" |
|
96 |
unfolding dist_bcontfun_def |
|
97 |
proof (intro cSUP_least) |
|
98 |
fix x |
|
99 |
show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e" |
|
100 |
using assms[THEN spec[where x=x]] by (simp add: dist_norm) |
|
101 |
qed (simp) |
|
102 |
||
103 |
instance |
|
104 |
proof |
|
105 |
fix f g::"('a, 'b) bcontfun" |
|
106 |
show "dist f g = 0 \<longleftrightarrow> f = g" |
|
107 |
proof |
|
108 |
have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g" by (rule dist_bounded) |
|
109 |
also assume "dist f g = 0" |
|
110 |
finally show "f = g" by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse) |
|
111 |
qed (auto simp: dist_bcontfun_def SUP_def simp del: Sup_image_eq intro!: cSup_eq) |
|
112 |
next |
|
113 |
fix f g h :: "('a, 'b) bcontfun" |
|
114 |
show "dist f g \<le> dist f h + dist g h" |
|
115 |
proof (subst dist_bcontfun_def, safe intro!: cSUP_least) |
|
116 |
fix x |
|
117 |
have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> |
|
118 |
dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)" |
|
119 |
by (rule dist_triangle2) |
|
120 |
also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h" by (rule dist_bounded) |
|
121 |
also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h" by (rule dist_bounded) |
|
122 |
finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h" by simp |
|
123 |
qed |
|
124 |
qed (simp add: open_bcontfun_def) |
|
125 |
end |
|
126 |
||
127 |
lemma closed_Pi_bcontfun: |
|
128 |
fixes I::"'a::metric_space set" and X::"'a \<Rightarrow> 'b::complete_space set" |
|
129 |
assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)" |
|
130 |
shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))" |
|
131 |
unfolding closed_sequential_limits |
|
132 |
proof safe |
|
133 |
fix f l |
|
134 |
assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f ----> l" |
|
135 |
have lim_fun: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (Rep_bcontfun l x) < e" |
|
136 |
using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim] |
|
137 |
by (intro uniformly_cauchy_imp_uniformly_convergent[where P="%_. True", simplified]) |
|
138 |
(metis dist_fun_lt_imp_dist_val_lt)+ |
|
139 |
show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" |
|
140 |
proof (rule, safe) |
|
141 |
fix x assume "x \<in> I" |
|
142 |
hence "closed (X x)" using assms by simp |
|
143 |
moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially" |
|
144 |
proof (rule always_eventually, safe) |
|
145 |
fix i |
|
146 |
from seq[THEN spec, of i] `x \<in> I` |
|
147 |
show "Rep_bcontfun (f i) x \<in> X x" |
|
148 |
by (auto simp: Abs_bcontfun_inverse) |
|
149 |
qed |
|
150 |
moreover note sequentially_bot |
|
151 |
moreover have "(\<lambda>n. Rep_bcontfun (f n) x) ----> Rep_bcontfun l x" |
|
152 |
using lim_fun by (blast intro!: metric_LIMSEQ_I) |
|
153 |
ultimately show "Rep_bcontfun l x \<in> X x" |
|
154 |
by (rule Lim_in_closed_set) |
|
155 |
qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse) |
|
156 |
qed |
|
157 |
||
158 |
subsection {* Complete Space *} |
|
159 |
||
160 |
instance bcontfun :: (metric_space, complete_space) complete_space |
|
161 |
proof |
|
162 |
fix f::"nat \<Rightarrow> ('a,'b) bcontfun" |
|
163 |
assume "Cauchy f" --{* Cauchy equals uniform convergence *} |
|
164 |
then obtain g where limit_function: |
|
165 |
"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e" |
|
166 |
using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" |
|
167 |
"\<lambda>n. Rep_bcontfun (f n)"] |
|
168 |
unfolding Cauchy_def by (metis dist_fun_lt_imp_dist_val_lt) |
|
169 |
||
170 |
then obtain N where fg_dist: --{* for an upper bound on g *} |
|
171 |
"\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1" |
|
172 |
by (force simp add: dist_commute) |
|
173 |
from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where |
|
174 |
f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b" by force |
|
175 |
have "g \<in> bcontfun" --{* The limit function is bounded and continuous *} |
|
176 |
proof (intro bcontfunI) |
|
177 |
show "continuous_on UNIV g" |
|
178 |
using bcontfunE[OF Rep_bcontfun] limit_function |
|
179 |
by (intro continuous_uniform_limit[where |
|
180 |
f="%n. Rep_bcontfun (f n)" and F="sequentially"]) (auto |
|
181 |
simp add: eventually_sequentially trivial_limit_def dist_norm) |
|
182 |
next |
|
183 |
fix x |
|
184 |
from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1" |
|
185 |
by (simp add: dist_norm norm_minus_commute) |
|
186 |
with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"] |
|
187 |
show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x] |
|
188 |
by simp |
|
189 |
qed |
|
190 |
show "convergent f" |
|
191 |
proof (rule convergentI, subst LIMSEQ_def, safe) |
|
192 |
--{* The limit function converges according to its norm *} |
|
193 |
fix e::real |
|
194 |
assume "e > 0" hence "e/2 > 0" by simp |
|
195 |
with limit_function[THEN spec, of"e/2"] |
|
196 |
have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2" |
|
197 |
by simp |
|
198 |
then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto |
|
199 |
show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e" |
|
200 |
proof (rule, safe) |
|
201 |
fix n |
|
202 |
assume "N \<le> n" |
|
203 |
with N show "dist (f n) (Abs_bcontfun g) < e" |
|
204 |
using dist_val_lt_imp_dist_fun_le[of |
|
205 |
"f n" "Abs_bcontfun g" "e/2"] |
|
206 |
Abs_bcontfun_inverse[OF `g \<in> bcontfun`] `e > 0` by simp |
|
207 |
qed |
|
208 |
qed |
|
209 |
qed |
|
210 |
||
211 |
subsection{* Supremum norm for a normed vector space *} |
|
212 |
||
213 |
instantiation bcontfun :: (topological_space, real_normed_vector) real_vector |
|
214 |
begin |
|
215 |
||
216 |
definition "-f = Abs_bcontfun (\<lambda>x. -(Rep_bcontfun f x))" |
|
217 |
||
218 |
definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)" |
|
219 |
||
220 |
definition "f - g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x - Rep_bcontfun g x)" |
|
221 |
||
222 |
definition "0 = Abs_bcontfun (\<lambda>x. 0)" |
|
223 |
||
224 |
definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)" |
|
225 |
||
226 |
lemma plus_cont: |
|
227 |
fixes f g ::"'a \<Rightarrow> 'b" |
|
228 |
assumes f: "f \<in> bcontfun" and g: "g \<in> bcontfun" |
|
229 |
shows "(\<lambda>x. f x + g x) \<in> bcontfun" |
|
230 |
proof - |
|
231 |
from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y" |
|
232 |
by auto |
|
233 |
moreover |
|
234 |
from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z" |
|
235 |
by auto |
|
236 |
ultimately show ?thesis |
|
237 |
proof (intro bcontfunI) |
|
238 |
fix x |
|
239 |
have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)" by simp |
|
240 |
also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0" by (rule dist_triangle_add) |
|
241 |
also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" |
|
242 |
unfolding zero_bcontfun_def using assms |
|
243 |
by (auto intro!: add_mono dist_bounded_Abs const_bcontfun) |
|
244 |
finally |
|
245 |
show "dist (f x + g x) 0 <= dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" . |
|
246 |
qed (simp add: continuous_on_add) |
|
247 |
qed |
|
248 |
||
249 |
lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x" |
|
250 |
by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun) |
|
251 |
||
252 |
lemma uminus_cont: |
|
253 |
fixes f ::"'a \<Rightarrow> 'b" |
|
254 |
assumes "f \<in> bcontfun" |
|
255 |
shows "(\<lambda>x. - f x) \<in> bcontfun" |
|
256 |
proof - |
|
257 |
from bcontfunE[OF assms, of 0] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y" |
|
258 |
by auto |
|
259 |
thus ?thesis |
|
260 |
proof (intro bcontfunI) |
|
261 |
fix x |
|
262 |
assume "\<And>x. dist (f x) 0 \<le> y" |
|
263 |
thus "dist (- f x) 0 \<le> y" by (subst dist_minus[symmetric]) simp |
|
264 |
qed (simp add: continuous_on_minus) |
|
265 |
qed |
|
266 |
||
267 |
lemma Rep_bcontfun_uminus[simp]: |
|
268 |
"Rep_bcontfun (- f) x = - Rep_bcontfun f x" |
|
269 |
by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun) |
|
270 |
||
271 |
lemma minus_cont: |
|
272 |
fixes f g ::"'a \<Rightarrow> 'b" |
|
273 |
assumes f: "f \<in> bcontfun" and g: "g \<in> bcontfun" |
|
274 |
shows "(\<lambda>x. f x - g x) \<in> bcontfun" |
|
275 |
using plus_cont [of f "- g"] assms by (simp add: uminus_cont fun_Compl_def) |
|
276 |
||
277 |
lemma Rep_bcontfun_minus[simp]: |
|
278 |
"Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x" |
|
279 |
by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun) |
|
280 |
||
281 |
lemma scaleR_cont: |
|
282 |
fixes a and f::"'a \<Rightarrow> 'b" |
|
283 |
assumes "f \<in> bcontfun" |
|
284 |
shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun" |
|
285 |
proof - |
|
286 |
from bcontfunE[OF assms, of 0] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y" |
|
287 |
by auto |
|
288 |
thus ?thesis |
|
289 |
proof (intro bcontfunI) |
|
290 |
fix x assume "\<And>x. dist (f x) 0 \<le> y" |
|
59554
4044f53326c9
inlined rules to free user-space from technical names
haftmann
parents:
59453
diff
changeset
|
291 |
then show "dist (a *\<^sub>R f x) 0 \<le> abs a * y" |
4044f53326c9
inlined rules to free user-space from technical names
haftmann
parents:
59453
diff
changeset
|
292 |
by (metis norm_cmul_rule_thm norm_conv_dist) |
59453 | 293 |
qed (simp add: continuous_intros) |
294 |
qed |
|
295 |
||
296 |
lemma Rep_bcontfun_scaleR[simp]: |
|
297 |
"Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x" |
|
298 |
by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun) |
|
299 |
||
300 |
instance |
|
301 |
proof |
|
302 |
qed (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def |
|
303 |
Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps |
|
304 |
plus_cont const_bcontfun minus_cont scaleR_cont) |
|
305 |
end |
|
306 |
||
307 |
instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector |
|
308 |
begin |
|
309 |
||
310 |
definition norm_bcontfun::"('a, 'b) bcontfun \<Rightarrow> real" where |
|
311 |
"norm_bcontfun f = dist f 0" |
|
312 |
||
313 |
definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f" |
|
314 |
||
315 |
instance |
|
316 |
proof |
|
317 |
fix f g::"('a, 'b) bcontfun" |
|
318 |
show "dist f g = norm (f - g)" |
|
319 |
by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def |
|
320 |
Abs_bcontfun_inverse const_bcontfun norm_conv_dist[symmetric] dist_norm) |
|
321 |
show "norm (f + g) \<le> norm f + norm g" |
|
322 |
unfolding norm_bcontfun_def |
|
323 |
proof (subst dist_bcontfun_def, safe intro!: cSUP_least) |
|
324 |
fix x |
|
325 |
have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> |
|
326 |
dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0" |
|
327 |
by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm |
|
328 |
le_less_linear less_irrefl norm_triangle_lt) |
|
329 |
also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0" |
|
330 |
using dist_bounded[of f x 0] |
|
331 |
by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def) |
|
332 |
also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0] |
|
333 |
by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def) |
|
334 |
finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp |
|
335 |
qed |
|
336 |
next |
|
337 |
fix a and f g:: "('a, 'b) bcontfun" |
|
338 |
show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f" |
|
339 |
proof - |
|
340 |
have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) = |
|
341 |
(SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)" |
|
342 |
proof (intro continuous_at_Sup_mono bdd_aboveI2) |
|
343 |
fix x |
|
344 |
show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0] |
|
345 |
by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def |
|
346 |
const_bcontfun) |
|
347 |
qed (auto intro!: monoI mult_left_mono continuous_intros) |
|
348 |
moreover |
|
349 |
have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) = |
|
350 |
(\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))" |
|
351 |
by (auto simp: norm_conv_dist[symmetric]) |
|
352 |
ultimately |
|
353 |
show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f" |
|
354 |
by (simp add: norm_bcontfun_def dist_bcontfun_def norm_conv_dist Abs_bcontfun_inverse |
|
355 |
zero_bcontfun_def const_bcontfun SUP_def del: Sup_image_eq) |
|
356 |
qed |
|
357 |
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def) |
|
358 |
||
359 |
end |
|
360 |
||
361 |
lemma bcontfun_normI: |
|
362 |
"continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun" |
|
363 |
unfolding norm_conv_dist |
|
364 |
by (auto intro: bcontfunI) |
|
365 |
||
366 |
lemma norm_bounded: |
|
367 |
fixes f ::"('a::topological_space, 'b::real_normed_vector) bcontfun" |
|
368 |
shows "norm (Rep_bcontfun f x) \<le> norm f" |
|
369 |
using dist_bounded[of f x 0] |
|
370 |
by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def |
|
371 |
const_bcontfun) |
|
372 |
||
373 |
lemma norm_bound: |
|
374 |
fixes f ::"('a::topological_space, 'b::real_normed_vector) bcontfun" |
|
375 |
assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b" |
|
376 |
shows "norm f \<le> b" |
|
377 |
using dist_bound[of f 0 b] assms |
|
378 |
by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def |
|
379 |
const_bcontfun) |
|
380 |
||
381 |
subsection{* Continuously Extended Functions *} |
|
382 |
||
383 |
definition clamp::"'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
384 |
"clamp a b x = (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)" |
|
385 |
||
386 |
definition ext_cont::"('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun" |
|
387 |
where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))" |
|
388 |
||
389 |
lemma ext_cont_def': |
|
390 |
"ext_cont f a b = Abs_bcontfun (\<lambda>x. |
|
391 |
f (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i))" |
|
392 |
unfolding ext_cont_def clamp_def .. |
|
393 |
||
394 |
lemma clamp_in_interval: |
|
395 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
396 |
shows "clamp a b x \<in> cbox a b" |
|
397 |
unfolding clamp_def |
|
398 |
using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def) |
|
399 |
||
400 |
lemma dist_clamps_le_dist_args: |
|
401 |
fixes x::"'a::euclidean_space" |
|
402 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
403 |
shows "dist (clamp a b y) (clamp a b x) \<le> dist y x" |
|
404 |
proof - |
|
405 |
from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)" |
|
406 |
by (simp add: cbox_def) |
|
407 |
hence "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) |
|
408 |
\<le> (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)" |
|
409 |
by (auto intro!: setsum_mono |
|
59865
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
410 |
simp add: clamp_def dist_real_def abs_le_square_iff[symmetric]) |
59453 | 411 |
thus ?thesis |
412 |
by (auto intro: real_sqrt_le_mono |
|
413 |
simp add: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def) |
|
414 |
qed |
|
415 |
||
416 |
lemma clamp_continuous_at: |
|
417 |
fixes f::"'a::euclidean_space \<Rightarrow> 'b::metric_space" |
|
418 |
fixes x |
|
419 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
420 |
assumes f_cont: "continuous_on (cbox a b) f" |
|
421 |
shows "continuous (at x) (\<lambda>x. f (clamp a b x))" |
|
422 |
unfolding continuous_at_eps_delta |
|
423 |
proof (safe) |
|
424 |
fix x::'a and e::real |
|
425 |
assume "0 < e" |
|
426 |
moreover |
|
427 |
have "clamp a b x \<in> cbox a b" by (simp add: clamp_in_interval assms) |
|
428 |
moreover |
|
429 |
note f_cont[simplified continuous_on_iff] |
|
430 |
ultimately |
|
431 |
obtain d where d: "0 < d" |
|
432 |
"\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e" |
|
433 |
by force |
|
434 |
show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow> |
|
435 |
dist (f (clamp a b x')) (f (clamp a b x)) < e" |
|
436 |
by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans]) |
|
437 |
qed |
|
438 |
||
439 |
lemma clamp_continuous_on: |
|
440 |
fixes f::"'a::euclidean_space \<Rightarrow> 'b::metric_space" |
|
441 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
442 |
assumes f_cont: "continuous_on (cbox a b) f" |
|
443 |
shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))" |
|
444 |
using assms |
|
445 |
by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at) |
|
446 |
||
447 |
lemma clamp_bcontfun: |
|
448 |
fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
449 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
450 |
assumes continuous: "continuous_on (cbox a b) f" |
|
451 |
shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun" |
|
452 |
proof - |
|
453 |
from compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded] |
|
454 |
have "bounded (f ` (cbox a b))" . |
|
455 |
then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c" by (auto simp add: bounded_pos) |
|
456 |
show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun" |
|
457 |
proof (intro bcontfun_normI) |
|
458 |
fix x |
|
459 |
from clamp_in_interval[OF assms(1), of x] f_bound |
|
460 |
show "norm (f (clamp a b x)) \<le> c" by (simp add: ext_cont_def) |
|
461 |
qed (simp add: clamp_continuous_on assms) |
|
462 |
qed |
|
463 |
||
464 |
lemma integral_clamp: |
|
465 |
"integral {t0::real..clamp t0 t1 x} f = |
|
466 |
(if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)" |
|
467 |
by (auto simp: clamp_def) |
|
468 |
||
469 |
||
470 |
declare [[coercion Rep_bcontfun]] |
|
471 |
||
472 |
lemma ext_cont_cancel[simp]: |
|
473 |
fixes x a b::"'a::euclidean_space" |
|
474 |
assumes x: "x \<in> cbox a b" |
|
475 |
assumes "continuous_on (cbox a b) f" |
|
476 |
shows "ext_cont f a b x = f x" |
|
477 |
using assms |
|
478 |
unfolding ext_cont_def |
|
479 |
proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun]) |
|
480 |
show "f (clamp a b x) = f x" |
|
481 |
using x unfolding clamp_def mem_box |
|
482 |
by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less) |
|
483 |
qed (auto simp: cbox_def) |
|
484 |
||
485 |
lemma ext_cont_cong: |
|
486 |
assumes "t0 = s0" |
|
487 |
assumes "t1 = s1" |
|
488 |
assumes "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t" |
|
489 |
assumes "continuous_on (cbox t0 t1) f" |
|
490 |
assumes "continuous_on (cbox s0 s1) g" |
|
491 |
assumes ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i" |
|
492 |
shows "ext_cont f t0 t1 = ext_cont g s0 s1" |
|
493 |
unfolding assms ext_cont_def |
|
494 |
using assms clamp_in_interval[OF ord] |
|
495 |
by (subst Rep_bcontfun_inject[symmetric]) simp |
|
496 |
||
497 |
end |