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