author immler Fri Mar 10 23:16:40 2017 +0100 (2017-03-10) changeset 65204 d23eded35a33 parent 65203 314246c6eeaa child 65205 f435640193b6
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
```     1.1 --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Sun Mar 12 19:06:10 2017 +0100
1.2 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Mar 10 23:16:40 2017 +0100
1.3 @@ -1,7 +1,8 @@
1.4  section \<open>Bounded Continuous Functions\<close>
1.5
1.6  theory Bounded_Continuous_Function
1.7 -imports Henstock_Kurzweil_Integration
1.8 +  imports
1.9 +    Henstock_Kurzweil_Integration
1.10  begin
1.11
1.12  subsection \<open>Definition\<close>
1.13 @@ -9,162 +10,163 @@
1.14  definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
1.15    where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
1.16
1.17 -typedef (overloaded) ('a, 'b) bcontfun =
1.18 -    "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
1.19 -  by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
1.20 +typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
1.21 +    "{f::'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}"
1.22 +  morphisms apply_bcontfun Bcontfun
1.23 +  by (auto intro: continuous_intros simp: bounded_def)
1.24 +
1.25 +declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
1.26 +
1.27 +setup_lifting type_definition_bcontfun
1.28 +
1.29 +lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
1.30 +  and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
1.31 +  using apply_bcontfun[of x]
1.32 +  by (auto simp: intro: continuous_on_subset)
1.33 +
1.34 +lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
1.35 +  by transfer auto
1.36
1.37  lemma bcontfunE:
1.38 -  assumes "f \<in> bcontfun"
1.39 -  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y"
1.40 -  using assms unfolding bcontfun_def
1.41 -  by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI)
1.42 -
1.43 -lemma bcontfunE':
1.44 -  assumes "f \<in> bcontfun"
1.45 -  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
1.46 -  using assms bcontfunE
1.47 -  by metis
1.48 +  assumes "continuous_on UNIV f" "bounded (range f)"
1.49 +  obtains g where "f = apply_bcontfun g"
1.50 +  by (blast intro: apply_bcontfun_cases assms)
1.51
1.52 -lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
1.53 -  unfolding bcontfun_def
1.54 -  by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)
1.55 -
1.56 -lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun"
1.57 -  using bcontfunI by metis
1.58 -
1.59 -lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)"
1.60 -  using Rep_bcontfun[of x]
1.61 -  by (auto simp: bcontfun_def intro: continuous_on_subset)
1.62 +lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
1.63 +  by (auto intro!: continuous_intros simp: image_def)
1.64
1.65  (* TODO: Generalize to uniform spaces? *)
1.66  instantiation bcontfun :: (topological_space, metric_space) metric_space
1.67  begin
1.68
1.69 -definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
1.70 -  where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
1.71 +lift_definition dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
1.72 +  is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
1.73
1.74 -definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
1.75 +definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
1.76    where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
1.77
1.78 -definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
1.79 +definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
1.80    where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
1.81
1.82 +lemma bounded_dist_le_SUP_dist:
1.83 +  "bounded (range f) \<Longrightarrow> bounded (range g) \<Longrightarrow> dist (f x) (g x) \<le> (SUP x. dist (f x) (g x))"
1.84 +  by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp)
1.85 +
1.86  lemma dist_bounded:
1.87 -  fixes f :: "('a, 'b) bcontfun"
1.88 -  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
1.89 -proof -
1.90 -  have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun)
1.91 -  from bcontfunE'[OF this] obtain y where y:
1.92 -    "continuous_on UNIV (Rep_bcontfun f)"
1.93 -    "\<And>x. dist (Rep_bcontfun f x) undefined \<le> y"
1.94 -    by auto
1.95 -  have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun)
1.96 -  from bcontfunE'[OF this] obtain z where z:
1.97 -    "continuous_on UNIV (Rep_bcontfun g)"
1.98 -    "\<And>x. dist (Rep_bcontfun g x) undefined \<le> z"
1.99 -    by auto
1.100 -  show ?thesis
1.101 -    unfolding dist_bcontfun_def
1.102 -  proof (intro cSUP_upper bdd_aboveI2)
1.103 -    fix x
1.104 -    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
1.105 -      dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
1.106 -      by (rule dist_triangle2)
1.107 -    also have "\<dots> \<le> y + z"
1.108 -      using y(2)[of x] z(2)[of x] by (rule add_mono)
1.109 -    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" .
1.110 -  qed simp
1.111 -qed
1.112 +  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
1.113 +  shows "dist (f x) (g x) \<le> dist f g"
1.114 +  by transfer (auto intro!: bounded_dist_le_SUP_dist)
1.115
1.116  lemma dist_bound:
1.117 -  fixes f :: "('a, 'b) bcontfun"
1.118 -  assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b"
1.119 +  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
1.120 +  assumes "\<And>x. dist (f x) (g x) \<le> b"
1.121    shows "dist f g \<le> b"
1.122 -  using assms by (auto simp: dist_bcontfun_def intro: cSUP_least)
1.123 -
1.124 -lemma dist_bounded_Abs:
1.125 -  fixes f g :: "'a \<Rightarrow> 'b"
1.126 -  assumes "f \<in> bcontfun" "g \<in> bcontfun"
1.127 -  shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)"
1.128 -  by (metis Abs_bcontfun_inverse assms dist_bounded)
1.129 -
1.130 -lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun"
1.131 -  by (auto intro: bcontfunI continuous_on_const)
1.132 +  using assms
1.133 +  by transfer (auto intro!: cSUP_least)
1.134
1.135  lemma dist_fun_lt_imp_dist_val_lt:
1.136 +  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
1.137    assumes "dist f g < e"
1.138 -  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
1.139 +  shows "dist (f x) (g x) < e"
1.140    using dist_bounded assms by (rule le_less_trans)
1.141
1.142 -lemma dist_val_lt_imp_dist_fun_le:
1.143 -  assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
1.144 -  shows "dist f g \<le> e"
1.145 -  unfolding dist_bcontfun_def
1.146 -proof (intro cSUP_least)
1.147 -  fix x
1.148 -  show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e"
1.149 -    using assms[THEN spec[where x=x]] by (simp add: dist_norm)
1.150 -qed simp
1.151 -
1.152  instance
1.153  proof
1.154 -  fix f g h :: "('a, 'b) bcontfun"
1.155 +  fix f g h :: "'a \<Rightarrow>\<^sub>C 'b"
1.156    show "dist f g = 0 \<longleftrightarrow> f = g"
1.157    proof
1.158 -    have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
1.159 +    have "\<And>x. dist (f x) (g x) \<le> dist f g"
1.160        by (rule dist_bounded)
1.161      also assume "dist f g = 0"
1.162      finally show "f = g"
1.163 -      by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
1.164 +      by (auto simp: apply_bcontfun_inject[symmetric])
1.165    qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
1.166    show "dist f g \<le> dist f h + dist g h"
1.167 -  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
1.168 +  proof (rule dist_bound)
1.169      fix x
1.170 -    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
1.171 -      dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)"
1.172 +    have "dist (f x) (g x) \<le> dist (f x) (h x) + dist (g x) (h x)"
1.173        by (rule dist_triangle2)
1.174 -    also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h"
1.175 +    also have "dist (f x) (h x) \<le> dist f h"
1.176        by (rule dist_bounded)
1.177 -    also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h"
1.178 +    also have "dist (g x) (h x) \<le> dist g h"
1.179        by (rule dist_bounded)
1.180 -    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
1.181 +    finally show "dist (f x) (g x) \<le> dist f h + dist g h"
1.182        by simp
1.183    qed
1.184  qed (rule open_bcontfun_def uniformity_bcontfun_def)+
1.185
1.186  end
1.187
1.188 -lemma closed_Pi_bcontfun:
1.189 +lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set"
1.190 +  is "\<lambda>I X. Pi I X \<inter> {f. continuous_on UNIV f \<and> bounded (range f)}"
1.191 +  by auto
1.192 +
1.193 +lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X"
1.194 +  by transfer simp
1.195 +
1.196 +lemmas mem_PiCD = mem_PiC_iff[THEN iffD1]
1.197 +  and mem_PiCI = mem_PiC_iff[THEN iffD2]
1.198 +
1.199 +lemma tendsto_bcontfun_uniform_limit:
1.200 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
1.201 +  assumes "(f \<longlongrightarrow> l) F"
1.202 +  shows "uniform_limit UNIV f l F"
1.203 +proof (rule uniform_limitI)
1.204 +  fix e::real assume "e > 0"
1.205 +  from tendstoD[OF assms this] have "\<forall>\<^sub>F x in F. dist (f x) l < e" .
1.206 +  then show "\<forall>\<^sub>F n in F. \<forall>x\<in>UNIV. dist ((f n) x) (l x) < e"
1.207 +    by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt)
1.208 +qed
1.209 +
1.210 +lemma uniform_limit_tendsto_bcontfun:
1.211 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
1.212 +    and l::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
1.213 +  assumes "uniform_limit UNIV f l F"
1.214 +  shows "(f \<longlongrightarrow> l) F"
1.215 +proof (rule tendstoI)
1.216 +  fix e::real assume "e > 0"
1.217 +  then have "e / 2 > 0" by simp
1.218 +  from uniform_limitD[OF assms this]
1.219 +  have "\<forall>\<^sub>F i in F. \<forall>x. dist (f i x) (l x) < e / 2" by simp
1.220 +  then have "\<forall>\<^sub>F x in F. dist (f x) l \<le> e / 2"
1.221 +    by eventually_elim (blast intro: dist_bound less_imp_le)
1.222 +  then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
1.223 +    by eventually_elim (use \<open>0 < e\<close> in auto)
1.224 +qed
1.225 +
1.226 +lemma uniform_limit_bcontfunE:
1.227 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
1.228 +    and l::"'a::topological_space \<Rightarrow> 'b::metric_space"
1.229 +  assumes "uniform_limit UNIV f l F" "F \<noteq> bot"
1.230 +  obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
1.231 +  where "l = l'" "(f \<longlongrightarrow> l') F"
1.232 +  by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
1.233 +      mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun uniform_limit_theorem)
1.234 +
1.235 +lemma closed_PiC:
1.236    fixes I :: "'a::metric_space set"
1.237      and X :: "'a \<Rightarrow> 'b::complete_space set"
1.238    assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
1.239 -  shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))"
1.240 +  shows "closed (PiC I X)"
1.241    unfolding closed_sequential_limits
1.242  proof safe
1.243    fix f l
1.244 -  assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l"
1.245 -  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.246 -    using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
1.247 -    by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
1.248 -      (metis dist_fun_lt_imp_dist_val_lt)+
1.249 -  show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)"
1.250 -  proof (rule, safe)
1.251 +  assume seq: "\<forall>n. f n \<in> PiC I X" and lim: "f \<longlonglongrightarrow> l"
1.252 +  show "l \<in> PiC I X"
1.253 +  proof (safe intro!: mem_PiCI)
1.254      fix x assume "x \<in> I"
1.255      then have "closed (X x)"
1.256        using assms by simp
1.257 -    moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially"
1.258 -    proof (rule always_eventually, safe)
1.259 -      fix i
1.260 -      from seq[THEN spec, of i] \<open>x \<in> I\<close>
1.261 -      show "Rep_bcontfun (f i) x \<in> X x"
1.262 -        by (auto simp: Abs_bcontfun_inverse)
1.263 -    qed
1.264 +    moreover have "eventually (\<lambda>i. f i x \<in> X x) sequentially"
1.265 +      using seq \<open>x \<in> I\<close>
1.266 +      by (auto intro!: eventuallyI dest!: mem_PiCD simp: Pi_iff)
1.267      moreover note sequentially_bot
1.268 -    moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x"
1.269 -      using lim_fun by (blast intro!: metric_LIMSEQ_I)
1.270 -    ultimately show "Rep_bcontfun l x \<in> X x"
1.271 +    moreover have "(\<lambda>n. (f n) x) \<longlonglongrightarrow> l x"
1.272 +      using tendsto_bcontfun_uniform_limit[OF lim]
1.273 +      by (rule tendsto_uniform_limitI) simp
1.274 +    ultimately show "l x \<in> X x"
1.275        by (rule Lim_in_closed_set)
1.276 -  qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse)
1.277 +  qed
1.278  qed
1.279
1.280
1.281 @@ -174,53 +176,15 @@
1.282  proof
1.283    fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
1.284    assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
1.285 -  then obtain g where limit_function:
1.286 -    "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e"
1.287 -    using uniformly_convergent_eq_cauchy[of "\<lambda>_. True"
1.288 -      "\<lambda>n. Rep_bcontfun (f n)"]
1.289 -    unfolding Cauchy_def
1.290 +  then obtain g where "uniform_limit UNIV f g sequentially"
1.291 +    using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" f]
1.292 +    unfolding Cauchy_def uniform_limit_sequentially_iff
1.293      by (metis dist_fun_lt_imp_dist_val_lt)
1.294
1.295 -  then obtain N where fg_dist:  \<comment> \<open>for an upper bound on @{term g}\<close>
1.296 -    "\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1"
1.297 -    by (force simp add: dist_commute)
1.298 -  from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where
1.299 -    f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b"
1.300 -    by force
1.301 -  have "g \<in> bcontfun"  \<comment> \<open>The limit function is bounded and continuous\<close>
1.302 -  proof (intro bcontfunI)
1.303 -    show "continuous_on UNIV g"
1.304 -      apply (rule bcontfunE[OF Rep_bcontfun])
1.305 -      using limit_function
1.306 -      by (auto simp add: uniform_limit_sequentially_iff intro: uniform_limit_theorem[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
1.307 -  next
1.308 -    fix x
1.309 -    from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
1.310 -      by (simp add: dist_norm norm_minus_commute)
1.311 -    with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"]
1.312 -    show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x]
1.313 -      by simp
1.314 -  qed
1.315 -  show "convergent f"
1.316 -  proof (rule convergentI, subst lim_sequentially, safe)
1.317 -    \<comment> \<open>The limit function converges according to its norm\<close>
1.318 -    fix e :: real
1.319 -    assume "e > 0"
1.320 -    then have "e/2 > 0" by simp
1.321 -    with limit_function[THEN spec, of"e/2"]
1.322 -    have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2"
1.323 -      by simp
1.324 -    then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto
1.325 -    show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e"
1.326 -    proof (rule, safe)
1.327 -      fix n
1.328 -      assume "N \<le> n"
1.329 -      with N show "dist (f n) (Abs_bcontfun g) < e"
1.330 -        using dist_val_lt_imp_dist_fun_le[of
1.331 -          "f n" "Abs_bcontfun g" "e/2"]
1.332 -          Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp
1.333 -    qed
1.334 -  qed
1.335 +  from uniform_limit_bcontfunE[OF this sequentially_bot]
1.336 +  obtain l' where "g = apply_bcontfun l'" "(f \<longlonglongrightarrow> l')" by metis
1.337 +  then show "convergent f"
1.338 +    by (intro convergentI)
1.339  qed
1.340
1.341
1.342 @@ -229,104 +193,42 @@
1.343  instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
1.344  begin
1.345
1.346 -definition "-f = Abs_bcontfun (\<lambda>x. -(Rep_bcontfun f x))"
1.347 -
1.348 -definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)"
1.349 +lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x"
1.350 +  by (auto intro!: continuous_intros)
1.351
1.352 -definition "f - g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x - Rep_bcontfun g x)"
1.353 -
1.354 -definition "0 = Abs_bcontfun (\<lambda>x. 0)"
1.355 -
1.356 -definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)"
1.357 +lift_definition plus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x + g x"
1.358 +  by (auto simp: intro!: continuous_intros bounded_plus_comp)
1.359
1.360 -lemma plus_cont:
1.361 -  fixes f g :: "'a \<Rightarrow> 'b"
1.362 -  assumes f: "f \<in> bcontfun"
1.363 -    and g: "g \<in> bcontfun"
1.364 -  shows "(\<lambda>x. f x + g x) \<in> bcontfun"
1.365 -proof -
1.366 -  from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
1.367 -    by auto
1.368 -  moreover
1.369 -  from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z"
1.370 -    by auto
1.371 -  ultimately show ?thesis
1.372 -  proof (intro bcontfunI)
1.373 -    fix x
1.374 -    have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)"
1.375 -      by simp
1.376 -    also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0"
1.378 -    also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
1.379 -      unfolding zero_bcontfun_def using assms
1.380 -      by (metis add_mono const_bcontfun dist_bounded_Abs)
1.381 -    finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
1.383 -qed
1.384 +lift_definition minus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x - g x"
1.385 +  by (auto simp: intro!: continuous_intros bounded_minus_comp)
1.386
1.387 -lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x"
1.388 -  by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun)
1.389 +lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0"
1.390 +  by (auto intro!: continuous_intros simp: image_def)
1.391
1.392 -lemma uminus_cont:
1.393 -  fixes f :: "'a \<Rightarrow> 'b"
1.394 -  assumes "f \<in> bcontfun"
1.395 -  shows "(\<lambda>x. - f x) \<in> bcontfun"
1.396 -proof -
1.397 -  from bcontfunE[OF assms, of 0] obtain y
1.398 -    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
1.399 -    by auto
1.400 -  then show ?thesis
1.401 -  proof (intro bcontfunI)
1.402 -    fix x
1.403 -    assume "\<And>x. dist (f x) 0 \<le> y"
1.404 -    then show "dist (- f x) 0 \<le> y"
1.405 -      by (subst dist_minus[symmetric]) simp
1.406 -  qed (simp add: continuous_on_minus)
1.407 -qed
1.408 +lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
1.409 +  by transfer simp
1.410
1.411 -lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
1.412 -  by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)
1.413 +lift_definition scaleR_bcontfun::"real \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>r g x. r *\<^sub>R g x"
1.414 +  by (auto simp: intro!: continuous_intros bounded_scaleR_comp)
1.415
1.416 -lemma minus_cont:
1.417 -  fixes f g :: "'a \<Rightarrow> 'b"
1.418 -  assumes f: "f \<in> bcontfun"
1.419 -    and g: "g \<in> bcontfun"
1.420 -  shows "(\<lambda>x. f x - g x) \<in> bcontfun"
1.421 -  using plus_cont [of f "- g"] assms
1.422 -  by (simp add: uminus_cont fun_Compl_def)
1.423 -
1.424 -lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
1.425 -  by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)
1.426 +lemmas [simp] =
1.427 +  const_bcontfun.rep_eq
1.428 +  uminus_bcontfun.rep_eq
1.429 +  plus_bcontfun.rep_eq
1.430 +  minus_bcontfun.rep_eq
1.431 +  zero_bcontfun.rep_eq
1.432 +  scaleR_bcontfun.rep_eq
1.433
1.434 -lemma scaleR_cont:
1.435 -  fixes a :: real
1.436 -    and f :: "'a \<Rightarrow> 'b"
1.437 -  assumes "f \<in> bcontfun"
1.438 -  shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun"
1.439 -proof -
1.440 -  from bcontfunE[OF assms, of 0] obtain y
1.441 -    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
1.442 -    by auto
1.443 -  then show ?thesis
1.444 -  proof (intro bcontfunI)
1.445 -    fix x
1.446 -    assume "\<And>x. dist (f x) 0 \<le> y"
1.447 -    then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
1.448 -      by (metis norm_cmul_rule_thm norm_conv_dist)
1.449 -  qed (simp add: continuous_intros)
1.450 -qed
1.451 -
1.452 -lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
1.453 -  by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
1.454
1.455  instance
1.456 -  by standard
1.457 -    (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
1.458 -      Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
1.459 -      plus_cont const_bcontfun minus_cont scaleR_cont)
1.460 +  by standard (auto intro!: bcontfun_eqI simp: algebra_simps)
1.461
1.462  end
1.463
1.464 +lemma bounded_norm_le_SUP_norm:
1.465 +  "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
1.466 +  by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
1.467 +
1.468  instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
1.469  begin
1.470
1.471 @@ -340,179 +242,68 @@
1.472    fix a :: real
1.473    fix f g :: "('a, 'b) bcontfun"
1.474    show "dist f g = norm (f - g)"
1.475 -    by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
1.476 -      Abs_bcontfun_inverse const_bcontfun dist_norm)
1.477 +    unfolding norm_bcontfun_def
1.478 +    by transfer (simp add: dist_norm)
1.479    show "norm (f + g) \<le> norm f + norm g"
1.480      unfolding norm_bcontfun_def
1.481 -  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
1.482 -    fix x
1.483 -    have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le>
1.484 -      dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0"
1.485 -      by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm
1.486 -        le_less_linear less_irrefl norm_triangle_lt)
1.487 -    also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0"
1.488 -      using dist_bounded[of f x 0]
1.489 -      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
1.490 -    also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0]
1.491 -      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
1.492 -    finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp
1.493 -  qed
1.494 +    by transfer
1.495 +      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm simp: dist_norm)
1.496    show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
1.497 -  proof -
1.498 -    have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) =
1.499 -      (SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)"
1.500 -    proof (intro continuous_at_Sup_mono bdd_aboveI2)
1.501 -      fix x
1.502 -      show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0]
1.503 -        by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
1.504 -          const_bcontfun)
1.505 -    qed (auto intro!: monoI mult_left_mono continuous_intros)
1.506 -    moreover
1.507 -    have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
1.508 -      (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
1.509 -      by auto
1.510 -    ultimately
1.511 -    show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
1.512 -      by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse
1.513 -        zero_bcontfun_def const_bcontfun image_image)
1.514 -  qed
1.515 +    unfolding norm_bcontfun_def
1.516 +    apply transfer
1.517 +    by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
1.518 +      (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
1.519 +        simp: bounded_norm_comp)
1.520  qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
1.521
1.522  end
1.523
1.524 -lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
1.525 -  by (metis bcontfunI dist_0_norm dist_commute)
1.526 -
1.527  lemma norm_bounded:
1.528    fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
1.529 -  shows "norm (Rep_bcontfun f x) \<le> norm f"
1.530 +  shows "norm (apply_bcontfun f x) \<le> norm f"
1.531    using dist_bounded[of f x 0]
1.532 -  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
1.533 -    const_bcontfun)
1.534 +  by (simp add: dist_norm)
1.535
1.536  lemma norm_bound:
1.537    fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
1.538 -  assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
1.539 +  assumes "\<And>x. norm (apply_bcontfun f x) \<le> b"
1.540    shows "norm f \<le> b"
1.541    using dist_bound[of f 0 b] assms
1.542 -  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun)
1.543 -
1.544 -
1.545 -subsection \<open>Continuously Extended Functions\<close>
1.546 -
1.547 -definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
1.548 -  "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.549 -
1.550 -definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
1.551 -  where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))"
1.552 -
1.553 -lemma ext_cont_def':
1.554 -  "ext_cont f a b = Abs_bcontfun (\<lambda>x.
1.555 -    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.556 -  unfolding ext_cont_def clamp_def ..
1.557 -
1.558 -lemma clamp_in_interval:
1.559 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
1.560 -  shows "clamp a b x \<in> cbox a b"
1.561 -  unfolding clamp_def
1.562 -  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
1.563 -
1.564 -lemma dist_clamps_le_dist_args:
1.565 -  fixes x :: "'a::euclidean_space"
1.566 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
1.567 -  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
1.568 -proof -
1.569 -  from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
1.570 -    by (simp add: cbox_def)
1.571 -  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
1.572 -    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
1.573 -    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
1.574 -  then show ?thesis
1.575 -    by (auto intro: real_sqrt_le_mono
1.576 -      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
1.577 -qed
1.578 +  by (simp add: dist_norm)
1.579
1.580 -lemma clamp_continuous_at:
1.581 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
1.582 -    and x :: 'a
1.583 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
1.584 -    and f_cont: "continuous_on (cbox a b) f"
1.585 -  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
1.586 -  unfolding continuous_at_eps_delta
1.587 -proof safe
1.588 -  fix x :: 'a
1.589 -  fix e :: real
1.590 -  assume "e > 0"
1.591 -  moreover have "clamp a b x \<in> cbox a b"
1.592 -    by (simp add: clamp_in_interval assms)
1.593 -  moreover note f_cont[simplified continuous_on_iff]
1.594 -  ultimately
1.595 -  obtain d where d: "0 < d"
1.596 -    "\<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.597 -    by force
1.598 -  show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
1.599 -    dist (f (clamp a b x')) (f (clamp a b x)) < e"
1.600 -    by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans])
1.601 -qed
1.602 -
1.603 -lemma clamp_continuous_on:
1.604 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
1.605 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
1.606 -    and f_cont: "continuous_on (cbox a b) f"
1.607 -  shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))"
1.608 -  using assms
1.609 -  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
1.610 -
1.611 -lemma clamp_bcontfun:
1.612 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.613 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
1.614 -    and continuous: "continuous_on (cbox a b) f"
1.615 -  shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
1.616 -proof -
1.617 -  have "bounded (f ` (cbox a b))"
1.618 -    by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
1.619 -  then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c"
1.620 -    by (auto simp add: bounded_pos)
1.621 -  show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
1.622 -  proof (intro bcontfun_normI)
1.623 -    fix x
1.624 -    show "norm (f (clamp a b x)) \<le> c"
1.625 -      using clamp_in_interval[OF assms(1), of x] f_bound
1.626 -      by (simp add: ext_cont_def)
1.627 -  qed (simp add: clamp_continuous_on assms)
1.628 -qed
1.629 +subsection \<open>(bounded) continuous extenstion\<close>
1.630
1.631  lemma integral_clamp:
1.632    "integral {t0::real..clamp t0 t1 x} f =
1.633      (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
1.634    by (auto simp: clamp_def)
1.635
1.636 -
1.637 -declare [[coercion Rep_bcontfun]]
1.638 +lemma continuous_on_interval_bcontfunE:
1.639 +  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::metric_space"
1.640 +  assumes "continuous_on {a .. b} f"
1.641 +  obtains g::"'a \<Rightarrow>\<^sub>C 'b" where
1.642 +    "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> g x = f x"
1.643 +    "\<And>x. g x = f (clamp a b x)"
1.644 +proof -
1.645 +  define g where "g \<equiv> ext_cont f a b"
1.646 +  have "continuous_on UNIV g"
1.647 +    using assms
1.648 +    by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval)
1.649 +  moreover
1.650 +  have "bounded (range g)"
1.651 +    by (auto simp: g_def ext_cont_def cbox_interval
1.652 +        intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
1.653 +  ultimately
1.654 +  obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
1.655 +  then have "h x = f x" if "a \<le> x" "x \<le> b" for x
1.656 +    by (auto simp: h[symmetric] g_def cbox_interval that)
1.657 +  moreover
1.658 +  have "h x = f (clamp a b x)" for x
1.659 +    by (auto simp: h[symmetric] g_def ext_cont_def)
1.660 +  ultimately show ?thesis ..
1.661 +qed
1.662
1.663 -lemma ext_cont_cancel[simp]:
1.664 -  fixes x a b :: "'a::euclidean_space"
1.665 -  assumes x: "x \<in> cbox a b"
1.666 -    and "continuous_on (cbox a b) f"
1.667 -  shows "ext_cont f a b x = f x"
1.668 -  using assms
1.669 -  unfolding ext_cont_def
1.670 -proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun])
1.671 -  show "f (clamp a b x) = f x"
1.672 -    using x unfolding clamp_def mem_box
1.673 -    by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less)
1.674 -qed (auto simp: cbox_def)
1.675 -
1.676 -lemma ext_cont_cong:
1.677 -  assumes "t0 = s0"
1.678 -    and "t1 = s1"
1.679 -    and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
1.680 -    and "continuous_on (cbox t0 t1) f"
1.681 -    and "continuous_on (cbox s0 s1) g"
1.682 -    and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
1.683 -  shows "ext_cont f t0 t1 = ext_cont g s0 s1"
1.684 -  unfolding assms ext_cont_def
1.685 -  using assms clamp_in_interval[OF ord]
1.686 -  by (subst Rep_bcontfun_inject[symmetric]) simp
1.687 +lifting_update bcontfun.lifting
1.688 +lifting_forget bcontfun.lifting
1.689
1.690  end
```
```     2.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Mar 12 19:06:10 2017 +0100
2.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Mar 10 23:16:40 2017 +0100
2.3 @@ -2543,4 +2543,69 @@
2.4      by simp
2.5  qed
2.6
2.7 +lemma has_integral_0_closure_imp_0:
2.8 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
2.9 +  assumes f: "continuous_on (closure S) f"
2.10 +    and nonneg_interior: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
2.11 +    and pos: "0 < emeasure lborel S"
2.12 +    and finite: "emeasure lborel S < \<infinity>"
2.13 +    and regular: "emeasure lborel (closure S) = emeasure lborel S"
2.14 +    and opn: "open S"
2.15 +  assumes int: "(f has_integral 0) (closure S)"
2.16 +  assumes x: "x \<in> closure S"
2.17 +  shows "f x = 0"
2.18 +proof -
2.19 +  have zero: "emeasure lborel (frontier S) = 0"
2.20 +    using finite closure_subset regular
2.21 +    unfolding frontier_def
2.22 +    by (subst emeasure_Diff) (auto simp: frontier_def interior_open \<open>open S\<close> )
2.23 +  have nonneg: "0 \<le> f x" if "x \<in> closure S" for x
2.24 +    using continuous_ge_on_closure[OF f that nonneg_interior] by simp
2.25 +  have "0 = integral (closure S) f"
2.26 +    by (blast intro: int sym)
2.27 +  also
2.28 +  note intl = has_integral_integrable[OF int]
2.29 +  have af: "f absolutely_integrable_on (closure S)"
2.30 +    using nonneg
2.31 +    by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
2.32 +  then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
2.33 +    by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
2.34 +  also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
2.35 +    by (rule integral_nonneg_eq_0_iff_AE[OF af]) (use nonneg in \<open>auto simp: indicator_def\<close>)
2.36 +  also have "\<dots> \<longleftrightarrow> (AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})"
2.37 +    by (auto simp: indicator_def)
2.38 +  finally have "(AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})" by simp
2.39 +  moreover have "(AE x in lebesgue. x \<in> - frontier S)"
2.40 +    using zero
2.41 +    by (auto simp: eventually_ae_filter null_sets_def intro!: exI[where x="frontier S"])
2.42 +  ultimately have ae: "AE x \<in> S in lebesgue. x \<in> {x \<in> closure S. f x = 0}" (is ?th)
2.43 +    by eventually_elim (use closure_subset in \<open>auto simp: \<close>)
2.44 +  have "closed {0::real}" by simp
2.45 +  with continuous_on_closed_vimage[OF closed_closure, of S f] f
2.46 +  have "closed (f -` {0} \<inter> closure S)" by blast
2.47 +  then have "closed {x \<in> closure S. f x = 0}" by (auto simp: vimage_def Int_def conj_commute)
2.48 +  with \<open>open S\<close> have "x \<in> {x \<in> closure S. f x = 0}" if "x \<in> S" for x using ae that
2.49 +    by (rule mem_closed_if_AE_lebesgue_open)
2.50 +  then have "f x = 0" if "x \<in> S" for x using that by auto
2.51 +  from continuous_constant_on_closure[OF f this \<open>x \<in> closure S\<close>]
2.52 +  show "f x = 0" .
2.53 +qed
2.54 +
2.55 +lemma has_integral_0_cbox_imp_0:
2.56 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
2.57 +  assumes f: "continuous_on (cbox a b) f"
2.58 +    and nonneg_interior: "\<And>x. x \<in> box a b \<Longrightarrow> 0 \<le> f x"
2.59 +  assumes int: "(f has_integral 0) (cbox a b)"
2.60 +  assumes ne: "box a b \<noteq> {}"
2.61 +  assumes x: "x \<in> cbox a b"
2.62 +  shows "f x = 0"
2.63 +proof -
2.64 +  have "0 < emeasure lborel (box a b)"
2.65 +    using ne x unfolding emeasure_lborel_box_eq
2.66 +    by (force intro!: prod_pos simp: mem_box algebra_simps)
2.67 +  then show ?thesis using assms
2.68 +    by (intro has_integral_0_closure_imp_0[of "box a b" f x])
2.69 +      (auto simp: emeasure_lborel_box_eq emeasure_lborel_cbox_eq algebra_simps mem_box)
2.70 +qed
2.71 +
2.72  end
```
```     3.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Mar 12 19:06:10 2017 +0100
3.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Mar 10 23:16:40 2017 +0100
3.3 @@ -268,6 +268,9 @@
3.4
3.5  subsection \<open>Basic theorems about integrals.\<close>
3.6
3.7 +lemma has_integral_eq_rhs: "(f has_integral j) S \<Longrightarrow> i = j \<Longrightarrow> (f has_integral i) S"
3.8 +  by (rule forw_subst)
3.9 +
3.10  lemma has_integral_unique:
3.11    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
3.12    assumes "(f has_integral k1) i"
3.13 @@ -499,6 +502,9 @@
3.14  lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) s"
3.15    by (drule_tac c="-1" in has_integral_cmul) auto
3.16
3.17 +lemma has_integral_neg_iff: "((\<lambda>x. - f x) has_integral k) s \<longleftrightarrow> (f has_integral - k) s"
3.18 +  using has_integral_neg[of f "- k"] has_integral_neg[of "\<lambda>x. - f x" k] by auto
3.19 +
3.21    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
3.22    assumes "(f has_integral k) s"
3.23 @@ -2604,11 +2610,14 @@
3.24      by auto
3.25  qed
3.26
3.27 -lemma integrable_continuous_real:
3.28 -  fixes f :: "real \<Rightarrow> 'a::banach"
3.29 +lemma integrable_continuous_interval:
3.30 +  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
3.31    assumes "continuous_on {a .. b} f"
3.32    shows "f integrable_on {a .. b}"
3.33 -  by (metis assms box_real(2) integrable_continuous)
3.34 +  by (metis assms integrable_continuous interval_cbox)
3.35 +
3.36 +lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
3.37 +
3.38
3.39  subsection \<open>Specialization of additivity to one dimension.\<close>
3.40
3.41 @@ -4566,6 +4575,18 @@
3.42    qed
3.43  qed
3.44
3.45 +lemma indefinite_integral_continuous':
3.46 +  fixes f::"real \<Rightarrow> 'a::banach"
3.47 +  assumes "f integrable_on {a..b}"
3.48 +  shows "continuous_on {a..b} (\<lambda>x. integral {x..b} f)"
3.49 +proof -
3.50 +  have "integral {a .. b} f - integral {a .. x} f = integral {x .. b} f" if "x \<in> {a .. b}" for x
3.51 +    using integral_combine[OF _ _ assms, of x] that
3.52 +    by (auto simp: algebra_simps)
3.53 +  with _ show ?thesis
3.54 +    by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous assms)
3.55 +qed
3.56 +
3.57
3.58  subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
3.59
3.60 @@ -7282,7 +7303,7 @@
3.61
3.62  subsection \<open>Exchange uniform limit and integral\<close>
3.63
3.64 -lemma uniform_limit_integral:
3.65 +lemma uniform_limit_integral_cbox:
3.66    fixes f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
3.67    assumes u: "uniform_limit (cbox a b) f g F"
3.68    assumes c: "\<And>n. continuous_on (cbox a b) (f n)"
3.69 @@ -7344,6 +7365,17 @@
3.70    ultimately show ?thesis ..
3.71  qed
3.72
3.73 +lemma uniform_limit_integral:
3.74 +  fixes f::"'a \<Rightarrow> 'b::ordered_euclidean_space \<Rightarrow> 'c::banach"
3.75 +  assumes u: "uniform_limit {a .. b} f g F"
3.76 +  assumes c: "\<And>n. continuous_on {a .. b} (f n)"
3.77 +  assumes [simp]: "F \<noteq> bot"
3.78 +  obtains I J where
3.79 +    "\<And>n. (f n has_integral I n) {a .. b}"
3.80 +    "(g has_integral J) {a .. b}"
3.81 +    "(I \<longlongrightarrow> J) F"
3.82 +  by (metis interval_cbox assms uniform_limit_integral_cbox)
3.83 +
3.84
3.85  subsection \<open>Integration by parts\<close>
3.86
3.87 @@ -7428,15 +7460,15 @@
3.88  subsection \<open>Integration by substitution\<close>
3.89
3.90
3.91 -lemma has_integral_substitution_strong:
3.92 +lemma has_integral_substitution_general:
3.93    fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
3.94 -  assumes s: "finite s" and le: "a \<le> b" "c \<le> d" "g a \<le> g b"
3.95 +  assumes s: "finite s" and le: "a \<le> b"
3.96        and subset: "g ` {a..b} \<subseteq> {c..d}"
3.97        and f [continuous_intros]: "continuous_on {c..d} f"
3.98        and g [continuous_intros]: "continuous_on {a..b} g"
3.99        and deriv [derivative_intros]:
3.100                "\<And>x. x \<in> {a..b} - s \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
3.101 -    shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
3.102 +    shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}"
3.103  proof -
3.104    let ?F = "\<lambda>x. integral {c..g x} f"
3.105    have cont_int: "continuous_on {a..b} ?F"
3.106 @@ -7461,22 +7493,48 @@
3.107    have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
3.108      using le cont_int s deriv cont_int
3.109      by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
3.110 -  also from subset have "g x \<in> {c..d}" if "x \<in> {a..b}" for x using that by blast
3.111 -  from this[of a] this[of b] le have "c \<le> g a" "g b \<le> d" by auto
3.112 -  hence "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
3.113 -    by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
3.114 -  hence "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f"
3.115 -    by (simp add: algebra_simps)
3.116 +  also
3.117 +  from subset have "g x \<in> {c..d}" if "x \<in> {a..b}" for x using that by blast
3.118 +  from this[of a] this[of b] le have cd: "c \<le> g a" "g b \<le> d" "c \<le> g b" "g a \<le> d" by auto
3.119 +  have "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f"
3.120 +  proof cases
3.121 +    assume "g a \<le> g b"
3.122 +    note le = le this
3.123 +    from cd have "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
3.124 +      by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
3.125 +    with le show ?thesis
3.126 +      by (cases "g a = g b") (simp_all add: algebra_simps)
3.127 +  next
3.128 +    assume less: "\<not>g a \<le> g b"
3.129 +    then have "g a \<ge> g b" by simp
3.130 +    note le = le this
3.131 +    from cd have "integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f"
3.132 +      by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
3.133 +    with less show ?thesis
3.134 +      by (simp_all add: algebra_simps)
3.135 +  qed
3.136    finally show ?thesis .
3.137  qed
3.138
3.139 +lemma has_integral_substitution_strong:
3.140 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
3.141 +  assumes s: "finite s" and le: "a \<le> b" "g a \<le> g b"
3.142 +    and subset: "g ` {a..b} \<subseteq> {c..d}"
3.143 +    and f [continuous_intros]: "continuous_on {c..d} f"
3.144 +    and g [continuous_intros]: "continuous_on {a..b} g"
3.145 +    and deriv [derivative_intros]:
3.146 +    "\<And>x. x \<in> {a..b} - s \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
3.147 +  shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
3.148 +  using has_integral_substitution_general[OF s le(1) subset f g deriv] le(2)
3.149 +  by (cases "g a = g b") auto
3.150 +
3.151  lemma has_integral_substitution:
3.152    fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
3.153 -  assumes "a \<le> b" "c \<le> d" "g a \<le> g b" "g ` {a..b} \<subseteq> {c..d}"
3.154 +  assumes "a \<le> b" "g a \<le> g b" "g ` {a..b} \<subseteq> {c..d}"
3.155        and "continuous_on {c..d} f"
3.156        and "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
3.157      shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
3.158 -  by (intro has_integral_substitution_strong[of "{}" a b c d] assms)
3.159 +  by (intro has_integral_substitution_strong[of "{}" a b g c d] assms)
3.160       (auto intro: DERIV_continuous_on assms)
3.161
3.162
```
```     4.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Mar 12 19:06:10 2017 +0100
4.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Mar 10 23:16:40 2017 +0100
4.3 @@ -586,6 +586,33 @@
4.4    ultimately show False by contradiction
4.5  qed
4.6
4.7 +lemma mem_closed_if_AE_lebesgue_open:
4.8 +  assumes "open S" "closed C"
4.9 +  assumes "AE x \<in> S in lebesgue. x \<in> C"
4.10 +  assumes "x \<in> S"
4.11 +  shows "x \<in> C"
4.12 +proof (rule ccontr)
4.13 +  assume xC: "x \<notin> C"
4.14 +  with openE[of "S - C"] assms
4.15 +  obtain e where e: "0 < e" "ball x e \<subseteq> S - C"
4.16 +    by blast
4.17 +  then obtain a b where box: "x \<in> box a b" "box a b \<subseteq> S - C"
4.18 +    by (metis rational_boxes order_trans)
4.19 +  then have "0 < emeasure lebesgue (box a b)"
4.20 +    by (auto simp: emeasure_lborel_box_eq mem_box algebra_simps intro!: prod_pos)
4.21 +  also have "\<dots> \<le> emeasure lebesgue (S - C)"
4.22 +    using assms box
4.23 +    by (auto intro!: emeasure_mono)
4.24 +  also have "\<dots> = 0"
4.25 +    using assms
4.26 +    by (auto simp: eventually_ae_filter completion.complete2 set_diff_eq null_setsD1)
4.27 +  finally show False by simp
4.28 +qed
4.29 +
4.30 +lemma mem_closed_if_AE_lebesgue: "closed C \<Longrightarrow> (AE x in lebesgue. x \<in> C) \<Longrightarrow> x \<in> C"
4.31 +  using mem_closed_if_AE_lebesgue_open[OF open_UNIV] by simp
4.32 +
4.33 +
4.34  subsection \<open>Affine transformation on the Lebesgue-Borel\<close>
4.35
4.36  lemma lborel_eqI:
```
```     5.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Mar 12 19:06:10 2017 +0100
5.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Mar 10 23:16:40 2017 +0100
5.3 @@ -3940,6 +3940,9 @@
5.4  lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
5.5    by (simp add: bounded_iff bdd_above_def)
5.6
5.7 +lemma bounded_norm_comp: "bounded ((\<lambda>x. norm (f x)) ` S) = bounded (f ` S)"
5.8 +  by (simp add: bounded_iff)
5.9 +
5.10  lemma boundedI:
5.11    assumes "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
5.12    shows "bounded S"
5.13 @@ -4056,6 +4059,19 @@
5.14      shows "bounded (- S) \<Longrightarrow> ~ (bounded S)"
5.15    using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
5.16
5.17 +lemma bounded_dist_comp:
5.18 +  assumes "bounded (f ` S)" "bounded (g ` S)"
5.19 +  shows "bounded ((\<lambda>x. dist (f x) (g x)) ` S)"
5.20 +proof -
5.21 +  from assms obtain M1 M2 where *: "dist (f x) undefined \<le> M1" "dist undefined (g x) \<le> M2" if "x \<in> S" for x
5.22 +    by (auto simp: bounded_any_center[of _ undefined] dist_commute)
5.23 +  have "dist (f x) (g x) \<le> M1 + M2" if "x \<in> S" for x
5.24 +    using *[OF that]
5.25 +    by (rule order_trans[OF dist_triangle add_mono])
5.26 +  then show ?thesis
5.27 +    by (auto intro!: boundedI)
5.28 +qed
5.29 +
5.30  lemma bounded_linear_image:
5.31    assumes "bounded S"
5.32      and "bounded_linear f"
5.33 @@ -4090,6 +4106,13 @@
5.34    apply (rule bounded_linear_scaleR_right)
5.35    done
5.36
5.37 +lemma bounded_scaleR_comp:
5.38 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
5.39 +  assumes "bounded (f ` S)"
5.40 +  shows "bounded ((\<lambda>x. r *\<^sub>R f x) ` S)"
5.41 +  using bounded_scaling[of "f ` S" r] assms
5.42 +  by (auto simp: image_image)
5.43 +
5.44  lemma bounded_translation:
5.45    fixes S :: "'a::real_normed_vector set"
5.46    assumes "bounded S"
5.47 @@ -4119,6 +4142,33 @@
5.48    shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
5.49  by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
5.50
5.51 +lemma uminus_bounded_comp [simp]:
5.52 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
5.53 +  shows "bounded ((\<lambda>x. - f x) ` S) \<longleftrightarrow> bounded (f ` S)"
5.54 +  using bounded_uminus[of "f ` S"]
5.55 +  by (auto simp: image_image)
5.56 +
5.57 +lemma bounded_plus_comp:
5.58 +  fixes f g::"'a \<Rightarrow> 'b::real_normed_vector"
5.59 +  assumes "bounded (f ` S)"
5.60 +  assumes "bounded (g ` S)"
5.61 +  shows "bounded ((\<lambda>x. f x + g x) ` S)"
5.62 +proof -
5.63 +  {
5.64 +    fix B C
5.65 +    assume "\<And>x. x\<in>S \<Longrightarrow> norm (f x) \<le> B" "\<And>x. x\<in>S \<Longrightarrow> norm (g x) \<le> C"
5.66 +    then have "\<And>x. x \<in> S \<Longrightarrow> norm (f x + g x) \<le> B + C"
5.67 +      by (auto intro!: norm_triangle_le add_mono)
5.68 +  } then show ?thesis
5.69 +    using assms by (fastforce simp: bounded_iff)
5.70 +qed
5.71 +
5.72 +lemma bounded_minus_comp:
5.73 +  "bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
5.74 +  for f g::"'a \<Rightarrow> 'b::real_normed_vector"
5.75 +  using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
5.76 +  by (auto simp: )
5.77 +
5.78
5.79  subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
5.80
5.81 @@ -5915,89 +5965,6 @@
5.82    then show ?thesis ..
5.83  qed
5.84
5.85 -text\<open>Cauchy-type criteria for uniform convergence.\<close>
5.86 -
5.87 -lemma uniformly_convergent_eq_cauchy:
5.88 -  fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
5.89 -  shows
5.90 -    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
5.91 -      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  \<longrightarrow> dist (s m x) (s n x) < e)"
5.92 -  (is "?lhs = ?rhs")
5.93 -proof
5.94 -  assume ?lhs
5.95 -  then obtain l where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e"
5.96 -    by auto
5.97 -  {
5.98 -    fix e :: real
5.99 -    assume "e > 0"
5.100 -    then obtain N :: nat where N: "\<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e / 2"
5.101 -      using l[THEN spec[where x="e/2"]] by auto
5.102 -    {
5.103 -      fix n m :: nat and x :: "'b"
5.104 -      assume "N \<le> m \<and> N \<le> n \<and> P x"
5.105 -      then have "dist (s m x) (s n x) < e"
5.106 -        using N[THEN spec[where x=m], THEN spec[where x=x]]
5.107 -        using N[THEN spec[where x=n], THEN spec[where x=x]]
5.108 -        using dist_triangle_half_l[of "s m x" "l x" e "s n x"] by auto
5.109 -    }
5.110 -    then have "\<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  --> dist (s m x) (s n x) < e"  by auto
5.111 -  }
5.112 -  then show ?rhs by auto
5.113 -next
5.114 -  assume ?rhs
5.115 -  then have "\<forall>x. P x \<longrightarrow> Cauchy (\<lambda>n. s n x)"
5.116 -    unfolding cauchy_def
5.117 -    apply auto
5.118 -    apply (erule_tac x=e in allE)
5.119 -    apply auto
5.120 -    done
5.121 -  then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l x) sequentially"
5.122 -    unfolding convergent_eq_Cauchy[symmetric]
5.123 -    using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l) sequentially"]
5.124 -    by auto
5.125 -  {
5.126 -    fix e :: real
5.127 -    assume "e > 0"
5.128 -    then obtain N where N:"\<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x \<longrightarrow> dist (s m x) (s n x) < e/2"
5.129 -      using \<open>?rhs\<close>[THEN spec[where x="e/2"]] by auto
5.130 -    {
5.131 -      fix x
5.132 -      assume "P x"
5.133 -      then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2"
5.134 -        using l[THEN spec[where x=x], unfolded lim_sequentially] and \<open>e > 0\<close>
5.135 -        by (auto elim!: allE[where x="e/2"])
5.136 -      fix n :: nat
5.137 -      assume "n \<ge> N"
5.138 -      then have "dist(s n x)(l x) < e"
5.139 -        using \<open>P x\<close>and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]]
5.140 -        using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"]
5.141 -        by (auto simp add: dist_commute)
5.142 -    }
5.143 -    then have "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
5.144 -      by auto
5.145 -  }
5.146 -  then show ?lhs by auto
5.147 -qed
5.148 -
5.149 -lemma uniformly_cauchy_imp_uniformly_convergent:
5.150 -  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
5.151 -  assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
5.152 -    and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
5.153 -  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
5.154 -proof -
5.155 -  obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
5.156 -    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
5.157 -  moreover
5.158 -  {
5.159 -    fix x
5.160 -    assume "P x"
5.161 -    then have "l x = l' x"
5.162 -      using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
5.163 -      using l and assms(2) unfolding lim_sequentially by blast
5.164 -  }
5.165 -  ultimately show ?thesis by auto
5.166 -qed
5.167 -
5.168
5.169  subsection \<open>Continuity\<close>
5.170
5.171 @@ -10960,6 +10927,109 @@
5.172    by blast
5.173
5.174
5.175 +
5.176 +subsection \<open>Continuous Extension\<close>
5.177 +
5.178 +definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
5.179 +  "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
5.180 +    then (\<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)
5.181 +    else a)"
5.182 +
5.183 +lemma clamp_in_interval[simp]:
5.184 +  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
5.185 +  shows "clamp a b x \<in> cbox a b"
5.186 +  unfolding clamp_def
5.187 +  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
5.188 +
5.189 +lemma clamp_cancel_cbox[simp]:
5.190 +  fixes x a b :: "'a::euclidean_space"
5.191 +  assumes x: "x \<in> cbox a b"
5.192 +  shows "clamp a b x = x"
5.193 +  using assms
5.194 +  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
5.195 +
5.196 +lemma clamp_empty_interval:
5.197 +  assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
5.198 +  shows "clamp a b = (\<lambda>_. a)"
5.199 +  using assms
5.200 +  by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
5.201 +
5.202 +lemma dist_clamps_le_dist_args:
5.203 +  fixes x :: "'a::euclidean_space"
5.204 +  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
5.205 +proof cases
5.206 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
5.207 +  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
5.208 +    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
5.209 +    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
5.210 +  then show ?thesis
5.211 +    by (auto intro: real_sqrt_le_mono
5.212 +      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
5.213 +qed (auto simp: clamp_def)
5.214 +
5.215 +lemma clamp_continuous_at:
5.216 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
5.217 +    and x :: 'a
5.218 +  assumes f_cont: "continuous_on (cbox a b) f"
5.219 +  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
5.220 +proof cases
5.221 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
5.222 +  show ?thesis
5.223 +    unfolding continuous_at_eps_delta
5.224 +  proof safe
5.225 +    fix x :: 'a
5.226 +    fix e :: real
5.227 +    assume "e > 0"
5.228 +    moreover have "clamp a b x \<in> cbox a b"
5.229 +      by (simp add: clamp_in_interval le)
5.230 +    moreover note f_cont[simplified continuous_on_iff]
5.231 +    ultimately
5.232 +    obtain d where d: "0 < d"
5.233 +      "\<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"
5.234 +      by force
5.235 +    show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
5.236 +      dist (f (clamp a b x')) (f (clamp a b x)) < e"
5.237 +      using le
5.238 +      by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
5.239 +  qed
5.240 +qed (auto simp: clamp_empty_interval)
5.241 +
5.242 +lemma clamp_continuous_on:
5.243 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
5.244 +  assumes f_cont: "continuous_on (cbox a b) f"
5.245 +  shows "continuous_on S (\<lambda>x. f (clamp a b x))"
5.246 +  using assms
5.247 +  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
5.248 +
5.249 +lemma clamp_bounded:
5.250 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
5.251 +  assumes bounded: "bounded (f ` (cbox a b))"
5.252 +  shows "bounded (range (\<lambda>x. f (clamp a b x)))"
5.253 +proof cases
5.254 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
5.255 +  from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
5.256 +    by (auto simp add: bounded_any_center[where a=undefined])
5.257 +  then show ?thesis
5.258 +    by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
5.259 +        simp: bounded_any_center[where a=undefined])
5.260 +qed (auto simp: clamp_empty_interval image_def)
5.261 +
5.262 +
5.263 +definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
5.264 +  where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
5.265 +
5.266 +lemma ext_cont_cancel_cbox[simp]:
5.267 +  fixes x a b :: "'a::euclidean_space"
5.268 +  assumes x: "x \<in> cbox a b"
5.269 +  shows "ext_cont f a b x = f x"
5.270 +  using assms
5.271 +  unfolding ext_cont_def
5.272 +  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
5.273 +
5.274 +lemma continuous_on_ext_cont[continuous_intros]:
5.275 +  "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
5.276 +  by (auto intro!: clamp_continuous_on simp: ext_cont_def)
5.277 +
5.278  no_notation
5.279    eucl_less (infix "<e" 50)
5.280
```
```     6.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Mar 12 19:06:10 2017 +0100
6.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Fri Mar 10 23:16:40 2017 +0100
6.3 @@ -203,6 +203,8 @@
6.4  lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
6.5    by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
6.6
6.7 +text\<open>Cauchy-type criteria for uniform convergence.\<close>
6.8 +
6.9  lemma Cauchy_uniformly_convergent:
6.10    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
6.11    assumes "uniformly_Cauchy_on X f"
6.12 @@ -235,6 +237,62 @@
6.13    qed
6.14  qed
6.15
6.16 +lemma uniformly_convergent_Cauchy:
6.17 +  assumes "uniformly_convergent_on X f"
6.18 +  shows "uniformly_Cauchy_on X f"
6.19 +proof (rule uniformly_Cauchy_onI)
6.20 +  fix e::real assume "e > 0"
6.21 +  then have "0 < e / 2" by simp
6.22 +  with assms[unfolded uniformly_convergent_on_def uniform_limit_sequentially_iff]
6.23 +  obtain l N where l:"x \<in> X \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f n x) (l x) < e / 2" for n x
6.24 +    by metis
6.25 +  from l l have "x \<in> X \<Longrightarrow> n \<ge> N \<Longrightarrow> m \<ge> N \<Longrightarrow> dist (f n x) (f m x) < e" for n m x
6.26 +    by (rule dist_triangle_half_l)
6.27 +  then show "\<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" by blast
6.28 +qed
6.29 +
6.30 +lemma uniformly_convergent_eq_Cauchy:
6.31 +  "uniformly_convergent_on X f = uniformly_Cauchy_on X f" for f::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
6.32 +  using Cauchy_uniformly_convergent uniformly_convergent_Cauchy by blast
6.33 +
6.34 +lemma uniformly_convergent_eq_cauchy:
6.35 +  fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
6.36 +  shows
6.37 +    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
6.38 +      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  \<longrightarrow> dist (s m x) (s n x) < e)"
6.39 +proof -
6.40 +  have *: "(\<forall>n\<ge>N. \<forall>x. Q x \<longrightarrow> R n x) \<longleftrightarrow> (\<forall>n x. N \<le> n \<and> Q x \<longrightarrow> R n x)"
6.41 +    "(\<forall>x. Q x \<longrightarrow> (\<forall>m\<ge>N. \<forall>n\<ge>N. S n m x)) \<longleftrightarrow> (\<forall>m n x. N \<le> m \<and> N \<le> n \<and> Q x \<longrightarrow> S n m x)"
6.42 +    for N::nat and Q::"'b \<Rightarrow> bool" and R S
6.43 +    by blast+
6.44 +  show ?thesis
6.45 +    using uniformly_convergent_eq_Cauchy[of "Collect P" s]
6.46 +    unfolding uniformly_convergent_on_def uniformly_Cauchy_on_def uniform_limit_sequentially_iff
6.47 +    by (simp add: *)
6.48 +qed
6.49 +
6.50 +lemma uniformly_cauchy_imp_uniformly_convergent:
6.51 +  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
6.52 +  assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
6.53 +    and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
6.54 +  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
6.55 +proof -
6.56 +  obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
6.57 +    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
6.58 +  moreover
6.59 +  {
6.60 +    fix x
6.61 +    assume "P x"
6.62 +    then have "l x = l' x"
6.63 +      using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
6.64 +      using l and assms(2) unfolding lim_sequentially by blast
6.65 +  }
6.66 +  ultimately show ?thesis by auto
6.67 +qed
6.68 +
6.69 +text \<open>TODO: remove explicit formulations
6.70 +  @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
6.71 +
6.72  lemma uniformly_convergent_imp_convergent:
6.73    "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
6.74    unfolding uniformly_convergent_on_def convergent_def
6.75 @@ -363,7 +421,7 @@
6.76  lemmas uniform_limit_uminus[uniform_limit_intros] =
6.77    bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
6.78
6.79 -lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x y. c) (\<lambda>x. c) f"
6.80 +lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x. c) c f"
6.81    by (auto intro!: uniform_limitI)
6.82
6.84 @@ -574,6 +632,24 @@
6.85    "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
6.86    by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
6.87
6.88 +lemma uniform_limit_bounded:
6.89 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::metric_space"
6.90 +  assumes l: "uniform_limit S f l F"
6.91 +  assumes bnd: "\<forall>\<^sub>F i in F. bounded (f i ` S)"
6.92 +  assumes "F \<noteq> bot"
6.93 +  shows "bounded (l ` S)"
6.94 +proof -
6.95 +  from l have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (l x) (f n x) < 1"
6.96 +    by (auto simp: uniform_limit_iff dist_commute dest!: spec[where x=1])
6.97 +  with bnd
6.98 +  have "\<forall>\<^sub>F n in F. \<exists>M. \<forall>x\<in>S. dist undefined (l x) \<le> M + 1"
6.99 +    by eventually_elim
6.100 +      (auto intro!: order_trans[OF dist_triangle2 add_mono] intro: less_imp_le
6.101 +        simp: bounded_any_center[where a=undefined])
6.102 +  then show ?thesis using assms
6.103 +    by (auto simp: bounded_any_center[where a=undefined] dest!: eventually_happens)
6.104 +qed
6.105 +
6.107    "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
6.108        uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
```
```     7.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Sun Mar 12 19:06:10 2017 +0100
7.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Fri Mar 10 23:16:40 2017 +0100
7.3 @@ -1140,6 +1140,29 @@
7.4      done
7.5  qed
7.6
7.7 +lemma Stone_Weierstrass_uniform_limit:
7.8 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
7.9 +  assumes S: "compact S"
7.10 +    and f: "continuous_on S f"
7.11 +  obtains g where "uniform_limit S g f sequentially" "\<And>n. polynomial_function (g n)"
7.12 +proof -
7.13 +  have pos: "inverse (Suc n) > 0" for n by auto
7.14 +  obtain g where g: "\<And>n. polynomial_function (g n)" "\<And>x n. x \<in> S \<Longrightarrow> norm(f x - g n x) < inverse (Suc n)"
7.15 +    using Stone_Weierstrass_polynomial_function[OF S f pos]
7.16 +    by metis
7.17 +  have "uniform_limit S g f sequentially"
7.18 +  proof (rule uniform_limitI)
7.19 +    fix e::real assume "0 < e"
7.20 +    with LIMSEQ_inverse_real_of_nat have "\<forall>\<^sub>F n in sequentially. inverse (Suc n) < e"
7.21 +      by (rule order_tendstoD)
7.22 +    moreover have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < inverse (Suc n)"
7.23 +      using g by (simp add: dist_norm norm_minus_commute)
7.24 +    ultimately show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < e"
7.25 +      by (eventually_elim) auto
7.26 +  qed
7.27 +  then show ?thesis using g(1) ..
7.28 +qed
7.29 +
7.30
7.31  subsection\<open>Polynomial functions as paths\<close>
7.32
```
```     8.1 --- a/src/HOL/Limits.thy	Sun Mar 12 19:06:10 2017 +0100
8.2 +++ b/src/HOL/Limits.thy	Fri Mar 10 23:16:40 2017 +0100
8.3 @@ -729,7 +729,7 @@
8.4      by (intro Zfun_minus) (simp add: tendsto_Zfun_iff)
8.5  qed
8.6
8.7 -lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
8.8 +lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real]
8.9
8.10
8.11  subsubsection \<open>Linear operators and multiplication\<close>
```
```     9.1 --- a/src/HOL/Topological_Spaces.thy	Sun Mar 12 19:06:10 2017 +0100
9.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 10 23:16:40 2017 +0100
9.3 @@ -150,12 +150,12 @@
9.4  instance t1_space \<subseteq> t0_space
9.5    by standard (fast dest: t1_space)
9.6
9.7 +context t1_space begin
9.8 +
9.9  lemma separation_t1: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
9.10 -  for x y :: "'a::t1_space"
9.11    using t1_space[of x y] by blast
9.12
9.13  lemma closed_singleton [iff]: "closed {a}"
9.14 -  for a :: "'a::t1_space"
9.15  proof -
9.16    let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
9.17    have "open ?T"
9.18 @@ -167,7 +167,6 @@
9.19  qed
9.20
9.21  lemma closed_insert [continuous_intros, simp]:
9.22 -  fixes a :: "'a::t1_space"
9.23    assumes "closed S"
9.24    shows "closed (insert a S)"
9.25  proof -
9.26 @@ -178,9 +177,9 @@
9.27  qed
9.28
9.29  lemma finite_imp_closed: "finite S \<Longrightarrow> closed S"
9.30 -  for S :: "'a::t1_space set"
9.31    by (induct pred: finite) simp_all
9.32
9.33 +end
9.34
9.35  text \<open>T2 spaces are also known as Hausdorff spaces.\<close>
9.36
9.37 @@ -190,12 +189,10 @@
9.38  instance t2_space \<subseteq> t1_space
9.39    by standard (fast dest: hausdorff)
9.40
9.41 -lemma separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
9.42 -  for x y :: "'a::t2_space"
9.43 +lemma (in t2_space) separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
9.44    using hausdorff [of x y] by blast
9.45
9.46 -lemma separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
9.47 -  for x y :: "'a::t0_space"
9.48 +lemma (in t0_space) separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
9.49    using t0_space [of x y] by blast
9.50
9.51
9.52 @@ -204,9 +201,9 @@
9.53  class perfect_space = topological_space +
9.54    assumes not_open_singleton: "\<not> open {x}"
9.55
9.56 -lemma UNIV_not_singleton: "UNIV \<noteq> {x}"
9.57 -  for x :: "'a::perfect_space"
9.58 -  by (metis open_UNIV not_open_singleton)
9.59 +lemma (in perfect_space) UNIV_not_singleton: "UNIV \<noteq> {x}"
9.60 +  for x::'a
9.61 +  by (metis (no_types) open_UNIV not_open_singleton)
9.62
9.63
9.64  subsection \<open>Generators for toplogies\<close>
9.65 @@ -476,10 +473,10 @@
9.66    "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
9.67    by (subst eventually_nhds) blast
9.68
9.69 -lemma eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
9.70 +lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
9.71    by (subst (asm) eventually_nhds) blast
9.72
9.73 -lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
9.74 +lemma (in topological_space) nhds_neq_bot [simp]: "nhds a \<noteq> bot"
9.75    by (simp add: trivial_limit_def eventually_nhds)
9.76
9.77  lemma (in t1_space) t1_space_nhds: "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
9.78 @@ -494,28 +491,34 @@
9.79  lemma (in discrete_topology) at_discrete: "at x within S = bot"
9.80    unfolding at_within_def nhds_discrete by simp
9.81
9.82 -lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
9.83 +lemma (in topological_space) at_within_eq:
9.84 +  "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
9.85    unfolding nhds_def at_within_def
9.86    by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)
9.87
9.88 -lemma eventually_at_filter:
9.89 +lemma (in topological_space) eventually_at_filter:
9.90    "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
9.91    by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute)
9.92
9.93 -lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
9.94 +lemma (in topological_space) at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
9.95    unfolding at_within_def by (intro inf_mono) auto
9.96
9.97 -lemma eventually_at_topological:
9.98 +lemma (in topological_space) eventually_at_topological:
9.99    "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
9.100    by (simp add: eventually_nhds eventually_at_filter)
9.101
9.102 -lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
9.103 +lemma (in topological_space) at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
9.104    unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
9.105
9.106 -lemma at_within_open_NO_MATCH: "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
9.107 +lemma (in topological_space) at_within_open_NO_MATCH:
9.108 +  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
9.109    by (simp only: at_within_open)
9.110
9.111 -lemma at_within_nhd:
9.112 +lemma (in topological_space) at_within_open_subset:
9.113 +  "a \<in> S \<Longrightarrow> open S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> at a within T = at a"
9.114 +  by (metis at_le at_within_open dual_order.antisym subset_UNIV)
9.115 +
9.116 +lemma (in topological_space) at_within_nhd:
9.117    assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
9.118    shows "at x within T = at x within U"
9.119    unfolding filter_eq_iff eventually_at_filter
9.120 @@ -526,14 +529,15 @@
9.121      by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
9.122  qed
9.123
9.124 -lemma at_within_empty [simp]: "at a within {} = bot"
9.125 +lemma (in topological_space) at_within_empty [simp]: "at a within {} = bot"
9.126    unfolding at_within_def by simp
9.127
9.128 -lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
9.129 +lemma (in topological_space) at_within_union:
9.130 +  "at x within (S \<union> T) = sup (at x within S) (at x within T)"
9.131    unfolding filter_eq_iff eventually_sup eventually_at_filter
9.132    by (auto elim!: eventually_rev_mp)
9.133
9.134 -lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
9.135 +lemma (in topological_space) at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
9.136    unfolding trivial_limit_def eventually_at_topological
9.137    apply safe
9.138     apply (case_tac "S = {a}")
9.139 @@ -542,8 +546,7 @@
9.140    apply fast
9.141    done
9.142
9.143 -lemma at_neq_bot [simp]: "at a \<noteq> bot"
9.144 -  for a :: "'a::perfect_space"
9.145 +lemma (in perfect_space) at_neq_bot [simp]: "at a \<noteq> bot"
9.146    by (simp add: at_eq_bot_iff not_open_singleton)
9.147
9.148  lemma (in order_topology) nhds_order:
9.149 @@ -556,7 +559,7 @@
9.150      by (simp only: nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def)
9.151  qed
9.152
9.153 -lemma filterlim_at_within_If:
9.154 +lemma (in topological_space) filterlim_at_within_If:
9.155    assumes "filterlim f G (at x within (A \<inter> {x. P x}))"
9.156      and "filterlim g G (at x within (A \<inter> {x. \<not>P x}))"
9.157    shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x within A)"
9.158 @@ -580,7 +583,7 @@
9.159    finally show "filterlim g G (inf (at x within A) (principal {x. \<not> P x}))" .
9.160  qed
9.161
9.162 -lemma filterlim_at_If:
9.163 +lemma (in topological_space) filterlim_at_If:
9.164    assumes "filterlim f G (at x within {x. P x})"
9.165      and "filterlim g G (at x within {x. \<not>P x})"
9.166    shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
9.167 @@ -641,22 +644,20 @@
9.168    using gt_ex[of x]
9.169    by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
9.170
9.171 -lemma at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
9.172 -  for x :: "'a::linorder_topology"
9.173 +lemma (in linorder_topology) at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
9.174    by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
9.175        elim: eventually_elim2 eventually_mono)
9.176
9.177 -lemma eventually_at_split:
9.178 +lemma (in linorder_topology) eventually_at_split:
9.179    "eventually P (at x) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
9.180 -  for x :: "'a::linorder_topology"
9.181    by (subst at_eq_sup_left_right) (simp add: eventually_sup)
9.182
9.183 -lemma eventually_at_leftI:
9.184 +lemma (in order_topology) eventually_at_leftI:
9.185    assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
9.186    shows   "eventually P (at_left b)"
9.187    using assms unfolding eventually_at_topological by (intro exI[of _ "{a<..}"]) auto
9.188
9.189 -lemma eventually_at_rightI:
9.190 +lemma (in order_topology) eventually_at_rightI:
9.191    assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
9.192    shows   "eventually P (at_right a)"
9.193    using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto
9.194 @@ -671,7 +672,7 @@
9.195  definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a"
9.196    where "Lim A f = (THE l. (f \<longlongrightarrow> l) A)"
9.197
9.198 -lemma tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
9.199 +lemma (in topological_space) tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
9.200    by simp
9.201
9.202  named_theorems tendsto_intros "introduction rules for tendsto"
9.203 @@ -682,7 +683,9 @@
9.204        |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
9.205  \<close>
9.206
9.207 -lemma (in topological_space) tendsto_def:
9.208 +context topological_space begin
9.209 +
9.210 +lemma tendsto_def:
9.211     "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
9.212     unfolding nhds_def filterlim_INF filterlim_principal by auto
9.213
9.214 @@ -692,14 +695,17 @@
9.215  lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f \<longlongrightarrow> l) F' \<Longrightarrow> (f \<longlongrightarrow> l) F"
9.216    unfolding tendsto_def le_filter_def by fast
9.217
9.218 -lemma tendsto_within_subset: "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
9.219 -  by (blast intro: tendsto_mono at_le)
9.220 -
9.221 -lemma filterlim_at:
9.222 +lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
9.223 +  by (auto simp: tendsto_def eventually_at_topological)
9.224 +
9.225 +lemma tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
9.226 +  by (simp add: tendsto_def)
9.227 +
9.228 +lemma  filterlim_at:
9.229    "(LIM x F. f x :> at b within s) \<longleftrightarrow> eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f \<longlongrightarrow> b) F"
9.230    by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
9.231
9.232 -lemma filterlim_at_withinI:
9.233 +lemma  filterlim_at_withinI:
9.234    assumes "filterlim f (nhds c) F"
9.235    assumes "eventually (\<lambda>x. f x \<in> A - {c}) F"
9.236    shows   "filterlim f (at c within A) F"
9.237 @@ -711,14 +717,23 @@
9.238    shows   "filterlim f (at c) F"
9.239    using assms by (intro filterlim_at_withinI) simp_all
9.240
9.241 -lemma (in topological_space) topological_tendstoI:
9.242 +lemma topological_tendstoI:
9.243    "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
9.244    by (auto simp: tendsto_def)
9.245
9.246 -lemma (in topological_space) topological_tendstoD:
9.247 +lemma topological_tendstoD:
9.248    "(f \<longlongrightarrow> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
9.249    by (auto simp: tendsto_def)
9.250
9.251 +lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
9.252 +  by (simp add: tendsto_def)
9.253 +
9.254 +end
9.255 +
9.256 +lemma tendsto_within_subset:
9.257 +  "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
9.258 +  by (blast intro: tendsto_mono at_le)
9.259 +
9.260  lemma (in order_topology) order_tendsto_iff:
9.261    "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
9.262    by (auto simp: nhds_order filterlim_inf filterlim_INF filterlim_principal)
9.263 @@ -734,9 +749,6 @@
9.264      and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
9.265    using assms by (auto simp: order_tendsto_iff)
9.266
9.267 -lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
9.268 -  by (simp add: tendsto_def)
9.269 -
9.270  lemma (in linorder_topology) tendsto_max:
9.271    assumes X: "(X \<longlongrightarrow> x) net"
9.272      and Y: "(Y \<longlongrightarrow> y) net"
9.273 @@ -773,11 +785,18 @@
9.274      by (auto simp: min_less_iff_disj elim: eventually_mono)
9.275  qed
9.276
9.277 -lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
9.278 -  by (auto simp: tendsto_def eventually_at_topological)
9.279 -
9.280 -lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
9.281 -  by (simp add: tendsto_def)
9.282 +lemma (in order_topology)
9.283 +  assumes "a < b"
9.284 +  shows at_within_Icc_at_right: "at a within {a..b} = at_right a"
9.285 +    and at_within_Icc_at_left:  "at b within {a..b} = at_left b"
9.286 +  using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"]
9.287 +  using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"]
9.288 +  by (auto intro!: order_class.antisym filter_leI
9.289 +      simp: eventually_at_filter less_le
9.290 +      elim: eventually_elim2)
9.291 +
9.292 +lemma (in order_topology) at_within_Icc_at: "a < x \<Longrightarrow> x < b \<Longrightarrow> at x within {a..b} = at x"
9.293 +  by (rule at_within_open_subset[where S="{a<..<b}"]) auto
9.294
9.295  lemma (in t2_space) tendsto_unique:
9.296    assumes "F \<noteq> bot"
9.297 @@ -810,22 +829,19 @@
9.298    shows "((\<lambda>x. a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
9.299    by (auto intro!: tendsto_unique [OF assms tendsto_const])
9.300
9.301 -lemma increasing_tendsto:
9.302 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
9.303 +lemma (in order_topology) increasing_tendsto:
9.304    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
9.305      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
9.306    shows "(f \<longlongrightarrow> l) F"
9.307    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
9.308
9.309 -lemma decreasing_tendsto:
9.310 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
9.311 +lemma (in order_topology) decreasing_tendsto:
9.312    assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
9.313      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
9.314    shows "(f \<longlongrightarrow> l) F"
9.315    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
9.316
9.317 -lemma tendsto_sandwich:
9.318 -  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
9.319 +lemma (in order_topology) tendsto_sandwich:
9.320    assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
9.321    assumes lim: "(f \<longlongrightarrow> c) net" "(h \<longlongrightarrow> c) net"
9.322    shows "(g \<longlongrightarrow> c) net"
9.323 @@ -839,8 +855,7 @@
9.324      using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
9.325  qed
9.326
9.327 -lemma limit_frequently_eq:
9.328 -  fixes c d :: "'a::t1_space"
9.329 +lemma (in t1_space) limit_frequently_eq:
9.330    assumes "F \<noteq> bot"
9.331      and "frequently (\<lambda>x. f x = c) F"
9.332      and "(f \<longlongrightarrow> d) F"
9.333 @@ -857,8 +872,7 @@
9.335  qed
9.336
9.337 -lemma tendsto_imp_eventually_ne:
9.338 -  fixes c :: "'a::t1_space"
9.339 +lemma (in t1_space) tendsto_imp_eventually_ne:
9.340    assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
9.341    shows "eventually (\<lambda>z. f z \<noteq> c') F"
9.342  proof (cases "F=bot")
9.343 @@ -876,8 +890,7 @@
9.344    qed
9.345  qed
9.346
9.347 -lemma tendsto_le:
9.348 -  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
9.349 +lemma (in linorder_topology) tendsto_le:
9.350    assumes F: "\<not> trivial_limit F"
9.351      and x: "(f \<longlongrightarrow> x) F"
9.352      and y: "(g \<longlongrightarrow> y) F"
9.353 @@ -895,16 +908,14 @@
9.355  qed
9.356
9.357 -lemma tendsto_lowerbound:
9.358 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
9.359 +lemma (in linorder_topology) tendsto_lowerbound:
9.360    assumes x: "(f \<longlongrightarrow> x) F"
9.361        and ev: "eventually (\<lambda>i. a \<le> f i) F"
9.362        and F: "\<not> trivial_limit F"
9.363    shows "a \<le> x"
9.364    using F x tendsto_const ev by (rule tendsto_le)
9.365
9.366 -lemma tendsto_upperbound:
9.367 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
9.368 +lemma (in linorder_topology) tendsto_upperbound:
9.369    assumes x: "(f \<longlongrightarrow> x) F"
9.370        and ev: "eventually (\<lambda>i. a \<ge> f i) F"
9.371        and F: "\<not> trivial_limit F"
9.372 @@ -1840,7 +1851,8 @@
9.373    unfolding continuous_on_def by auto
9.374
9.375  lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
9.376 -  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
9.377 +  unfolding continuous_on_def
9.378 +  by (metis subset_eq tendsto_within_subset)
9.379
9.380  lemma continuous_on_compose[continuous_intros]:
9.381    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g \<circ> f)"
9.382 @@ -1912,6 +1924,25 @@
9.383         (auto intro: less_le_trans[OF _ mono] less_imp_le)
9.384  qed
9.385
9.386 +lemma continuous_on_IccI:
9.387 +  "\<lbrakk>(f \<longlongrightarrow> f a) (at_right a);
9.388 +    (f \<longlongrightarrow> f b) (at_left b);
9.389 +    (\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> f \<midarrow>x\<rightarrow> f x); a < b\<rbrakk> \<Longrightarrow>
9.390 +    continuous_on {a .. b} f"
9.391 +  for a::"'a::linorder_topology"
9.392 +  using at_within_open[of _ "{a<..<b}"]
9.393 +  by (auto simp: continuous_on_def at_within_Icc_at_right at_within_Icc_at_left le_less
9.394 +      at_within_Icc_at)
9.395 +
9.396 +lemma
9.397 +  fixes a b::"'a::linorder_topology"
9.398 +  assumes "continuous_on {a .. b} f" "a < b"
9.399 +  shows continuous_on_Icc_at_rightD: "(f \<longlongrightarrow> f a) (at_right a)"
9.400 +    and continuous_on_Icc_at_leftD: "(f \<longlongrightarrow> f b) (at_left b)"
9.401 +  using assms
9.402 +  by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
9.403 +      dest: bspec[where x=a] bspec[where x=b])
9.404 +
9.405
9.406  subsubsection \<open>Continuity at a point\<close>
9.407
```
```    10.1 --- a/src/HOL/Transcendental.thy	Sun Mar 12 19:06:10 2017 +0100
10.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 10 23:16:40 2017 +0100
10.3 @@ -1493,6 +1493,8 @@
10.5    done
10.6
10.7 +lemmas of_real_exp = exp_of_real[symmetric]
10.8 +
10.9  corollary exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
10.10    by (metis Reals_cases Reals_of_real exp_of_real)
10.11
10.12 @@ -1795,6 +1797,10 @@
10.13    for x :: real
10.14    using ln_less_cancel_iff [of x 1] by simp
10.15
10.16 +lemma ln_le_zero_iff [simp]: "0 < x \<Longrightarrow> ln x \<le> 0 \<longleftrightarrow> x \<le> 1"
10.17 +  for x :: real
10.18 +  by (metis less_numeral_extra(1) ln_le_cancel_iff ln_one)
10.19 +
10.20  lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
10.21    for x :: real
10.22    using ln_less_cancel_iff [of 1 x] by simp
10.23 @@ -2347,6 +2353,10 @@
10.24    by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
10.25       (auto simp: eventually_at_top_dense)
10.26
10.27 +lemma filtermap_ln_at_right: "filtermap ln (at_right (0::real)) = at_bot"
10.28 +  by (auto intro!: filtermap_fun_inverse[where g="\<lambda>x. exp x"] ln_at_0
10.29 +      simp: filterlim_at exp_at_bot)
10.30 +
10.31  lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) \<longlongrightarrow> (0::real)) at_top"
10.32  proof (induct k)
10.33    case 0
```