src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
changeset 63627 6ddb43c6b711
parent 63626 44ce6b524ff3
child 63631 2edc8da89edc
child 63633 2accfb71e33b
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Aug 05 18:34:57 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,518 +0,0 @@
     1.4 -section \<open>Bounded Continuous Functions\<close>
     1.5 -
     1.6 -theory Bounded_Continuous_Function
     1.7 -imports Henstock_Kurzweil_Integration
     1.8 -begin
     1.9 -
    1.10 -subsection \<open>Definition\<close>
    1.11 -
    1.12 -definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
    1.13 -  where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
    1.14 -
    1.15 -typedef (overloaded) ('a, 'b) bcontfun =
    1.16 -    "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
    1.17 -  by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
    1.18 -
    1.19 -lemma bcontfunE:
    1.20 -  assumes "f \<in> bcontfun"
    1.21 -  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y"
    1.22 -  using assms unfolding bcontfun_def
    1.23 -  by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI)
    1.24 -
    1.25 -lemma bcontfunE':
    1.26 -  assumes "f \<in> bcontfun"
    1.27 -  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
    1.28 -  using assms bcontfunE
    1.29 -  by metis
    1.30 -
    1.31 -lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
    1.32 -  unfolding bcontfun_def
    1.33 -  by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)
    1.34 -
    1.35 -lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun"
    1.36 -  using bcontfunI by metis
    1.37 -
    1.38 -lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)"
    1.39 -  using Rep_bcontfun[of x]
    1.40 -  by (auto simp: bcontfun_def intro: continuous_on_subset)
    1.41 -
    1.42 -(* TODO: Generalize to uniform spaces? *)
    1.43 -instantiation bcontfun :: (topological_space, metric_space) metric_space
    1.44 -begin
    1.45 -
    1.46 -definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
    1.47 -  where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
    1.48 -
    1.49 -definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
    1.50 -  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.51 -
    1.52 -definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
    1.53 -  where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    1.54 -
    1.55 -lemma dist_bounded:
    1.56 -  fixes f :: "('a, 'b) bcontfun"
    1.57 -  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
    1.58 -proof -
    1.59 -  have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun)
    1.60 -  from bcontfunE'[OF this] obtain y where y:
    1.61 -    "continuous_on UNIV (Rep_bcontfun f)"
    1.62 -    "\<And>x. dist (Rep_bcontfun f x) undefined \<le> y"
    1.63 -    by auto
    1.64 -  have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun)
    1.65 -  from bcontfunE'[OF this] obtain z where z:
    1.66 -    "continuous_on UNIV (Rep_bcontfun g)"
    1.67 -    "\<And>x. dist (Rep_bcontfun g x) undefined \<le> z"
    1.68 -    by auto
    1.69 -  show ?thesis
    1.70 -    unfolding dist_bcontfun_def
    1.71 -  proof (intro cSUP_upper bdd_aboveI2)
    1.72 -    fix x
    1.73 -    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
    1.74 -      dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
    1.75 -      by (rule dist_triangle2)
    1.76 -    also have "\<dots> \<le> y + z"
    1.77 -      using y(2)[of x] z(2)[of x] by (rule add_mono)
    1.78 -    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" .
    1.79 -  qed simp
    1.80 -qed
    1.81 -
    1.82 -lemma dist_bound:
    1.83 -  fixes f :: "('a, 'b) bcontfun"
    1.84 -  assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b"
    1.85 -  shows "dist f g \<le> b"
    1.86 -  using assms by (auto simp: dist_bcontfun_def intro: cSUP_least)
    1.87 -
    1.88 -lemma dist_bounded_Abs:
    1.89 -  fixes f g :: "'a \<Rightarrow> 'b"
    1.90 -  assumes "f \<in> bcontfun" "g \<in> bcontfun"
    1.91 -  shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)"
    1.92 -  by (metis Abs_bcontfun_inverse assms dist_bounded)
    1.93 -
    1.94 -lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun"
    1.95 -  by (auto intro: bcontfunI continuous_on_const)
    1.96 -
    1.97 -lemma dist_fun_lt_imp_dist_val_lt:
    1.98 -  assumes "dist f g < e"
    1.99 -  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
   1.100 -  using dist_bounded assms by (rule le_less_trans)
   1.101 -
   1.102 -lemma dist_val_lt_imp_dist_fun_le:
   1.103 -  assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
   1.104 -  shows "dist f g \<le> e"
   1.105 -  unfolding dist_bcontfun_def
   1.106 -proof (intro cSUP_least)
   1.107 -  fix x
   1.108 -  show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e"
   1.109 -    using assms[THEN spec[where x=x]] by (simp add: dist_norm)
   1.110 -qed simp
   1.111 -
   1.112 -instance
   1.113 -proof
   1.114 -  fix f g h :: "('a, 'b) bcontfun"
   1.115 -  show "dist f g = 0 \<longleftrightarrow> f = g"
   1.116 -  proof
   1.117 -    have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
   1.118 -      by (rule dist_bounded)
   1.119 -    also assume "dist f g = 0"
   1.120 -    finally show "f = g"
   1.121 -      by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
   1.122 -  qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
   1.123 -  show "dist f g \<le> dist f h + dist g h"
   1.124 -  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
   1.125 -    fix x
   1.126 -    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
   1.127 -      dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)"
   1.128 -      by (rule dist_triangle2)
   1.129 -    also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h"
   1.130 -      by (rule dist_bounded)
   1.131 -    also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h"
   1.132 -      by (rule dist_bounded)
   1.133 -    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
   1.134 -      by simp
   1.135 -  qed
   1.136 -qed (rule open_bcontfun_def uniformity_bcontfun_def)+
   1.137 -
   1.138 -end
   1.139 -
   1.140 -lemma closed_Pi_bcontfun:
   1.141 -  fixes I :: "'a::metric_space set"
   1.142 -    and X :: "'a \<Rightarrow> 'b::complete_space set"
   1.143 -  assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
   1.144 -  shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))"
   1.145 -  unfolding closed_sequential_limits
   1.146 -proof safe
   1.147 -  fix f l
   1.148 -  assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l"
   1.149 -  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"
   1.150 -    using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
   1.151 -    by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
   1.152 -      (metis dist_fun_lt_imp_dist_val_lt)+
   1.153 -  show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)"
   1.154 -  proof (rule, safe)
   1.155 -    fix x assume "x \<in> I"
   1.156 -    then have "closed (X x)"
   1.157 -      using assms by simp
   1.158 -    moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially"
   1.159 -    proof (rule always_eventually, safe)
   1.160 -      fix i
   1.161 -      from seq[THEN spec, of i] \<open>x \<in> I\<close>
   1.162 -      show "Rep_bcontfun (f i) x \<in> X x"
   1.163 -        by (auto simp: Abs_bcontfun_inverse)
   1.164 -    qed
   1.165 -    moreover note sequentially_bot
   1.166 -    moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x"
   1.167 -      using lim_fun by (blast intro!: metric_LIMSEQ_I)
   1.168 -    ultimately show "Rep_bcontfun l x \<in> X x"
   1.169 -      by (rule Lim_in_closed_set)
   1.170 -  qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse)
   1.171 -qed
   1.172 -
   1.173 -
   1.174 -subsection \<open>Complete Space\<close>
   1.175 -
   1.176 -instance bcontfun :: (metric_space, complete_space) complete_space
   1.177 -proof
   1.178 -  fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
   1.179 -  assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
   1.180 -  then obtain g where limit_function:
   1.181 -    "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e"
   1.182 -    using uniformly_convergent_eq_cauchy[of "\<lambda>_. True"
   1.183 -      "\<lambda>n. Rep_bcontfun (f n)"]
   1.184 -    unfolding Cauchy_def
   1.185 -    by (metis dist_fun_lt_imp_dist_val_lt)
   1.186 -
   1.187 -  then obtain N where fg_dist:  \<comment> \<open>for an upper bound on @{term g}\<close>
   1.188 -    "\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1"
   1.189 -    by (force simp add: dist_commute)
   1.190 -  from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where
   1.191 -    f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b"
   1.192 -    by force
   1.193 -  have "g \<in> bcontfun"  \<comment> \<open>The limit function is bounded and continuous\<close>
   1.194 -  proof (intro bcontfunI)
   1.195 -    show "continuous_on UNIV g"
   1.196 -      using bcontfunE[OF Rep_bcontfun] limit_function
   1.197 -      by (intro continuous_uniform_limit[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
   1.198 -        (auto simp add: eventually_sequentially trivial_limit_def dist_norm)
   1.199 -  next
   1.200 -    fix x
   1.201 -    from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
   1.202 -      by (simp add: dist_norm norm_minus_commute)
   1.203 -    with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"]
   1.204 -    show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x]
   1.205 -      by simp
   1.206 -  qed
   1.207 -  show "convergent f"
   1.208 -  proof (rule convergentI, subst lim_sequentially, safe)
   1.209 -    \<comment> \<open>The limit function converges according to its norm\<close>
   1.210 -    fix e :: real
   1.211 -    assume "e > 0"
   1.212 -    then have "e/2 > 0" by simp
   1.213 -    with limit_function[THEN spec, of"e/2"]
   1.214 -    have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2"
   1.215 -      by simp
   1.216 -    then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto
   1.217 -    show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e"
   1.218 -    proof (rule, safe)
   1.219 -      fix n
   1.220 -      assume "N \<le> n"
   1.221 -      with N show "dist (f n) (Abs_bcontfun g) < e"
   1.222 -        using dist_val_lt_imp_dist_fun_le[of
   1.223 -          "f n" "Abs_bcontfun g" "e/2"]
   1.224 -          Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp
   1.225 -    qed
   1.226 -  qed
   1.227 -qed
   1.228 -
   1.229 -
   1.230 -subsection \<open>Supremum norm for a normed vector space\<close>
   1.231 -
   1.232 -instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
   1.233 -begin
   1.234 -
   1.235 -definition "-f = Abs_bcontfun (\<lambda>x. -(Rep_bcontfun f x))"
   1.236 -
   1.237 -definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)"
   1.238 -
   1.239 -definition "f - g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x - Rep_bcontfun g x)"
   1.240 -
   1.241 -definition "0 = Abs_bcontfun (\<lambda>x. 0)"
   1.242 -
   1.243 -definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)"
   1.244 -
   1.245 -lemma plus_cont:
   1.246 -  fixes f g :: "'a \<Rightarrow> 'b"
   1.247 -  assumes f: "f \<in> bcontfun"
   1.248 -    and g: "g \<in> bcontfun"
   1.249 -  shows "(\<lambda>x. f x + g x) \<in> bcontfun"
   1.250 -proof -
   1.251 -  from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
   1.252 -    by auto
   1.253 -  moreover
   1.254 -  from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z"
   1.255 -    by auto
   1.256 -  ultimately show ?thesis
   1.257 -  proof (intro bcontfunI)
   1.258 -    fix x
   1.259 -    have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)"
   1.260 -      by simp
   1.261 -    also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0"
   1.262 -      by (rule dist_triangle_add)
   1.263 -    also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
   1.264 -      unfolding zero_bcontfun_def using assms
   1.265 -      by (metis add_mono const_bcontfun dist_bounded_Abs)
   1.266 -    finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
   1.267 -  qed (simp add: continuous_on_add)
   1.268 -qed
   1.269 -
   1.270 -lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x"
   1.271 -  by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun)
   1.272 -
   1.273 -lemma uminus_cont:
   1.274 -  fixes f :: "'a \<Rightarrow> 'b"
   1.275 -  assumes "f \<in> bcontfun"
   1.276 -  shows "(\<lambda>x. - f x) \<in> bcontfun"
   1.277 -proof -
   1.278 -  from bcontfunE[OF assms, of 0] obtain y
   1.279 -    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
   1.280 -    by auto
   1.281 -  then show ?thesis
   1.282 -  proof (intro bcontfunI)
   1.283 -    fix x
   1.284 -    assume "\<And>x. dist (f x) 0 \<le> y"
   1.285 -    then show "dist (- f x) 0 \<le> y"
   1.286 -      by (subst dist_minus[symmetric]) simp
   1.287 -  qed (simp add: continuous_on_minus)
   1.288 -qed
   1.289 -
   1.290 -lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
   1.291 -  by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)
   1.292 -
   1.293 -lemma minus_cont:
   1.294 -  fixes f g :: "'a \<Rightarrow> 'b"
   1.295 -  assumes f: "f \<in> bcontfun"
   1.296 -    and g: "g \<in> bcontfun"
   1.297 -  shows "(\<lambda>x. f x - g x) \<in> bcontfun"
   1.298 -  using plus_cont [of f "- g"] assms
   1.299 -  by (simp add: uminus_cont fun_Compl_def)
   1.300 -
   1.301 -lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
   1.302 -  by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)
   1.303 -
   1.304 -lemma scaleR_cont:
   1.305 -  fixes a :: real
   1.306 -    and f :: "'a \<Rightarrow> 'b"
   1.307 -  assumes "f \<in> bcontfun"
   1.308 -  shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun"
   1.309 -proof -
   1.310 -  from bcontfunE[OF assms, of 0] obtain y
   1.311 -    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
   1.312 -    by auto
   1.313 -  then show ?thesis
   1.314 -  proof (intro bcontfunI)
   1.315 -    fix x
   1.316 -    assume "\<And>x. dist (f x) 0 \<le> y"
   1.317 -    then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
   1.318 -      by (metis norm_cmul_rule_thm norm_conv_dist)
   1.319 -  qed (simp add: continuous_intros)
   1.320 -qed
   1.321 -
   1.322 -lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
   1.323 -  by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
   1.324 -
   1.325 -instance
   1.326 -  by standard
   1.327 -    (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
   1.328 -      Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
   1.329 -      plus_cont const_bcontfun minus_cont scaleR_cont)
   1.330 -
   1.331 -end
   1.332 -
   1.333 -instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
   1.334 -begin
   1.335 -
   1.336 -definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
   1.337 -  where "norm_bcontfun f = dist f 0"
   1.338 -
   1.339 -definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f"
   1.340 -
   1.341 -instance
   1.342 -proof
   1.343 -  fix a :: real
   1.344 -  fix f g :: "('a, 'b) bcontfun"
   1.345 -  show "dist f g = norm (f - g)"
   1.346 -    by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
   1.347 -      Abs_bcontfun_inverse const_bcontfun dist_norm)
   1.348 -  show "norm (f + g) \<le> norm f + norm g"
   1.349 -    unfolding norm_bcontfun_def
   1.350 -  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
   1.351 -    fix x
   1.352 -    have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le>
   1.353 -      dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0"
   1.354 -      by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm
   1.355 -        le_less_linear less_irrefl norm_triangle_lt)
   1.356 -    also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0"
   1.357 -      using dist_bounded[of f x 0]
   1.358 -      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
   1.359 -    also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0]
   1.360 -      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
   1.361 -    finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp
   1.362 -  qed
   1.363 -  show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   1.364 -  proof -
   1.365 -    have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) =
   1.366 -      (SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)"
   1.367 -    proof (intro continuous_at_Sup_mono bdd_aboveI2)
   1.368 -      fix x
   1.369 -      show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0]
   1.370 -        by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
   1.371 -          const_bcontfun)
   1.372 -    qed (auto intro!: monoI mult_left_mono continuous_intros)
   1.373 -    moreover
   1.374 -    have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
   1.375 -      (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
   1.376 -      by auto
   1.377 -    ultimately
   1.378 -    show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   1.379 -      by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse
   1.380 -        zero_bcontfun_def const_bcontfun image_image)
   1.381 -  qed
   1.382 -qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
   1.383 -
   1.384 -end
   1.385 -
   1.386 -lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
   1.387 -  by (metis bcontfunI dist_0_norm dist_commute)
   1.388 -
   1.389 -lemma norm_bounded:
   1.390 -  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   1.391 -  shows "norm (Rep_bcontfun f x) \<le> norm f"
   1.392 -  using dist_bounded[of f x 0]
   1.393 -  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
   1.394 -    const_bcontfun)
   1.395 -
   1.396 -lemma norm_bound:
   1.397 -  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   1.398 -  assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
   1.399 -  shows "norm f \<le> b"
   1.400 -  using dist_bound[of f 0 b] assms
   1.401 -  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun)
   1.402 -
   1.403 -
   1.404 -subsection \<open>Continuously Extended Functions\<close>
   1.405 -
   1.406 -definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.407 -  "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)"
   1.408 -
   1.409 -definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
   1.410 -  where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))"
   1.411 -
   1.412 -lemma ext_cont_def':
   1.413 -  "ext_cont f a b = Abs_bcontfun (\<lambda>x.
   1.414 -    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))"
   1.415 -  unfolding ext_cont_def clamp_def ..
   1.416 -
   1.417 -lemma clamp_in_interval:
   1.418 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.419 -  shows "clamp a b x \<in> cbox a b"
   1.420 -  unfolding clamp_def
   1.421 -  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
   1.422 -
   1.423 -lemma dist_clamps_le_dist_args:
   1.424 -  fixes x :: "'a::euclidean_space"
   1.425 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.426 -  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
   1.427 -proof -
   1.428 -  from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   1.429 -    by (simp add: cbox_def)
   1.430 -  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
   1.431 -    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
   1.432 -    by (auto intro!: setsum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
   1.433 -  then show ?thesis
   1.434 -    by (auto intro: real_sqrt_le_mono
   1.435 -      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
   1.436 -qed
   1.437 -
   1.438 -lemma clamp_continuous_at:
   1.439 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   1.440 -    and x :: 'a
   1.441 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.442 -    and f_cont: "continuous_on (cbox a b) f"
   1.443 -  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
   1.444 -  unfolding continuous_at_eps_delta
   1.445 -proof safe
   1.446 -  fix x :: 'a
   1.447 -  fix e :: real
   1.448 -  assume "e > 0"
   1.449 -  moreover have "clamp a b x \<in> cbox a b"
   1.450 -    by (simp add: clamp_in_interval assms)
   1.451 -  moreover note f_cont[simplified continuous_on_iff]
   1.452 -  ultimately
   1.453 -  obtain d where d: "0 < d"
   1.454 -    "\<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"
   1.455 -    by force
   1.456 -  show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
   1.457 -    dist (f (clamp a b x')) (f (clamp a b x)) < e"
   1.458 -    by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans])
   1.459 -qed
   1.460 -
   1.461 -lemma clamp_continuous_on:
   1.462 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   1.463 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.464 -    and f_cont: "continuous_on (cbox a b) f"
   1.465 -  shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))"
   1.466 -  using assms
   1.467 -  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
   1.468 -
   1.469 -lemma clamp_bcontfun:
   1.470 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   1.471 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.472 -    and continuous: "continuous_on (cbox a b) f"
   1.473 -  shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
   1.474 -proof -
   1.475 -  have "bounded (f ` (cbox a b))"
   1.476 -    by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
   1.477 -  then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c"
   1.478 -    by (auto simp add: bounded_pos)
   1.479 -  show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
   1.480 -  proof (intro bcontfun_normI)
   1.481 -    fix x
   1.482 -    show "norm (f (clamp a b x)) \<le> c"
   1.483 -      using clamp_in_interval[OF assms(1), of x] f_bound
   1.484 -      by (simp add: ext_cont_def)
   1.485 -  qed (simp add: clamp_continuous_on assms)
   1.486 -qed
   1.487 -
   1.488 -lemma integral_clamp:
   1.489 -  "integral {t0::real..clamp t0 t1 x} f =
   1.490 -    (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
   1.491 -  by (auto simp: clamp_def)
   1.492 -
   1.493 -
   1.494 -declare [[coercion Rep_bcontfun]]
   1.495 -
   1.496 -lemma ext_cont_cancel[simp]:
   1.497 -  fixes x a b :: "'a::euclidean_space"
   1.498 -  assumes x: "x \<in> cbox a b"
   1.499 -    and "continuous_on (cbox a b) f"
   1.500 -  shows "ext_cont f a b x = f x"
   1.501 -  using assms
   1.502 -  unfolding ext_cont_def
   1.503 -proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun])
   1.504 -  show "f (clamp a b x) = f x"
   1.505 -    using x unfolding clamp_def mem_box
   1.506 -    by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less)
   1.507 -qed (auto simp: cbox_def)
   1.508 -
   1.509 -lemma ext_cont_cong:
   1.510 -  assumes "t0 = s0"
   1.511 -    and "t1 = s1"
   1.512 -    and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
   1.513 -    and "continuous_on (cbox t0 t1) f"
   1.514 -    and "continuous_on (cbox s0 s1) g"
   1.515 -    and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
   1.516 -  shows "ext_cont f t0 t1 = ext_cont g s0 s1"
   1.517 -  unfolding assms ext_cont_def
   1.518 -  using assms clamp_in_interval[OF ord]
   1.519 -  by (subst Rep_bcontfun_inject[symmetric]) simp
   1.520 -
   1.521 -end