author  hoelzl 
Mon, 08 Aug 2016 14:13:14 +0200  
changeset 63627  6ddb43c6b711 
parent 63594  src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy@bd218a9320b5 
child 64267  b9a1486e79be 
permissions  rwrr 
60420  1 
section \<open>Bounded Continuous Functions\<close> 
60421  2 

59453  3 
theory Bounded_Continuous_Function 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
62379
diff
changeset

4 
imports Henstock_Kurzweil_Integration 
59453  5 
begin 
6 

60421  7 
subsection \<open>Definition\<close> 
59453  8 

60421  9 
definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set" 
10 
where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}" 

59453  11 

61260  12 
typedef (overloaded) ('a, 'b) bcontfun = 
13 
"bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set" 

59453  14 
by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def) 
15 

16 
lemma bcontfunE: 

17 
assumes "f \<in> bcontfun" 

18 
obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y" 

19 
using assms unfolding bcontfun_def 

20 
by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI) 

21 

22 
lemma bcontfunE': 

23 
assumes "f \<in> bcontfun" 

24 
obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y" 

25 
using assms bcontfunE 

26 
by metis 

27 

60421  28 
lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun" 
59453  29 
unfolding bcontfun_def 
30 
by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE) 

31 

60421  32 
lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun" 
59453  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 

62101  39 
(* TODO: Generalize to uniform spaces? *) 
59453  40 
instantiation bcontfun :: (topological_space, metric_space) metric_space 
41 
begin 

42 

60421  43 
definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real" 
44 
where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))" 

59453  45 

62101  46 
definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter" 
47 
where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})" 

48 

60421  49 
definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool" 
62101  50 
where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)" 
59453  51 

52 
lemma dist_bounded: 

60421  53 
fixes f :: "('a, 'b) bcontfun" 
59453  54 
shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g" 
55 
proof  

60421  56 
have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun) 
59453  57 
from bcontfunE'[OF this] obtain y where y: 
58 
"continuous_on UNIV (Rep_bcontfun f)" 

59 
"\<And>x. dist (Rep_bcontfun f x) undefined \<le> y" 

60 
by auto 

60421  61 
have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun) 
59453  62 
from bcontfunE'[OF this] obtain z where z: 
63 
"continuous_on UNIV (Rep_bcontfun g)" 

64 
"\<And>x. dist (Rep_bcontfun g x) undefined \<le> z" 

65 
by auto 

60421  66 
show ?thesis 
67 
unfolding dist_bcontfun_def 

59453  68 
proof (intro cSUP_upper bdd_aboveI2) 
69 
fix x 

60421  70 
have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> 
71 
dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined" 

59453  72 
by (rule dist_triangle2) 
60421  73 
also have "\<dots> \<le> y + z" 
74 
using y(2)[of x] z(2)[of x] by (rule add_mono) 

59453  75 
finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" . 
76 
qed simp 

77 
qed 

78 

79 
lemma dist_bound: 

60421  80 
fixes f :: "('a, 'b) bcontfun" 
59453  81 
assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b" 
82 
shows "dist f g \<le> b" 

83 
using assms by (auto simp: dist_bcontfun_def intro: cSUP_least) 

84 

85 
lemma dist_bounded_Abs: 

60421  86 
fixes f g :: "'a \<Rightarrow> 'b" 
59453  87 
assumes "f \<in> bcontfun" "g \<in> bcontfun" 
88 
shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)" 

89 
by (metis Abs_bcontfun_inverse assms dist_bounded) 

90 

91 
lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun" 

92 
by (auto intro: bcontfunI continuous_on_const) 

93 

94 
lemma dist_fun_lt_imp_dist_val_lt: 

95 
assumes "dist f g < e" 

96 
shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e" 

97 
using dist_bounded assms by (rule le_less_trans) 

98 

99 
lemma dist_val_lt_imp_dist_fun_le: 

100 
assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e" 

101 
shows "dist f g \<le> e" 

60421  102 
unfolding dist_bcontfun_def 
59453  103 
proof (intro cSUP_least) 
104 
fix x 

105 
show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e" 

106 
using assms[THEN spec[where x=x]] by (simp add: dist_norm) 

60421  107 
qed simp 
59453  108 

109 
instance 

110 
proof 

60421  111 
fix f g h :: "('a, 'b) bcontfun" 
59453  112 
show "dist f g = 0 \<longleftrightarrow> f = g" 
113 
proof 

60421  114 
have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g" 
115 
by (rule dist_bounded) 

59453  116 
also assume "dist f g = 0" 
60421  117 
finally show "f = g" 
118 
by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse) 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62101
diff
changeset

119 
qed (auto simp: dist_bcontfun_def intro!: cSup_eq) 
59453  120 
show "dist f g \<le> dist f h + dist g h" 
121 
proof (subst dist_bcontfun_def, safe intro!: cSUP_least) 

122 
fix x 

123 
have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> 

124 
dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)" 

125 
by (rule dist_triangle2) 

60421  126 
also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h" 
127 
by (rule dist_bounded) 

128 
also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h" 

129 
by (rule dist_bounded) 

130 
finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h" 

131 
by simp 

59453  132 
qed 
62101  133 
qed (rule open_bcontfun_def uniformity_bcontfun_def)+ 
60421  134 

59453  135 
end 
136 

137 
lemma closed_Pi_bcontfun: 

60421  138 
fixes I :: "'a::metric_space set" 
139 
and X :: "'a \<Rightarrow> 'b::complete_space set" 

59453  140 
assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)" 
141 
shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))" 

142 
unfolding closed_sequential_limits 

143 
proof safe 

144 
fix f l 

61969  145 
assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l" 
59453  146 
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" 
147 
using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim] 

60421  148 
by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified]) 
59453  149 
(metis dist_fun_lt_imp_dist_val_lt)+ 
150 
show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" 

151 
proof (rule, safe) 

152 
fix x assume "x \<in> I" 

60421  153 
then have "closed (X x)" 
154 
using assms by simp 

59453  155 
moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially" 
156 
proof (rule always_eventually, safe) 

157 
fix i 

60420  158 
from seq[THEN spec, of i] \<open>x \<in> I\<close> 
59453  159 
show "Rep_bcontfun (f i) x \<in> X x" 
160 
by (auto simp: Abs_bcontfun_inverse) 

161 
qed 

162 
moreover note sequentially_bot 

61969  163 
moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x" 
59453  164 
using lim_fun by (blast intro!: metric_LIMSEQ_I) 
165 
ultimately show "Rep_bcontfun l x \<in> X x" 

166 
by (rule Lim_in_closed_set) 

167 
qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse) 

168 
qed 

169 

60421  170 

60420  171 
subsection \<open>Complete Space\<close> 
59453  172 

173 
instance bcontfun :: (metric_space, complete_space) complete_space 

174 
proof 

60421  175 
fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun" 
61808  176 
assume "Cauchy f" \<comment> \<open>Cauchy equals uniform convergence\<close> 
59453  177 
then obtain g where limit_function: 
178 
"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e" 

179 
using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" 

180 
"\<lambda>n. Rep_bcontfun (f n)"] 

60421  181 
unfolding Cauchy_def 
182 
by (metis dist_fun_lt_imp_dist_val_lt) 

59453  183 

61808  184 
then obtain N where fg_dist: \<comment> \<open>for an upper bound on @{term g}\<close> 
59453  185 
"\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1" 
186 
by (force simp add: dist_commute) 

187 
from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where 

60421  188 
f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b" 
189 
by force 

61808  190 
have "g \<in> bcontfun" \<comment> \<open>The limit function is bounded and continuous\<close> 
59453  191 
proof (intro bcontfunI) 
192 
show "continuous_on UNIV g" 

193 
using bcontfunE[OF Rep_bcontfun] limit_function 

60421  194 
by (intro continuous_uniform_limit[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"]) 
195 
(auto simp add: eventually_sequentially trivial_limit_def dist_norm) 

59453  196 
next 
197 
fix x 

198 
from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1" 

199 
by (simp add: dist_norm norm_minus_commute) 

200 
with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"] 

201 
show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x] 

202 
by simp 

203 
qed 

204 
show "convergent f" 

60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59865
diff
changeset

205 
proof (rule convergentI, subst lim_sequentially, safe) 
61808  206 
\<comment> \<open>The limit function converges according to its norm\<close> 
60421  207 
fix e :: real 
208 
assume "e > 0" 

209 
then have "e/2 > 0" by simp 

59453  210 
with limit_function[THEN spec, of"e/2"] 
211 
have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2" 

212 
by simp 

213 
then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto 

214 
show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e" 

215 
proof (rule, safe) 

216 
fix n 

217 
assume "N \<le> n" 

218 
with N show "dist (f n) (Abs_bcontfun g) < e" 

219 
using dist_val_lt_imp_dist_fun_le[of 

220 
"f n" "Abs_bcontfun g" "e/2"] 

60420  221 
Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp 
59453  222 
qed 
223 
qed 

224 
qed 

225 

60421  226 

227 
subsection \<open>Supremum norm for a normed vector space\<close> 

59453  228 

229 
instantiation bcontfun :: (topological_space, real_normed_vector) real_vector 

230 
begin 

231 

232 
definition "f = Abs_bcontfun (\<lambda>x. (Rep_bcontfun f x))" 

233 

234 
definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)" 

235 

236 
definition "f  g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x  Rep_bcontfun g x)" 

237 

238 
definition "0 = Abs_bcontfun (\<lambda>x. 0)" 

239 

240 
definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)" 

241 

242 
lemma plus_cont: 

60421  243 
fixes f g :: "'a \<Rightarrow> 'b" 
244 
assumes f: "f \<in> bcontfun" 

245 
and g: "g \<in> bcontfun" 

59453  246 
shows "(\<lambda>x. f x + g x) \<in> bcontfun" 
247 
proof  

248 
from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y" 

249 
by auto 

250 
moreover 

251 
from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z" 

252 
by auto 

253 
ultimately show ?thesis 

254 
proof (intro bcontfunI) 

255 
fix x 

60421  256 
have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)" 
257 
by simp 

258 
also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0" 

259 
by (rule dist_triangle_add) 

59453  260 
also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" 
261 
unfolding zero_bcontfun_def using assms 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

262 
by (metis add_mono const_bcontfun dist_bounded_Abs) 
60421  263 
finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" . 
59453  264 
qed (simp add: continuous_on_add) 
265 
qed 

266 

267 
lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x" 

268 
by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun) 

269 

270 
lemma uminus_cont: 

60421  271 
fixes f :: "'a \<Rightarrow> 'b" 
59453  272 
assumes "f \<in> bcontfun" 
273 
shows "(\<lambda>x.  f x) \<in> bcontfun" 

274 
proof  

60421  275 
from bcontfunE[OF assms, of 0] obtain y 
276 
where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y" 

59453  277 
by auto 
60421  278 
then show ?thesis 
59453  279 
proof (intro bcontfunI) 
280 
fix x 

281 
assume "\<And>x. dist (f x) 0 \<le> y" 

60421  282 
then show "dist ( f x) 0 \<le> y" 
283 
by (subst dist_minus[symmetric]) simp 

59453  284 
qed (simp add: continuous_on_minus) 
285 
qed 

286 

60421  287 
lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun ( f) x =  Rep_bcontfun f x" 
59453  288 
by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun) 
289 

290 
lemma minus_cont: 

60421  291 
fixes f g :: "'a \<Rightarrow> 'b" 
292 
assumes f: "f \<in> bcontfun" 

293 
and g: "g \<in> bcontfun" 

59453  294 
shows "(\<lambda>x. f x  g x) \<in> bcontfun" 
60421  295 
using plus_cont [of f " g"] assms 
296 
by (simp add: uminus_cont fun_Compl_def) 

59453  297 

60421  298 
lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f  g) x = Rep_bcontfun f x  Rep_bcontfun g x" 
59453  299 
by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun) 
300 

301 
lemma scaleR_cont: 

60421  302 
fixes a :: real 
303 
and f :: "'a \<Rightarrow> 'b" 

59453  304 
assumes "f \<in> bcontfun" 
305 
shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun" 

306 
proof  

60421  307 
from bcontfunE[OF assms, of 0] obtain y 
308 
where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y" 

59453  309 
by auto 
60421  310 
then show ?thesis 
59453  311 
proof (intro bcontfunI) 
60421  312 
fix x 
313 
assume "\<And>x. dist (f x) 0 \<le> y" 

61945  314 
then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y" 
59554
4044f53326c9
inlined rules to free userspace from technical names
haftmann
parents:
59453
diff
changeset

315 
by (metis norm_cmul_rule_thm norm_conv_dist) 
59453  316 
qed (simp add: continuous_intros) 
317 
qed 

318 

60421  319 
lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x" 
59453  320 
by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun) 
321 

322 
instance 

61169  323 
by standard 
60421  324 
(simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def 
325 
Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps 

326 
plus_cont const_bcontfun minus_cont scaleR_cont) 

327 

59453  328 
end 
329 

330 
instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector 

331 
begin 

332 

60421  333 
definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real" 
334 
where "norm_bcontfun f = dist f 0" 

59453  335 

336 
definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f" 

337 

338 
instance 

339 
proof 

60421  340 
fix a :: real 
341 
fix f g :: "('a, 'b) bcontfun" 

59453  342 
show "dist f g = norm (f  g)" 
343 
by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

344 
Abs_bcontfun_inverse const_bcontfun dist_norm) 
59453  345 
show "norm (f + g) \<le> norm f + norm g" 
346 
unfolding norm_bcontfun_def 

347 
proof (subst dist_bcontfun_def, safe intro!: cSUP_least) 

348 
fix x 

349 
have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> 

350 
dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0" 

351 
by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm 

352 
le_less_linear less_irrefl norm_triangle_lt) 

353 
also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0" 

354 
using dist_bounded[of f x 0] 

355 
by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def) 

356 
also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0] 

357 
by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def) 

358 
finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp 

359 
qed 

360 
show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f" 

361 
proof  

362 
have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) = 

363 
(SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)" 

364 
proof (intro continuous_at_Sup_mono bdd_aboveI2) 

365 
fix x 

366 
show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0] 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

367 
by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def 
59453  368 
const_bcontfun) 
369 
qed (auto intro!: monoI mult_left_mono continuous_intros) 

370 
moreover 

60421  371 
have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) = 
59453  372 
(\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))" 
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

373 
by auto 
59453  374 
ultimately 
375 
show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f" 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

376 
by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

377 
zero_bcontfun_def const_bcontfun image_image) 
59453  378 
qed 
379 
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def) 

380 

381 
end 

382 

60421  383 
lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun" 
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

384 
by (metis bcontfunI dist_0_norm dist_commute) 
59453  385 

386 
lemma norm_bounded: 

60421  387 
fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun" 
59453  388 
shows "norm (Rep_bcontfun f x) \<le> norm f" 
389 
using dist_bounded[of f x 0] 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

390 
by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def 
59453  391 
const_bcontfun) 
392 

393 
lemma norm_bound: 

60421  394 
fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun" 
59453  395 
assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b" 
396 
shows "norm f \<le> b" 

397 
using dist_bound[of f 0 b] assms 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

398 
by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun) 
59453  399 

400 

60421  401 
subsection \<open>Continuously Extended Functions\<close> 
402 

403 
definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where 

59453  404 
"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)" 
405 

60421  406 
definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun" 
59453  407 
where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))" 
408 

409 
lemma ext_cont_def': 

410 
"ext_cont f a b = Abs_bcontfun (\<lambda>x. 

411 
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))" 

60421  412 
unfolding ext_cont_def clamp_def .. 
59453  413 

414 
lemma clamp_in_interval: 

415 
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" 

416 
shows "clamp a b x \<in> cbox a b" 

417 
unfolding clamp_def 

418 
using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def) 

419 

420 
lemma dist_clamps_le_dist_args: 

60421  421 
fixes x :: "'a::euclidean_space" 
59453  422 
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" 
423 
shows "dist (clamp a b y) (clamp a b x) \<le> dist y x" 

424 
proof  

60421  425 
from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)" 
426 
by (simp add: cbox_def) 

427 
then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le> 

428 
(\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)" 

429 
by (auto intro!: setsum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric]) 

430 
then show ?thesis 

431 
by (auto intro: real_sqrt_le_mono 

432 
simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def) 

59453  433 
qed 
434 

435 
lemma clamp_continuous_at: 

60421  436 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space" 
437 
and x :: 'a 

59453  438 
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" 
60421  439 
and f_cont: "continuous_on (cbox a b) f" 
59453  440 
shows "continuous (at x) (\<lambda>x. f (clamp a b x))" 
60421  441 
unfolding continuous_at_eps_delta 
442 
proof safe 

443 
fix x :: 'a 

444 
fix e :: real 

445 
assume "e > 0" 

446 
moreover have "clamp a b x \<in> cbox a b" 

447 
by (simp add: clamp_in_interval assms) 

448 
moreover note f_cont[simplified continuous_on_iff] 

59453  449 
ultimately 
450 
obtain d where d: "0 < d" 

451 
"\<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" 

452 
by force 

453 
show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow> 

454 
dist (f (clamp a b x')) (f (clamp a b x)) < e" 

455 
by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans]) 

456 
qed 

457 

458 
lemma clamp_continuous_on: 

60421  459 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space" 
59453  460 
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" 
60421  461 
and f_cont: "continuous_on (cbox a b) f" 
59453  462 
shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))" 
463 
using assms 

464 
by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at) 

465 

466 
lemma clamp_bcontfun: 

60421  467 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" 
59453  468 
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" 
60421  469 
and continuous: "continuous_on (cbox a b) f" 
59453  470 
shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun" 
471 
proof  

60421  472 
have "bounded (f ` (cbox a b))" 
473 
by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded]) 

474 
then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c" 

475 
by (auto simp add: bounded_pos) 

59453  476 
show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun" 
477 
proof (intro bcontfun_normI) 

478 
fix x 

60421  479 
show "norm (f (clamp a b x)) \<le> c" 
480 
using clamp_in_interval[OF assms(1), of x] f_bound 

481 
by (simp add: ext_cont_def) 

59453  482 
qed (simp add: clamp_continuous_on assms) 
483 
qed 

484 

485 
lemma integral_clamp: 

486 
"integral {t0::real..clamp t0 t1 x} f = 

487 
(if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)" 

488 
by (auto simp: clamp_def) 

489 

490 

491 
declare [[coercion Rep_bcontfun]] 

492 

493 
lemma ext_cont_cancel[simp]: 

60421  494 
fixes x a b :: "'a::euclidean_space" 
59453  495 
assumes x: "x \<in> cbox a b" 
60421  496 
and "continuous_on (cbox a b) f" 
59453  497 
shows "ext_cont f a b x = f x" 
498 
using assms 

499 
unfolding ext_cont_def 

500 
proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun]) 

501 
show "f (clamp a b x) = f x" 

502 
using x unfolding clamp_def mem_box 

503 
by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less) 

504 
qed (auto simp: cbox_def) 

505 

506 
lemma ext_cont_cong: 

507 
assumes "t0 = s0" 

60421  508 
and "t1 = s1" 
509 
and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t" 

510 
and "continuous_on (cbox t0 t1) f" 

511 
and "continuous_on (cbox s0 s1) g" 

512 
and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i" 

59453  513 
shows "ext_cont f t0 t1 = ext_cont g s0 s1" 
514 
unfolding assms ext_cont_def 

515 
using assms clamp_in_interval[OF ord] 

516 
by (subst Rep_bcontfun_inject[symmetric]) simp 

517 

518 
end 