src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62343 24106dc44def
child 62379 340738057c8c
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 section \<open>Bounded Continuous Functions\<close>
     2 
     3 theory Bounded_Continuous_Function
     4 imports Integration
     5 begin
     6 
     7 subsection \<open>Definition\<close>
     8 
     9 definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
    10   where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
    11 
    12 typedef (overloaded) ('a, 'b) bcontfun =
    13     "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
    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 
    28 lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
    29   unfolding bcontfun_def
    30   by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)
    31 
    32 lemma bcontfunI': "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 (* TODO: Generalize to uniform spaces? *)
    40 instantiation bcontfun :: (topological_space, metric_space) metric_space
    41 begin
    42 
    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))"
    45 
    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 
    49 definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
    50   where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    51 
    52 lemma dist_bounded:
    53   fixes f :: "('a, 'b) bcontfun"
    54   shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
    55 proof -
    56   have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun)
    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
    61   have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun)
    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
    66   show ?thesis
    67     unfolding dist_bcontfun_def
    68   proof (intro cSUP_upper bdd_aboveI2)
    69     fix x
    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"
    72       by (rule dist_triangle2)
    73     also have "\<dots> \<le> y + z"
    74       using y(2)[of x] z(2)[of x] by (rule add_mono)
    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:
    80   fixes f :: "('a, 'b) bcontfun"
    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:
    86   fixes f g :: "'a \<Rightarrow> 'b"
    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"
   102   unfolding dist_bcontfun_def
   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)
   107 qed simp
   108 
   109 instance
   110 proof
   111   fix f g h :: "('a, 'b) bcontfun"
   112   show "dist f g = 0 \<longleftrightarrow> f = g"
   113   proof
   114     have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
   115       by (rule dist_bounded)
   116     also assume "dist f g = 0"
   117     finally show "f = g"
   118       by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
   119   qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
   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)
   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
   132   qed
   133 qed (rule open_bcontfun_def uniformity_bcontfun_def)+
   134 
   135 end
   136 
   137 lemma closed_Pi_bcontfun:
   138   fixes I :: "'a::metric_space set"
   139     and X :: "'a \<Rightarrow> 'b::complete_space set"
   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
   145   assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l"
   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]
   148     by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
   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"
   153     then have "closed (X x)"
   154       using assms by simp
   155     moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially"
   156     proof (rule always_eventually, safe)
   157       fix i
   158       from seq[THEN spec, of i] \<open>x \<in> I\<close>
   159       show "Rep_bcontfun (f i) x \<in> X x"
   160         by (auto simp: Abs_bcontfun_inverse)
   161     qed
   162     moreover note sequentially_bot
   163     moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x"
   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 
   170 
   171 subsection \<open>Complete Space\<close>
   172 
   173 instance bcontfun :: (metric_space, complete_space) complete_space
   174 proof
   175   fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
   176   assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
   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)"]
   181     unfolding Cauchy_def
   182     by (metis dist_fun_lt_imp_dist_val_lt)
   183 
   184   then obtain N where fg_dist:  \<comment> \<open>for an upper bound on @{term g}\<close>
   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
   188     f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b"
   189     by force
   190   have "g \<in> bcontfun"  \<comment> \<open>The limit function is bounded and continuous\<close>
   191   proof (intro bcontfunI)
   192     show "continuous_on UNIV g"
   193       using bcontfunE[OF Rep_bcontfun] limit_function
   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)
   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"
   205   proof (rule convergentI, subst lim_sequentially, safe)
   206     \<comment> \<open>The limit function converges according to its norm\<close>
   207     fix e :: real
   208     assume "e > 0"
   209     then have "e/2 > 0" by simp
   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"]
   221           Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp
   222     qed
   223   qed
   224 qed
   225 
   226 
   227 subsection \<open>Supremum norm for a normed vector space\<close>
   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:
   243   fixes f g :: "'a \<Rightarrow> 'b"
   244   assumes f: "f \<in> bcontfun"
   245     and g: "g \<in> bcontfun"
   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
   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)
   260     also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
   261       unfolding zero_bcontfun_def using assms
   262       by (auto intro!: add_mono dist_bounded_Abs const_bcontfun)
   263     finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
   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:
   271   fixes f :: "'a \<Rightarrow> 'b"
   272   assumes "f \<in> bcontfun"
   273   shows "(\<lambda>x. - f x) \<in> bcontfun"
   274 proof -
   275   from bcontfunE[OF assms, of 0] obtain y
   276     where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
   277     by auto
   278   then show ?thesis
   279   proof (intro bcontfunI)
   280     fix x
   281     assume "\<And>x. dist (f x) 0 \<le> y"
   282     then show "dist (- f x) 0 \<le> y"
   283       by (subst dist_minus[symmetric]) simp
   284   qed (simp add: continuous_on_minus)
   285 qed
   286 
   287 lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
   288   by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)
   289 
   290 lemma minus_cont:
   291   fixes f g :: "'a \<Rightarrow> 'b"
   292   assumes f: "f \<in> bcontfun"
   293     and g: "g \<in> bcontfun"
   294   shows "(\<lambda>x. f x - g x) \<in> bcontfun"
   295   using plus_cont [of f "- g"] assms
   296   by (simp add: uminus_cont fun_Compl_def)
   297 
   298 lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
   299   by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)
   300 
   301 lemma scaleR_cont:
   302   fixes a :: real
   303     and f :: "'a \<Rightarrow> 'b"
   304   assumes "f \<in> bcontfun"
   305   shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun"
   306 proof -
   307   from bcontfunE[OF assms, of 0] obtain y
   308     where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
   309     by auto
   310   then show ?thesis
   311   proof (intro bcontfunI)
   312     fix x
   313     assume "\<And>x. dist (f x) 0 \<le> y"
   314     then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
   315       by (metis norm_cmul_rule_thm norm_conv_dist)
   316   qed (simp add: continuous_intros)
   317 qed
   318 
   319 lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
   320   by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
   321 
   322 instance
   323   by standard
   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 
   328 end
   329 
   330 instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
   331 begin
   332 
   333 definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
   334   where "norm_bcontfun f = dist f 0"
   335 
   336 definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f"
   337 
   338 instance
   339 proof
   340   fix a :: real
   341   fix f g :: "('a, 'b) bcontfun"
   342   show "dist f g = norm (f - g)"
   343     by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
   344       Abs_bcontfun_inverse const_bcontfun norm_conv_dist[symmetric] dist_norm)
   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]
   367         by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
   368           const_bcontfun)
   369     qed (auto intro!: monoI mult_left_mono continuous_intros)
   370     moreover
   371     have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
   372       (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
   373       by (auto simp: norm_conv_dist[symmetric])
   374     ultimately
   375     show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   376       by (simp add: norm_bcontfun_def dist_bcontfun_def norm_conv_dist Abs_bcontfun_inverse
   377         zero_bcontfun_def const_bcontfun image_image) presburger
   378   qed
   379 qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
   380 
   381 end
   382 
   383 lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
   384   unfolding norm_conv_dist
   385   by (auto intro: bcontfunI)
   386 
   387 lemma norm_bounded:
   388   fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   389   shows "norm (Rep_bcontfun f x) \<le> norm f"
   390   using dist_bounded[of f x 0]
   391   by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
   392     const_bcontfun)
   393 
   394 lemma norm_bound:
   395   fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   396   assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
   397   shows "norm f \<le> b"
   398   using dist_bound[of f 0 b] assms
   399   by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
   400     const_bcontfun)
   401 
   402 
   403 subsection \<open>Continuously Extended Functions\<close>
   404 
   405 definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   406   "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)"
   407 
   408 definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
   409   where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))"
   410 
   411 lemma ext_cont_def':
   412   "ext_cont f a b = Abs_bcontfun (\<lambda>x.
   413     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))"
   414   unfolding ext_cont_def clamp_def ..
   415 
   416 lemma clamp_in_interval:
   417   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   418   shows "clamp a b x \<in> cbox a b"
   419   unfolding clamp_def
   420   using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
   421 
   422 lemma dist_clamps_le_dist_args:
   423   fixes x :: "'a::euclidean_space"
   424   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   425   shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
   426 proof -
   427   from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   428     by (simp add: cbox_def)
   429   then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
   430     (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
   431     by (auto intro!: setsum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
   432   then show ?thesis
   433     by (auto intro: real_sqrt_le_mono
   434       simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
   435 qed
   436 
   437 lemma clamp_continuous_at:
   438   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   439     and x :: 'a
   440   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   441     and f_cont: "continuous_on (cbox a b) f"
   442   shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
   443   unfolding continuous_at_eps_delta
   444 proof safe
   445   fix x :: 'a
   446   fix e :: real
   447   assume "e > 0"
   448   moreover have "clamp a b x \<in> cbox a b"
   449     by (simp add: clamp_in_interval assms)
   450   moreover note f_cont[simplified continuous_on_iff]
   451   ultimately
   452   obtain d where d: "0 < d"
   453     "\<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"
   454     by force
   455   show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
   456     dist (f (clamp a b x')) (f (clamp a b x)) < e"
   457     by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans])
   458 qed
   459 
   460 lemma clamp_continuous_on:
   461   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   462   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   463     and f_cont: "continuous_on (cbox a b) f"
   464   shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))"
   465   using assms
   466   by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
   467 
   468 lemma clamp_bcontfun:
   469   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   470   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   471     and continuous: "continuous_on (cbox a b) f"
   472   shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
   473 proof -
   474   have "bounded (f ` (cbox a b))"
   475     by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
   476   then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c"
   477     by (auto simp add: bounded_pos)
   478   show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
   479   proof (intro bcontfun_normI)
   480     fix x
   481     show "norm (f (clamp a b x)) \<le> c"
   482       using clamp_in_interval[OF assms(1), of x] f_bound
   483       by (simp add: ext_cont_def)
   484   qed (simp add: clamp_continuous_on assms)
   485 qed
   486 
   487 lemma integral_clamp:
   488   "integral {t0::real..clamp t0 t1 x} f =
   489     (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
   490   by (auto simp: clamp_def)
   491 
   492 
   493 declare [[coercion Rep_bcontfun]]
   494 
   495 lemma ext_cont_cancel[simp]:
   496   fixes x a b :: "'a::euclidean_space"
   497   assumes x: "x \<in> cbox a b"
   498     and "continuous_on (cbox a b) f"
   499   shows "ext_cont f a b x = f x"
   500   using assms
   501   unfolding ext_cont_def
   502 proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun])
   503   show "f (clamp a b x) = f x"
   504     using x unfolding clamp_def mem_box
   505     by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less)
   506 qed (auto simp: cbox_def)
   507 
   508 lemma ext_cont_cong:
   509   assumes "t0 = s0"
   510     and "t1 = s1"
   511     and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
   512     and "continuous_on (cbox t0 t1) f"
   513     and "continuous_on (cbox s0 s1) g"
   514     and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
   515   shows "ext_cont f t0 t1 = ext_cont g s0 s1"
   516   unfolding assms ext_cont_def
   517   using assms clamp_in_interval[OF ord]
   518   by (subst Rep_bcontfun_inject[symmetric]) simp
   519 
   520 end