modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Fri Mar 10 23:16:40 2017 +0100
@@ -1,7 +1,8 @@
section \<open>Bounded Continuous Functions\<close>
theory Bounded_Continuous_Function
-imports Henstock_Kurzweil_Integration
+ imports
+ Henstock_Kurzweil_Integration
begin
subsection \<open>Definition\<close>
@@ -9,162 +10,163 @@
definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
-typedef (overloaded) ('a, 'b) bcontfun =
- "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
- by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
+typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
+ "{f::'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}"
+ morphisms apply_bcontfun Bcontfun
+ by (auto intro: continuous_intros simp: bounded_def)
+
+declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
+
+setup_lifting type_definition_bcontfun
+
+lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
+ and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
+ using apply_bcontfun[of x]
+ by (auto simp: intro: continuous_on_subset)
+
+lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
+ by transfer auto
lemma bcontfunE:
- assumes "f \<in> bcontfun"
- obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y"
- using assms unfolding bcontfun_def
- by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI)
-
-lemma bcontfunE':
- assumes "f \<in> bcontfun"
- obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
- using assms bcontfunE
- by metis
+ assumes "continuous_on UNIV f" "bounded (range f)"
+ obtains g where "f = apply_bcontfun g"
+ by (blast intro: apply_bcontfun_cases assms)
-lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
- unfolding bcontfun_def
- by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)
-
-lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun"
- using bcontfunI by metis
-
-lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)"
- using Rep_bcontfun[of x]
- by (auto simp: bcontfun_def intro: continuous_on_subset)
+lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
+ by (auto intro!: continuous_intros simp: image_def)
(* TODO: Generalize to uniform spaces? *)
instantiation bcontfun :: (topological_space, metric_space) metric_space
begin
-definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
- where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
+lift_definition dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
+ is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
-definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
+definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
-definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
+definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
+lemma bounded_dist_le_SUP_dist:
+ "bounded (range f) \<Longrightarrow> bounded (range g) \<Longrightarrow> dist (f x) (g x) \<le> (SUP x. dist (f x) (g x))"
+ by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp)
+
lemma dist_bounded:
- fixes f :: "('a, 'b) bcontfun"
- shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
-proof -
- have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun)
- from bcontfunE'[OF this] obtain y where y:
- "continuous_on UNIV (Rep_bcontfun f)"
- "\<And>x. dist (Rep_bcontfun f x) undefined \<le> y"
- by auto
- have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun)
- from bcontfunE'[OF this] obtain z where z:
- "continuous_on UNIV (Rep_bcontfun g)"
- "\<And>x. dist (Rep_bcontfun g x) undefined \<le> z"
- by auto
- show ?thesis
- unfolding dist_bcontfun_def
- proof (intro cSUP_upper bdd_aboveI2)
- fix x
- have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
- dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
- by (rule dist_triangle2)
- also have "\<dots> \<le> y + z"
- using y(2)[of x] z(2)[of x] by (rule add_mono)
- finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" .
- qed simp
-qed
+ fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
+ shows "dist (f x) (g x) \<le> dist f g"
+ by transfer (auto intro!: bounded_dist_le_SUP_dist)
lemma dist_bound:
- fixes f :: "('a, 'b) bcontfun"
- assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b"
+ fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
+ assumes "\<And>x. dist (f x) (g x) \<le> b"
shows "dist f g \<le> b"
- using assms by (auto simp: dist_bcontfun_def intro: cSUP_least)
-
-lemma dist_bounded_Abs:
- fixes f g :: "'a \<Rightarrow> 'b"
- assumes "f \<in> bcontfun" "g \<in> bcontfun"
- shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)"
- by (metis Abs_bcontfun_inverse assms dist_bounded)
-
-lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun"
- by (auto intro: bcontfunI continuous_on_const)
+ using assms
+ by transfer (auto intro!: cSUP_least)
lemma dist_fun_lt_imp_dist_val_lt:
+ fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
assumes "dist f g < e"
- shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
+ shows "dist (f x) (g x) < e"
using dist_bounded assms by (rule le_less_trans)
-lemma dist_val_lt_imp_dist_fun_le:
- assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
- shows "dist f g \<le> e"
- unfolding dist_bcontfun_def
-proof (intro cSUP_least)
- fix x
- show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e"
- using assms[THEN spec[where x=x]] by (simp add: dist_norm)
-qed simp
-
instance
proof
- fix f g h :: "('a, 'b) bcontfun"
+ fix f g h :: "'a \<Rightarrow>\<^sub>C 'b"
show "dist f g = 0 \<longleftrightarrow> f = g"
proof
- have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
+ have "\<And>x. dist (f x) (g x) \<le> dist f g"
by (rule dist_bounded)
also assume "dist f g = 0"
finally show "f = g"
- by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
+ by (auto simp: apply_bcontfun_inject[symmetric])
qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
show "dist f g \<le> dist f h + dist g h"
- proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
+ proof (rule dist_bound)
fix x
- have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
- dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)"
+ have "dist (f x) (g x) \<le> dist (f x) (h x) + dist (g x) (h x)"
by (rule dist_triangle2)
- also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h"
+ also have "dist (f x) (h x) \<le> dist f h"
by (rule dist_bounded)
- also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h"
+ also have "dist (g x) (h x) \<le> dist g h"
by (rule dist_bounded)
- finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
+ finally show "dist (f x) (g x) \<le> dist f h + dist g h"
by simp
qed
qed (rule open_bcontfun_def uniformity_bcontfun_def)+
end
-lemma closed_Pi_bcontfun:
+lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set"
+ is "\<lambda>I X. Pi I X \<inter> {f. continuous_on UNIV f \<and> bounded (range f)}"
+ by auto
+
+lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X"
+ by transfer simp
+
+lemmas mem_PiCD = mem_PiC_iff[THEN iffD1]
+ and mem_PiCI = mem_PiC_iff[THEN iffD2]
+
+lemma tendsto_bcontfun_uniform_limit:
+ fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
+ assumes "(f \<longlongrightarrow> l) F"
+ shows "uniform_limit UNIV f l F"
+proof (rule uniform_limitI)
+ fix e::real assume "e > 0"
+ from tendstoD[OF assms this] have "\<forall>\<^sub>F x in F. dist (f x) l < e" .
+ then show "\<forall>\<^sub>F n in F. \<forall>x\<in>UNIV. dist ((f n) x) (l x) < e"
+ by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt)
+qed
+
+lemma uniform_limit_tendsto_bcontfun:
+ fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
+ and l::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
+ assumes "uniform_limit UNIV f l F"
+ shows "(f \<longlongrightarrow> l) F"
+proof (rule tendstoI)
+ fix e::real assume "e > 0"
+ then have "e / 2 > 0" by simp
+ from uniform_limitD[OF assms this]
+ have "\<forall>\<^sub>F i in F. \<forall>x. dist (f i x) (l x) < e / 2" by simp
+ then have "\<forall>\<^sub>F x in F. dist (f x) l \<le> e / 2"
+ by eventually_elim (blast intro: dist_bound less_imp_le)
+ then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
+ by eventually_elim (use \<open>0 < e\<close> in auto)
+qed
+
+lemma uniform_limit_bcontfunE:
+ fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
+ and l::"'a::topological_space \<Rightarrow> 'b::metric_space"
+ assumes "uniform_limit UNIV f l F" "F \<noteq> bot"
+ obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
+ where "l = l'" "(f \<longlongrightarrow> l') F"
+ by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
+ mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun uniform_limit_theorem)
+
+lemma closed_PiC:
fixes I :: "'a::metric_space set"
and X :: "'a \<Rightarrow> 'b::complete_space set"
assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
- shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))"
+ shows "closed (PiC I X)"
unfolding closed_sequential_limits
proof safe
fix f l
- assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l"
- 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"
- using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
- by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
- (metis dist_fun_lt_imp_dist_val_lt)+
- show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)"
- proof (rule, safe)
+ assume seq: "\<forall>n. f n \<in> PiC I X" and lim: "f \<longlonglongrightarrow> l"
+ show "l \<in> PiC I X"
+ proof (safe intro!: mem_PiCI)
fix x assume "x \<in> I"
then have "closed (X x)"
using assms by simp
- moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially"
- proof (rule always_eventually, safe)
- fix i
- from seq[THEN spec, of i] \<open>x \<in> I\<close>
- show "Rep_bcontfun (f i) x \<in> X x"
- by (auto simp: Abs_bcontfun_inverse)
- qed
+ moreover have "eventually (\<lambda>i. f i x \<in> X x) sequentially"
+ using seq \<open>x \<in> I\<close>
+ by (auto intro!: eventuallyI dest!: mem_PiCD simp: Pi_iff)
moreover note sequentially_bot
- moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x"
- using lim_fun by (blast intro!: metric_LIMSEQ_I)
- ultimately show "Rep_bcontfun l x \<in> X x"
+ moreover have "(\<lambda>n. (f n) x) \<longlonglongrightarrow> l x"
+ using tendsto_bcontfun_uniform_limit[OF lim]
+ by (rule tendsto_uniform_limitI) simp
+ ultimately show "l x \<in> X x"
by (rule Lim_in_closed_set)
- qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse)
+ qed
qed
@@ -174,53 +176,15 @@
proof
fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
assume "Cauchy f" \<comment> \<open>Cauchy equals uniform convergence\<close>
- then obtain g where limit_function:
- "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e"
- using uniformly_convergent_eq_cauchy[of "\<lambda>_. True"
- "\<lambda>n. Rep_bcontfun (f n)"]
- unfolding Cauchy_def
+ then obtain g where "uniform_limit UNIV f g sequentially"
+ using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" f]
+ unfolding Cauchy_def uniform_limit_sequentially_iff
by (metis dist_fun_lt_imp_dist_val_lt)
- then obtain N where fg_dist: \<comment> \<open>for an upper bound on @{term g}\<close>
- "\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1"
- by (force simp add: dist_commute)
- from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where
- f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b"
- by force
- have "g \<in> bcontfun" \<comment> \<open>The limit function is bounded and continuous\<close>
- proof (intro bcontfunI)
- show "continuous_on UNIV g"
- apply (rule bcontfunE[OF Rep_bcontfun])
- using limit_function
- by (auto simp add: uniform_limit_sequentially_iff intro: uniform_limit_theorem[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
- next
- fix x
- from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
- by (simp add: dist_norm norm_minus_commute)
- with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"]
- show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x]
- by simp
- qed
- show "convergent f"
- proof (rule convergentI, subst lim_sequentially, safe)
- \<comment> \<open>The limit function converges according to its norm\<close>
- fix e :: real
- assume "e > 0"
- then have "e/2 > 0" by simp
- with limit_function[THEN spec, of"e/2"]
- have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2"
- by simp
- then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto
- show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e"
- proof (rule, safe)
- fix n
- assume "N \<le> n"
- with N show "dist (f n) (Abs_bcontfun g) < e"
- using dist_val_lt_imp_dist_fun_le[of
- "f n" "Abs_bcontfun g" "e/2"]
- Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp
- qed
- qed
+ from uniform_limit_bcontfunE[OF this sequentially_bot]
+ obtain l' where "g = apply_bcontfun l'" "(f \<longlonglongrightarrow> l')" by metis
+ then show "convergent f"
+ by (intro convergentI)
qed
@@ -229,104 +193,42 @@
instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
begin
-definition "-f = Abs_bcontfun (\<lambda>x. -(Rep_bcontfun f x))"
-
-definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)"
+lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x"
+ by (auto intro!: continuous_intros)
-definition "f - g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x - Rep_bcontfun g x)"
-
-definition "0 = Abs_bcontfun (\<lambda>x. 0)"
-
-definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)"
+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"
+ by (auto simp: intro!: continuous_intros bounded_plus_comp)
-lemma plus_cont:
- fixes f g :: "'a \<Rightarrow> 'b"
- assumes f: "f \<in> bcontfun"
- and g: "g \<in> bcontfun"
- shows "(\<lambda>x. f x + g x) \<in> bcontfun"
-proof -
- from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
- by auto
- moreover
- from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z"
- by auto
- ultimately show ?thesis
- proof (intro bcontfunI)
- fix x
- have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)"
- by simp
- also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0"
- by (rule dist_triangle_add)
- also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
- unfolding zero_bcontfun_def using assms
- by (metis add_mono const_bcontfun dist_bounded_Abs)
- finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
- qed (simp add: continuous_on_add)
-qed
+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"
+ by (auto simp: intro!: continuous_intros bounded_minus_comp)
-lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x"
- by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun)
+lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0"
+ by (auto intro!: continuous_intros simp: image_def)
-lemma uminus_cont:
- fixes f :: "'a \<Rightarrow> 'b"
- assumes "f \<in> bcontfun"
- shows "(\<lambda>x. - f x) \<in> bcontfun"
-proof -
- from bcontfunE[OF assms, of 0] obtain y
- where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
- by auto
- then show ?thesis
- proof (intro bcontfunI)
- fix x
- assume "\<And>x. dist (f x) 0 \<le> y"
- then show "dist (- f x) 0 \<le> y"
- by (subst dist_minus[symmetric]) simp
- qed (simp add: continuous_on_minus)
-qed
+lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
+ by transfer simp
-lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
- by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)
+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"
+ by (auto simp: intro!: continuous_intros bounded_scaleR_comp)
-lemma minus_cont:
- fixes f g :: "'a \<Rightarrow> 'b"
- assumes f: "f \<in> bcontfun"
- and g: "g \<in> bcontfun"
- shows "(\<lambda>x. f x - g x) \<in> bcontfun"
- using plus_cont [of f "- g"] assms
- by (simp add: uminus_cont fun_Compl_def)
-
-lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
- by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)
+lemmas [simp] =
+ const_bcontfun.rep_eq
+ uminus_bcontfun.rep_eq
+ plus_bcontfun.rep_eq
+ minus_bcontfun.rep_eq
+ zero_bcontfun.rep_eq
+ scaleR_bcontfun.rep_eq
-lemma scaleR_cont:
- fixes a :: real
- and f :: "'a \<Rightarrow> 'b"
- assumes "f \<in> bcontfun"
- shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun"
-proof -
- from bcontfunE[OF assms, of 0] obtain y
- where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
- by auto
- then show ?thesis
- proof (intro bcontfunI)
- fix x
- assume "\<And>x. dist (f x) 0 \<le> y"
- then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
- by (metis norm_cmul_rule_thm norm_conv_dist)
- qed (simp add: continuous_intros)
-qed
-
-lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
- by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
instance
- by standard
- (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
- Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
- plus_cont const_bcontfun minus_cont scaleR_cont)
+ by standard (auto intro!: bcontfun_eqI simp: algebra_simps)
end
+lemma bounded_norm_le_SUP_norm:
+ "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
+ by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
+
instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
begin
@@ -340,179 +242,68 @@
fix a :: real
fix f g :: "('a, 'b) bcontfun"
show "dist f g = norm (f - g)"
- by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
- Abs_bcontfun_inverse const_bcontfun dist_norm)
+ unfolding norm_bcontfun_def
+ by transfer (simp add: dist_norm)
show "norm (f + g) \<le> norm f + norm g"
unfolding norm_bcontfun_def
- proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
- fix x
- have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le>
- dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0"
- by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm
- le_less_linear less_irrefl norm_triangle_lt)
- also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0"
- using dist_bounded[of f x 0]
- by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
- also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0]
- by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
- finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp
- qed
+ by transfer
+ (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm simp: dist_norm)
show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
- proof -
- have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) =
- (SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)"
- proof (intro continuous_at_Sup_mono bdd_aboveI2)
- fix x
- show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0]
- by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
- const_bcontfun)
- qed (auto intro!: monoI mult_left_mono continuous_intros)
- moreover
- have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
- (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
- by auto
- ultimately
- show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
- by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse
- zero_bcontfun_def const_bcontfun image_image)
- qed
+ unfolding norm_bcontfun_def
+ apply transfer
+ by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
+ (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
+ simp: bounded_norm_comp)
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
end
-lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
- by (metis bcontfunI dist_0_norm dist_commute)
-
lemma norm_bounded:
fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
- shows "norm (Rep_bcontfun f x) \<le> norm f"
+ shows "norm (apply_bcontfun f x) \<le> norm f"
using dist_bounded[of f x 0]
- by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
- const_bcontfun)
+ by (simp add: dist_norm)
lemma norm_bound:
fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
- assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
+ assumes "\<And>x. norm (apply_bcontfun f x) \<le> b"
shows "norm f \<le> b"
using dist_bound[of f 0 b] assms
- by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun)
-
-
-subsection \<open>Continuously Extended Functions\<close>
-
-definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- "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)"
-
-definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
- where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))"
-
-lemma ext_cont_def':
- "ext_cont f a b = Abs_bcontfun (\<lambda>x.
- 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))"
- unfolding ext_cont_def clamp_def ..
-
-lemma clamp_in_interval:
- assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
- shows "clamp a b x \<in> cbox a b"
- unfolding clamp_def
- using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
-
-lemma dist_clamps_le_dist_args:
- fixes x :: "'a::euclidean_space"
- assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
- shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
-proof -
- from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
- by (simp add: cbox_def)
- then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
- (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
- by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
- then show ?thesis
- by (auto intro: real_sqrt_le_mono
- simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
-qed
+ by (simp add: dist_norm)
-lemma clamp_continuous_at:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
- and x :: 'a
- assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
- and f_cont: "continuous_on (cbox a b) f"
- shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
- unfolding continuous_at_eps_delta
-proof safe
- fix x :: 'a
- fix e :: real
- assume "e > 0"
- moreover have "clamp a b x \<in> cbox a b"
- by (simp add: clamp_in_interval assms)
- moreover note f_cont[simplified continuous_on_iff]
- ultimately
- obtain d where d: "0 < d"
- "\<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"
- by force
- show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
- dist (f (clamp a b x')) (f (clamp a b x)) < e"
- by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans])
-qed
-
-lemma clamp_continuous_on:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
- assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
- and f_cont: "continuous_on (cbox a b) f"
- shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))"
- using assms
- by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
-
-lemma clamp_bcontfun:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
- assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
- and continuous: "continuous_on (cbox a b) f"
- shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
-proof -
- have "bounded (f ` (cbox a b))"
- by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
- then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c"
- by (auto simp add: bounded_pos)
- show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
- proof (intro bcontfun_normI)
- fix x
- show "norm (f (clamp a b x)) \<le> c"
- using clamp_in_interval[OF assms(1), of x] f_bound
- by (simp add: ext_cont_def)
- qed (simp add: clamp_continuous_on assms)
-qed
+subsection \<open>(bounded) continuous extenstion\<close>
lemma integral_clamp:
"integral {t0::real..clamp t0 t1 x} f =
(if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
by (auto simp: clamp_def)
-
-declare [[coercion Rep_bcontfun]]
+lemma continuous_on_interval_bcontfunE:
+ fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::metric_space"
+ assumes "continuous_on {a .. b} f"
+ obtains g::"'a \<Rightarrow>\<^sub>C 'b" where
+ "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> g x = f x"
+ "\<And>x. g x = f (clamp a b x)"
+proof -
+ define g where "g \<equiv> ext_cont f a b"
+ have "continuous_on UNIV g"
+ using assms
+ by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval)
+ moreover
+ have "bounded (range g)"
+ by (auto simp: g_def ext_cont_def cbox_interval
+ intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
+ ultimately
+ obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
+ then have "h x = f x" if "a \<le> x" "x \<le> b" for x
+ by (auto simp: h[symmetric] g_def cbox_interval that)
+ moreover
+ have "h x = f (clamp a b x)" for x
+ by (auto simp: h[symmetric] g_def ext_cont_def)
+ ultimately show ?thesis ..
+qed
-lemma ext_cont_cancel[simp]:
- fixes x a b :: "'a::euclidean_space"
- assumes x: "x \<in> cbox a b"
- and "continuous_on (cbox a b) f"
- shows "ext_cont f a b x = f x"
- using assms
- unfolding ext_cont_def
-proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun])
- show "f (clamp a b x) = f x"
- using x unfolding clamp_def mem_box
- by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less)
-qed (auto simp: cbox_def)
-
-lemma ext_cont_cong:
- assumes "t0 = s0"
- and "t1 = s1"
- and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
- and "continuous_on (cbox t0 t1) f"
- and "continuous_on (cbox s0 s1) g"
- and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
- shows "ext_cont f t0 t1 = ext_cont g s0 s1"
- unfolding assms ext_cont_def
- using assms clamp_in_interval[OF ord]
- by (subst Rep_bcontfun_inject[symmetric]) simp
+lifting_update bcontfun.lifting
+lifting_forget bcontfun.lifting
end
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Mar 10 23:16:40 2017 +0100
@@ -2543,4 +2543,69 @@
by simp
qed
+lemma has_integral_0_closure_imp_0:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes f: "continuous_on (closure S) f"
+ and nonneg_interior: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
+ and pos: "0 < emeasure lborel S"
+ and finite: "emeasure lborel S < \<infinity>"
+ and regular: "emeasure lborel (closure S) = emeasure lborel S"
+ and opn: "open S"
+ assumes int: "(f has_integral 0) (closure S)"
+ assumes x: "x \<in> closure S"
+ shows "f x = 0"
+proof -
+ have zero: "emeasure lborel (frontier S) = 0"
+ using finite closure_subset regular
+ unfolding frontier_def
+ by (subst emeasure_Diff) (auto simp: frontier_def interior_open \<open>open S\<close> )
+ have nonneg: "0 \<le> f x" if "x \<in> closure S" for x
+ using continuous_ge_on_closure[OF f that nonneg_interior] by simp
+ have "0 = integral (closure S) f"
+ by (blast intro: int sym)
+ also
+ note intl = has_integral_integrable[OF int]
+ have af: "f absolutely_integrable_on (closure S)"
+ using nonneg
+ by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
+ then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
+ by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
+ also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
+ by (rule integral_nonneg_eq_0_iff_AE[OF af]) (use nonneg in \<open>auto simp: indicator_def\<close>)
+ also have "\<dots> \<longleftrightarrow> (AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})"
+ by (auto simp: indicator_def)
+ finally have "(AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})" by simp
+ moreover have "(AE x in lebesgue. x \<in> - frontier S)"
+ using zero
+ by (auto simp: eventually_ae_filter null_sets_def intro!: exI[where x="frontier S"])
+ ultimately have ae: "AE x \<in> S in lebesgue. x \<in> {x \<in> closure S. f x = 0}" (is ?th)
+ by eventually_elim (use closure_subset in \<open>auto simp: \<close>)
+ have "closed {0::real}" by simp
+ with continuous_on_closed_vimage[OF closed_closure, of S f] f
+ have "closed (f -` {0} \<inter> closure S)" by blast
+ then have "closed {x \<in> closure S. f x = 0}" by (auto simp: vimage_def Int_def conj_commute)
+ with \<open>open S\<close> have "x \<in> {x \<in> closure S. f x = 0}" if "x \<in> S" for x using ae that
+ by (rule mem_closed_if_AE_lebesgue_open)
+ then have "f x = 0" if "x \<in> S" for x using that by auto
+ from continuous_constant_on_closure[OF f this \<open>x \<in> closure S\<close>]
+ show "f x = 0" .
+qed
+
+lemma has_integral_0_cbox_imp_0:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes f: "continuous_on (cbox a b) f"
+ and nonneg_interior: "\<And>x. x \<in> box a b \<Longrightarrow> 0 \<le> f x"
+ assumes int: "(f has_integral 0) (cbox a b)"
+ assumes ne: "box a b \<noteq> {}"
+ assumes x: "x \<in> cbox a b"
+ shows "f x = 0"
+proof -
+ have "0 < emeasure lborel (box a b)"
+ using ne x unfolding emeasure_lborel_box_eq
+ by (force intro!: prod_pos simp: mem_box algebra_simps)
+ then show ?thesis using assms
+ by (intro has_integral_0_closure_imp_0[of "box a b" f x])
+ (auto simp: emeasure_lborel_box_eq emeasure_lborel_cbox_eq algebra_simps mem_box)
+qed
+
end
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Mar 10 23:16:40 2017 +0100
@@ -268,6 +268,9 @@
subsection \<open>Basic theorems about integrals.\<close>
+lemma has_integral_eq_rhs: "(f has_integral j) S \<Longrightarrow> i = j \<Longrightarrow> (f has_integral i) S"
+ by (rule forw_subst)
+
lemma has_integral_unique:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
assumes "(f has_integral k1) i"
@@ -499,6 +502,9 @@
lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) s"
by (drule_tac c="-1" in has_integral_cmul) auto
+lemma has_integral_neg_iff: "((\<lambda>x. - f x) has_integral k) s \<longleftrightarrow> (f has_integral - k) s"
+ using has_integral_neg[of f "- k"] has_integral_neg[of "\<lambda>x. - f x" k] by auto
+
lemma has_integral_add:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
assumes "(f has_integral k) s"
@@ -2604,11 +2610,14 @@
by auto
qed
-lemma integrable_continuous_real:
- fixes f :: "real \<Rightarrow> 'a::banach"
+lemma integrable_continuous_interval:
+ fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
assumes "continuous_on {a .. b} f"
shows "f integrable_on {a .. b}"
- by (metis assms box_real(2) integrable_continuous)
+ by (metis assms integrable_continuous interval_cbox)
+
+lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
+
subsection \<open>Specialization of additivity to one dimension.\<close>
@@ -4566,6 +4575,18 @@
qed
qed
+lemma indefinite_integral_continuous':
+ fixes f::"real \<Rightarrow> 'a::banach"
+ assumes "f integrable_on {a..b}"
+ shows "continuous_on {a..b} (\<lambda>x. integral {x..b} f)"
+proof -
+ have "integral {a .. b} f - integral {a .. x} f = integral {x .. b} f" if "x \<in> {a .. b}" for x
+ using integral_combine[OF _ _ assms, of x] that
+ by (auto simp: algebra_simps)
+ with _ show ?thesis
+ by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous assms)
+qed
+
subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
@@ -7282,7 +7303,7 @@
subsection \<open>Exchange uniform limit and integral\<close>
-lemma uniform_limit_integral:
+lemma uniform_limit_integral_cbox:
fixes f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
assumes u: "uniform_limit (cbox a b) f g F"
assumes c: "\<And>n. continuous_on (cbox a b) (f n)"
@@ -7344,6 +7365,17 @@
ultimately show ?thesis ..
qed
+lemma uniform_limit_integral:
+ fixes f::"'a \<Rightarrow> 'b::ordered_euclidean_space \<Rightarrow> 'c::banach"
+ assumes u: "uniform_limit {a .. b} f g F"
+ assumes c: "\<And>n. continuous_on {a .. b} (f n)"
+ assumes [simp]: "F \<noteq> bot"
+ obtains I J where
+ "\<And>n. (f n has_integral I n) {a .. b}"
+ "(g has_integral J) {a .. b}"
+ "(I \<longlongrightarrow> J) F"
+ by (metis interval_cbox assms uniform_limit_integral_cbox)
+
subsection \<open>Integration by parts\<close>
@@ -7428,15 +7460,15 @@
subsection \<open>Integration by substitution\<close>
-lemma has_integral_substitution_strong:
+lemma has_integral_substitution_general:
fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
- assumes s: "finite s" and le: "a \<le> b" "c \<le> d" "g a \<le> g b"
+ assumes s: "finite s" and le: "a \<le> b"
and subset: "g ` {a..b} \<subseteq> {c..d}"
and f [continuous_intros]: "continuous_on {c..d} f"
and g [continuous_intros]: "continuous_on {a..b} g"
and deriv [derivative_intros]:
"\<And>x. x \<in> {a..b} - s \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
- shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
+ 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}"
proof -
let ?F = "\<lambda>x. integral {c..g x} f"
have cont_int: "continuous_on {a..b} ?F"
@@ -7461,22 +7493,48 @@
have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
using le cont_int s deriv cont_int
by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
- also from subset have "g x \<in> {c..d}" if "x \<in> {a..b}" for x using that by blast
- from this[of a] this[of b] le have "c \<le> g a" "g b \<le> d" by auto
- hence "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
- by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
- hence "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f"
- by (simp add: algebra_simps)
+ also
+ from subset have "g x \<in> {c..d}" if "x \<in> {a..b}" for x using that by blast
+ 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
+ have "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f"
+ proof cases
+ assume "g a \<le> g b"
+ note le = le this
+ from cd have "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
+ by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
+ with le show ?thesis
+ by (cases "g a = g b") (simp_all add: algebra_simps)
+ next
+ assume less: "\<not>g a \<le> g b"
+ then have "g a \<ge> g b" by simp
+ note le = le this
+ from cd have "integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f"
+ by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
+ with less show ?thesis
+ by (simp_all add: algebra_simps)
+ qed
finally show ?thesis .
qed
+lemma has_integral_substitution_strong:
+ fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
+ assumes s: "finite s" and le: "a \<le> b" "g a \<le> g b"
+ and subset: "g ` {a..b} \<subseteq> {c..d}"
+ and f [continuous_intros]: "continuous_on {c..d} f"
+ and g [continuous_intros]: "continuous_on {a..b} g"
+ and deriv [derivative_intros]:
+ "\<And>x. x \<in> {a..b} - s \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
+ shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
+ using has_integral_substitution_general[OF s le(1) subset f g deriv] le(2)
+ by (cases "g a = g b") auto
+
lemma has_integral_substitution:
fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
- assumes "a \<le> b" "c \<le> d" "g a \<le> g b" "g ` {a..b} \<subseteq> {c..d}"
+ assumes "a \<le> b" "g a \<le> g b" "g ` {a..b} \<subseteq> {c..d}"
and "continuous_on {c..d} f"
and "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
- by (intro has_integral_substitution_strong[of "{}" a b c d] assms)
+ by (intro has_integral_substitution_strong[of "{}" a b g c d] assms)
(auto intro: DERIV_continuous_on assms)
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Mar 10 23:16:40 2017 +0100
@@ -586,6 +586,33 @@
ultimately show False by contradiction
qed
+lemma mem_closed_if_AE_lebesgue_open:
+ assumes "open S" "closed C"
+ assumes "AE x \<in> S in lebesgue. x \<in> C"
+ assumes "x \<in> S"
+ shows "x \<in> C"
+proof (rule ccontr)
+ assume xC: "x \<notin> C"
+ with openE[of "S - C"] assms
+ obtain e where e: "0 < e" "ball x e \<subseteq> S - C"
+ by blast
+ then obtain a b where box: "x \<in> box a b" "box a b \<subseteq> S - C"
+ by (metis rational_boxes order_trans)
+ then have "0 < emeasure lebesgue (box a b)"
+ by (auto simp: emeasure_lborel_box_eq mem_box algebra_simps intro!: prod_pos)
+ also have "\<dots> \<le> emeasure lebesgue (S - C)"
+ using assms box
+ by (auto intro!: emeasure_mono)
+ also have "\<dots> = 0"
+ using assms
+ by (auto simp: eventually_ae_filter completion.complete2 set_diff_eq null_setsD1)
+ finally show False by simp
+qed
+
+lemma mem_closed_if_AE_lebesgue: "closed C \<Longrightarrow> (AE x in lebesgue. x \<in> C) \<Longrightarrow> x \<in> C"
+ using mem_closed_if_AE_lebesgue_open[OF open_UNIV] by simp
+
+
subsection \<open>Affine transformation on the Lebesgue-Borel\<close>
lemma lborel_eqI:
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Mar 10 23:16:40 2017 +0100
@@ -3940,6 +3940,9 @@
lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
by (simp add: bounded_iff bdd_above_def)
+lemma bounded_norm_comp: "bounded ((\<lambda>x. norm (f x)) ` S) = bounded (f ` S)"
+ by (simp add: bounded_iff)
+
lemma boundedI:
assumes "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
shows "bounded S"
@@ -4056,6 +4059,19 @@
shows "bounded (- S) \<Longrightarrow> ~ (bounded S)"
using bounded_Un [of S "-S"] by (simp add: sup_compl_top)
+lemma bounded_dist_comp:
+ assumes "bounded (f ` S)" "bounded (g ` S)"
+ shows "bounded ((\<lambda>x. dist (f x) (g x)) ` S)"
+proof -
+ from assms obtain M1 M2 where *: "dist (f x) undefined \<le> M1" "dist undefined (g x) \<le> M2" if "x \<in> S" for x
+ by (auto simp: bounded_any_center[of _ undefined] dist_commute)
+ have "dist (f x) (g x) \<le> M1 + M2" if "x \<in> S" for x
+ using *[OF that]
+ by (rule order_trans[OF dist_triangle add_mono])
+ then show ?thesis
+ by (auto intro!: boundedI)
+qed
+
lemma bounded_linear_image:
assumes "bounded S"
and "bounded_linear f"
@@ -4090,6 +4106,13 @@
apply (rule bounded_linear_scaleR_right)
done
+lemma bounded_scaleR_comp:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ assumes "bounded (f ` S)"
+ shows "bounded ((\<lambda>x. r *\<^sub>R f x) ` S)"
+ using bounded_scaling[of "f ` S" r] assms
+ by (auto simp: image_image)
+
lemma bounded_translation:
fixes S :: "'a::real_normed_vector set"
assumes "bounded S"
@@ -4119,6 +4142,33 @@
shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
+lemma uminus_bounded_comp [simp]:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "bounded ((\<lambda>x. - f x) ` S) \<longleftrightarrow> bounded (f ` S)"
+ using bounded_uminus[of "f ` S"]
+ by (auto simp: image_image)
+
+lemma bounded_plus_comp:
+ fixes f g::"'a \<Rightarrow> 'b::real_normed_vector"
+ assumes "bounded (f ` S)"
+ assumes "bounded (g ` S)"
+ shows "bounded ((\<lambda>x. f x + g x) ` S)"
+proof -
+ {
+ fix B C
+ assume "\<And>x. x\<in>S \<Longrightarrow> norm (f x) \<le> B" "\<And>x. x\<in>S \<Longrightarrow> norm (g x) \<le> C"
+ then have "\<And>x. x \<in> S \<Longrightarrow> norm (f x + g x) \<le> B + C"
+ by (auto intro!: norm_triangle_le add_mono)
+ } then show ?thesis
+ using assms by (fastforce simp: bounded_iff)
+qed
+
+lemma bounded_minus_comp:
+ "bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
+ for f g::"'a \<Rightarrow> 'b::real_normed_vector"
+ using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
+ by (auto simp: )
+
subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
@@ -5915,89 +5965,6 @@
then show ?thesis ..
qed
-text\<open>Cauchy-type criteria for uniform convergence.\<close>
-
-lemma uniformly_convergent_eq_cauchy:
- fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
- shows
- "(\<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>
- (\<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)"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs
- 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"
- by auto
- {
- fix e :: real
- assume "e > 0"
- then obtain N :: nat where N: "\<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e / 2"
- using l[THEN spec[where x="e/2"]] by auto
- {
- fix n m :: nat and x :: "'b"
- assume "N \<le> m \<and> N \<le> n \<and> P x"
- then have "dist (s m x) (s n x) < e"
- using N[THEN spec[where x=m], THEN spec[where x=x]]
- using N[THEN spec[where x=n], THEN spec[where x=x]]
- using dist_triangle_half_l[of "s m x" "l x" e "s n x"] by auto
- }
- 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
- }
- then show ?rhs by auto
-next
- assume ?rhs
- then have "\<forall>x. P x \<longrightarrow> Cauchy (\<lambda>n. s n x)"
- unfolding cauchy_def
- apply auto
- apply (erule_tac x=e in allE)
- apply auto
- done
- then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l x) sequentially"
- unfolding convergent_eq_Cauchy[symmetric]
- using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l) sequentially"]
- by auto
- {
- fix e :: real
- assume "e > 0"
- 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"
- using \<open>?rhs\<close>[THEN spec[where x="e/2"]] by auto
- {
- fix x
- assume "P x"
- then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2"
- using l[THEN spec[where x=x], unfolded lim_sequentially] and \<open>e > 0\<close>
- by (auto elim!: allE[where x="e/2"])
- fix n :: nat
- assume "n \<ge> N"
- then have "dist(s n x)(l x) < e"
- using \<open>P x\<close>and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]]
- using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"]
- by (auto simp add: dist_commute)
- }
- then have "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
- by auto
- }
- then show ?lhs by auto
-qed
-
-lemma uniformly_cauchy_imp_uniformly_convergent:
- fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
- 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"
- and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
- shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
-proof -
- 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"
- using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
- moreover
- {
- fix x
- assume "P x"
- then have "l x = l' x"
- using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
- using l and assms(2) unfolding lim_sequentially by blast
- }
- ultimately show ?thesis by auto
-qed
-
subsection \<open>Continuity\<close>
@@ -10960,6 +10927,109 @@
by blast
+
+subsection \<open>Continuous Extension\<close>
+
+definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
+ 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)
+ else a)"
+
+lemma clamp_in_interval[simp]:
+ assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
+ shows "clamp a b x \<in> cbox a b"
+ unfolding clamp_def
+ using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
+
+lemma clamp_cancel_cbox[simp]:
+ fixes x a b :: "'a::euclidean_space"
+ assumes x: "x \<in> cbox a b"
+ shows "clamp a b x = x"
+ using assms
+ by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
+
+lemma clamp_empty_interval:
+ assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
+ shows "clamp a b = (\<lambda>_. a)"
+ using assms
+ by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
+
+lemma dist_clamps_le_dist_args:
+ fixes x :: "'a::euclidean_space"
+ shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
+proof cases
+ assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+ then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
+ (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
+ by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
+ then show ?thesis
+ by (auto intro: real_sqrt_le_mono
+ simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
+qed (auto simp: clamp_def)
+
+lemma clamp_continuous_at:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+ and x :: 'a
+ assumes f_cont: "continuous_on (cbox a b) f"
+ shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
+proof cases
+ assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+ show ?thesis
+ unfolding continuous_at_eps_delta
+ proof safe
+ fix x :: 'a
+ fix e :: real
+ assume "e > 0"
+ moreover have "clamp a b x \<in> cbox a b"
+ by (simp add: clamp_in_interval le)
+ moreover note f_cont[simplified continuous_on_iff]
+ ultimately
+ obtain d where d: "0 < d"
+ "\<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"
+ by force
+ show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
+ dist (f (clamp a b x')) (f (clamp a b x)) < e"
+ using le
+ by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
+ qed
+qed (auto simp: clamp_empty_interval)
+
+lemma clamp_continuous_on:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+ assumes f_cont: "continuous_on (cbox a b) f"
+ shows "continuous_on S (\<lambda>x. f (clamp a b x))"
+ using assms
+ by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
+
+lemma clamp_bounded:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+ assumes bounded: "bounded (f ` (cbox a b))"
+ shows "bounded (range (\<lambda>x. f (clamp a b x)))"
+proof cases
+ assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+ from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
+ by (auto simp add: bounded_any_center[where a=undefined])
+ then show ?thesis
+ by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
+ simp: bounded_any_center[where a=undefined])
+qed (auto simp: clamp_empty_interval image_def)
+
+
+definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
+ where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
+
+lemma ext_cont_cancel_cbox[simp]:
+ fixes x a b :: "'a::euclidean_space"
+ assumes x: "x \<in> cbox a b"
+ shows "ext_cont f a b x = f x"
+ using assms
+ unfolding ext_cont_def
+ by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
+
+lemma continuous_on_ext_cont[continuous_intros]:
+ "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
+ by (auto intro!: clamp_continuous_on simp: ext_cont_def)
+
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Analysis/Uniform_Limit.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Fri Mar 10 23:16:40 2017 +0100
@@ -203,6 +203,8 @@
lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
+text\<open>Cauchy-type criteria for uniform convergence.\<close>
+
lemma Cauchy_uniformly_convergent:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
assumes "uniformly_Cauchy_on X f"
@@ -235,6 +237,62 @@
qed
qed
+lemma uniformly_convergent_Cauchy:
+ assumes "uniformly_convergent_on X f"
+ shows "uniformly_Cauchy_on X f"
+proof (rule uniformly_Cauchy_onI)
+ fix e::real assume "e > 0"
+ then have "0 < e / 2" by simp
+ with assms[unfolded uniformly_convergent_on_def uniform_limit_sequentially_iff]
+ obtain l N where l:"x \<in> X \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f n x) (l x) < e / 2" for n x
+ by metis
+ 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
+ by (rule dist_triangle_half_l)
+ 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
+qed
+
+lemma uniformly_convergent_eq_Cauchy:
+ "uniformly_convergent_on X f = uniformly_Cauchy_on X f" for f::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
+ using Cauchy_uniformly_convergent uniformly_convergent_Cauchy by blast
+
+lemma uniformly_convergent_eq_cauchy:
+ fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
+ shows
+ "(\<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>
+ (\<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)"
+proof -
+ 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)"
+ "(\<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)"
+ for N::nat and Q::"'b \<Rightarrow> bool" and R S
+ by blast+
+ show ?thesis
+ using uniformly_convergent_eq_Cauchy[of "Collect P" s]
+ unfolding uniformly_convergent_on_def uniformly_Cauchy_on_def uniform_limit_sequentially_iff
+ by (simp add: *)
+qed
+
+lemma uniformly_cauchy_imp_uniformly_convergent:
+ fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
+ 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"
+ and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
+ shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
+proof -
+ 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"
+ using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
+ moreover
+ {
+ fix x
+ assume "P x"
+ then have "l x = l' x"
+ using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
+ using l and assms(2) unfolding lim_sequentially by blast
+ }
+ ultimately show ?thesis by auto
+qed
+
+text \<open>TODO: remove explicit formulations
+ @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
+
lemma uniformly_convergent_imp_convergent:
"uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
unfolding uniformly_convergent_on_def convergent_def
@@ -363,7 +421,7 @@
lemmas uniform_limit_uminus[uniform_limit_intros] =
bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
-lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x y. c) (\<lambda>x. c) f"
+lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x. c) c f"
by (auto intro!: uniform_limitI)
lemma uniform_limit_add[uniform_limit_intros]:
@@ -574,6 +632,24 @@
"uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
+lemma uniform_limit_bounded:
+ fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::metric_space"
+ assumes l: "uniform_limit S f l F"
+ assumes bnd: "\<forall>\<^sub>F i in F. bounded (f i ` S)"
+ assumes "F \<noteq> bot"
+ shows "bounded (l ` S)"
+proof -
+ from l have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (l x) (f n x) < 1"
+ by (auto simp: uniform_limit_iff dist_commute dest!: spec[where x=1])
+ with bnd
+ have "\<forall>\<^sub>F n in F. \<exists>M. \<forall>x\<in>S. dist undefined (l x) \<le> M + 1"
+ by eventually_elim
+ (auto intro!: order_trans[OF dist_triangle2 add_mono] intro: less_imp_le
+ simp: bounded_any_center[where a=undefined])
+ then show ?thesis using assms
+ by (auto simp: bounded_any_center[where a=undefined] dest!: eventually_happens)
+qed
+
lemma uniformly_convergent_add:
"uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Fri Mar 10 23:16:40 2017 +0100
@@ -1140,6 +1140,29 @@
done
qed
+lemma Stone_Weierstrass_uniform_limit:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes S: "compact S"
+ and f: "continuous_on S f"
+ obtains g where "uniform_limit S g f sequentially" "\<And>n. polynomial_function (g n)"
+proof -
+ have pos: "inverse (Suc n) > 0" for n by auto
+ 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)"
+ using Stone_Weierstrass_polynomial_function[OF S f pos]
+ by metis
+ have "uniform_limit S g f sequentially"
+ proof (rule uniform_limitI)
+ fix e::real assume "0 < e"
+ with LIMSEQ_inverse_real_of_nat have "\<forall>\<^sub>F n in sequentially. inverse (Suc n) < e"
+ by (rule order_tendstoD)
+ moreover have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < inverse (Suc n)"
+ using g by (simp add: dist_norm norm_minus_commute)
+ ultimately show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < e"
+ by (eventually_elim) auto
+ qed
+ then show ?thesis using g(1) ..
+qed
+
subsection\<open>Polynomial functions as paths\<close>
--- a/src/HOL/Limits.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Limits.thy Fri Mar 10 23:16:40 2017 +0100
@@ -729,7 +729,7 @@
by (intro Zfun_minus) (simp add: tendsto_Zfun_iff)
qed
-lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
+lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real]
subsubsection \<open>Linear operators and multiplication\<close>
--- a/src/HOL/Topological_Spaces.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Mar 10 23:16:40 2017 +0100
@@ -150,12 +150,12 @@
instance t1_space \<subseteq> t0_space
by standard (fast dest: t1_space)
+context t1_space begin
+
lemma separation_t1: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
- for x y :: "'a::t1_space"
using t1_space[of x y] by blast
lemma closed_singleton [iff]: "closed {a}"
- for a :: "'a::t1_space"
proof -
let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
have "open ?T"
@@ -167,7 +167,6 @@
qed
lemma closed_insert [continuous_intros, simp]:
- fixes a :: "'a::t1_space"
assumes "closed S"
shows "closed (insert a S)"
proof -
@@ -178,9 +177,9 @@
qed
lemma finite_imp_closed: "finite S \<Longrightarrow> closed S"
- for S :: "'a::t1_space set"
by (induct pred: finite) simp_all
+end
text \<open>T2 spaces are also known as Hausdorff spaces.\<close>
@@ -190,12 +189,10 @@
instance t2_space \<subseteq> t1_space
by standard (fast dest: hausdorff)
-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 = {})"
- for x y :: "'a::t2_space"
+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 = {})"
using hausdorff [of x y] by blast
-lemma separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
- for x y :: "'a::t0_space"
+lemma (in t0_space) separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
using t0_space [of x y] by blast
@@ -204,9 +201,9 @@
class perfect_space = topological_space +
assumes not_open_singleton: "\<not> open {x}"
-lemma UNIV_not_singleton: "UNIV \<noteq> {x}"
- for x :: "'a::perfect_space"
- by (metis open_UNIV not_open_singleton)
+lemma (in perfect_space) UNIV_not_singleton: "UNIV \<noteq> {x}"
+ for x::'a
+ by (metis (no_types) open_UNIV not_open_singleton)
subsection \<open>Generators for toplogies\<close>
@@ -476,10 +473,10 @@
"open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
by (subst eventually_nhds) blast
-lemma eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
+lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
by (subst (asm) eventually_nhds) blast
-lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
+lemma (in topological_space) nhds_neq_bot [simp]: "nhds a \<noteq> bot"
by (simp add: trivial_limit_def eventually_nhds)
lemma (in t1_space) t1_space_nhds: "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
@@ -494,28 +491,34 @@
lemma (in discrete_topology) at_discrete: "at x within S = bot"
unfolding at_within_def nhds_discrete by simp
-lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
+lemma (in topological_space) at_within_eq:
+ "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
unfolding nhds_def at_within_def
by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)
-lemma eventually_at_filter:
+lemma (in topological_space) eventually_at_filter:
"eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute)
-lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
+lemma (in topological_space) at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
unfolding at_within_def by (intro inf_mono) auto
-lemma eventually_at_topological:
+lemma (in topological_space) eventually_at_topological:
"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))"
by (simp add: eventually_nhds eventually_at_filter)
-lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
+lemma (in topological_space) at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
-lemma at_within_open_NO_MATCH: "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
+lemma (in topological_space) at_within_open_NO_MATCH:
+ "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
by (simp only: at_within_open)
-lemma at_within_nhd:
+lemma (in topological_space) at_within_open_subset:
+ "a \<in> S \<Longrightarrow> open S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> at a within T = at a"
+ by (metis at_le at_within_open dual_order.antisym subset_UNIV)
+
+lemma (in topological_space) at_within_nhd:
assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
shows "at x within T = at x within U"
unfolding filter_eq_iff eventually_at_filter
@@ -526,14 +529,15 @@
by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
qed
-lemma at_within_empty [simp]: "at a within {} = bot"
+lemma (in topological_space) at_within_empty [simp]: "at a within {} = bot"
unfolding at_within_def by simp
-lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
+lemma (in topological_space) at_within_union:
+ "at x within (S \<union> T) = sup (at x within S) (at x within T)"
unfolding filter_eq_iff eventually_sup eventually_at_filter
by (auto elim!: eventually_rev_mp)
-lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
+lemma (in topological_space) at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
unfolding trivial_limit_def eventually_at_topological
apply safe
apply (case_tac "S = {a}")
@@ -542,8 +546,7 @@
apply fast
done
-lemma at_neq_bot [simp]: "at a \<noteq> bot"
- for a :: "'a::perfect_space"
+lemma (in perfect_space) at_neq_bot [simp]: "at a \<noteq> bot"
by (simp add: at_eq_bot_iff not_open_singleton)
lemma (in order_topology) nhds_order:
@@ -556,7 +559,7 @@
by (simp only: nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def)
qed
-lemma filterlim_at_within_If:
+lemma (in topological_space) filterlim_at_within_If:
assumes "filterlim f G (at x within (A \<inter> {x. P x}))"
and "filterlim g G (at x within (A \<inter> {x. \<not>P x}))"
shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x within A)"
@@ -580,7 +583,7 @@
finally show "filterlim g G (inf (at x within A) (principal {x. \<not> P x}))" .
qed
-lemma filterlim_at_If:
+lemma (in topological_space) filterlim_at_If:
assumes "filterlim f G (at x within {x. P x})"
and "filterlim g G (at x within {x. \<not>P x})"
shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
@@ -641,22 +644,20 @@
using gt_ex[of x]
by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
-lemma at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
- for x :: "'a::linorder_topology"
+lemma (in linorder_topology) at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
elim: eventually_elim2 eventually_mono)
-lemma eventually_at_split:
+lemma (in linorder_topology) eventually_at_split:
"eventually P (at x) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
- for x :: "'a::linorder_topology"
by (subst at_eq_sup_left_right) (simp add: eventually_sup)
-lemma eventually_at_leftI:
+lemma (in order_topology) eventually_at_leftI:
assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
shows "eventually P (at_left b)"
using assms unfolding eventually_at_topological by (intro exI[of _ "{a<..}"]) auto
-lemma eventually_at_rightI:
+lemma (in order_topology) eventually_at_rightI:
assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
shows "eventually P (at_right a)"
using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto
@@ -671,7 +672,7 @@
definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a"
where "Lim A f = (THE l. (f \<longlongrightarrow> l) A)"
-lemma tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
+lemma (in topological_space) tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
by simp
named_theorems tendsto_intros "introduction rules for tendsto"
@@ -682,7 +683,9 @@
|> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
\<close>
-lemma (in topological_space) tendsto_def:
+context topological_space begin
+
+lemma tendsto_def:
"(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
unfolding nhds_def filterlim_INF filterlim_principal by auto
@@ -692,14 +695,17 @@
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f \<longlongrightarrow> l) F' \<Longrightarrow> (f \<longlongrightarrow> l) F"
unfolding tendsto_def le_filter_def by fast
-lemma tendsto_within_subset: "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
- by (blast intro: tendsto_mono at_le)
-
-lemma filterlim_at:
+lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
+ by (auto simp: tendsto_def eventually_at_topological)
+
+lemma tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
+ by (simp add: tendsto_def)
+
+lemma filterlim_at:
"(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"
by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
-lemma filterlim_at_withinI:
+lemma filterlim_at_withinI:
assumes "filterlim f (nhds c) F"
assumes "eventually (\<lambda>x. f x \<in> A - {c}) F"
shows "filterlim f (at c within A) F"
@@ -711,14 +717,23 @@
shows "filterlim f (at c) F"
using assms by (intro filterlim_at_withinI) simp_all
-lemma (in topological_space) topological_tendstoI:
+lemma topological_tendstoI:
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
by (auto simp: tendsto_def)
-lemma (in topological_space) topological_tendstoD:
+lemma topological_tendstoD:
"(f \<longlongrightarrow> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
by (auto simp: tendsto_def)
+lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
+ by (simp add: tendsto_def)
+
+end
+
+lemma tendsto_within_subset:
+ "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
+ by (blast intro: tendsto_mono at_le)
+
lemma (in order_topology) order_tendsto_iff:
"(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)"
by (auto simp: nhds_order filterlim_inf filterlim_INF filterlim_principal)
@@ -734,9 +749,6 @@
and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
using assms by (auto simp: order_tendsto_iff)
-lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
- by (simp add: tendsto_def)
-
lemma (in linorder_topology) tendsto_max:
assumes X: "(X \<longlongrightarrow> x) net"
and Y: "(Y \<longlongrightarrow> y) net"
@@ -773,11 +785,18 @@
by (auto simp: min_less_iff_disj elim: eventually_mono)
qed
-lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
- by (auto simp: tendsto_def eventually_at_topological)
-
-lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
- by (simp add: tendsto_def)
+lemma (in order_topology)
+ assumes "a < b"
+ shows at_within_Icc_at_right: "at a within {a..b} = at_right a"
+ and at_within_Icc_at_left: "at b within {a..b} = at_left b"
+ using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"]
+ using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"]
+ by (auto intro!: order_class.antisym filter_leI
+ simp: eventually_at_filter less_le
+ elim: eventually_elim2)
+
+lemma (in order_topology) at_within_Icc_at: "a < x \<Longrightarrow> x < b \<Longrightarrow> at x within {a..b} = at x"
+ by (rule at_within_open_subset[where S="{a<..<b}"]) auto
lemma (in t2_space) tendsto_unique:
assumes "F \<noteq> bot"
@@ -810,22 +829,19 @@
shows "((\<lambda>x. a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
by (auto intro!: tendsto_unique [OF assms tendsto_const])
-lemma increasing_tendsto:
- fixes f :: "_ \<Rightarrow> 'a::order_topology"
+lemma (in order_topology) increasing_tendsto:
assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
shows "(f \<longlongrightarrow> l) F"
using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
-lemma decreasing_tendsto:
- fixes f :: "_ \<Rightarrow> 'a::order_topology"
+lemma (in order_topology) decreasing_tendsto:
assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
shows "(f \<longlongrightarrow> l) F"
using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
-lemma tendsto_sandwich:
- fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
+lemma (in order_topology) tendsto_sandwich:
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
assumes lim: "(f \<longlongrightarrow> c) net" "(h \<longlongrightarrow> c) net"
shows "(g \<longlongrightarrow> c) net"
@@ -839,8 +855,7 @@
using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
qed
-lemma limit_frequently_eq:
- fixes c d :: "'a::t1_space"
+lemma (in t1_space) limit_frequently_eq:
assumes "F \<noteq> bot"
and "frequently (\<lambda>x. f x = c) F"
and "(f \<longlongrightarrow> d) F"
@@ -857,8 +872,7 @@
unfolding frequently_def by contradiction
qed
-lemma tendsto_imp_eventually_ne:
- fixes c :: "'a::t1_space"
+lemma (in t1_space) tendsto_imp_eventually_ne:
assumes "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
shows "eventually (\<lambda>z. f z \<noteq> c') F"
proof (cases "F=bot")
@@ -876,8 +890,7 @@
qed
qed
-lemma tendsto_le:
- fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
+lemma (in linorder_topology) tendsto_le:
assumes F: "\<not> trivial_limit F"
and x: "(f \<longlongrightarrow> x) F"
and y: "(g \<longlongrightarrow> y) F"
@@ -895,16 +908,14 @@
by (simp add: eventually_False)
qed
-lemma tendsto_lowerbound:
- fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
+lemma (in linorder_topology) tendsto_lowerbound:
assumes x: "(f \<longlongrightarrow> x) F"
and ev: "eventually (\<lambda>i. a \<le> f i) F"
and F: "\<not> trivial_limit F"
shows "a \<le> x"
using F x tendsto_const ev by (rule tendsto_le)
-lemma tendsto_upperbound:
- fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
+lemma (in linorder_topology) tendsto_upperbound:
assumes x: "(f \<longlongrightarrow> x) F"
and ev: "eventually (\<lambda>i. a \<ge> f i) F"
and F: "\<not> trivial_limit F"
@@ -1840,7 +1851,8 @@
unfolding continuous_on_def by auto
lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
- unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
+ unfolding continuous_on_def
+ by (metis subset_eq tendsto_within_subset)
lemma continuous_on_compose[continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g \<circ> f)"
@@ -1912,6 +1924,25 @@
(auto intro: less_le_trans[OF _ mono] less_imp_le)
qed
+lemma continuous_on_IccI:
+ "\<lbrakk>(f \<longlongrightarrow> f a) (at_right a);
+ (f \<longlongrightarrow> f b) (at_left b);
+ (\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> f \<midarrow>x\<rightarrow> f x); a < b\<rbrakk> \<Longrightarrow>
+ continuous_on {a .. b} f"
+ for a::"'a::linorder_topology"
+ using at_within_open[of _ "{a<..<b}"]
+ by (auto simp: continuous_on_def at_within_Icc_at_right at_within_Icc_at_left le_less
+ at_within_Icc_at)
+
+lemma
+ fixes a b::"'a::linorder_topology"
+ assumes "continuous_on {a .. b} f" "a < b"
+ shows continuous_on_Icc_at_rightD: "(f \<longlongrightarrow> f a) (at_right a)"
+ and continuous_on_Icc_at_leftD: "(f \<longlongrightarrow> f b) (at_left b)"
+ using assms
+ by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
+ dest: bspec[where x=a] bspec[where x=b])
+
subsubsection \<open>Continuity at a point\<close>
--- a/src/HOL/Transcendental.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Transcendental.thy Fri Mar 10 23:16:40 2017 +0100
@@ -1493,6 +1493,8 @@
apply (simp add: scaleR_conv_of_real)
done
+lemmas of_real_exp = exp_of_real[symmetric]
+
corollary exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
by (metis Reals_cases Reals_of_real exp_of_real)
@@ -1795,6 +1797,10 @@
for x :: real
using ln_less_cancel_iff [of x 1] by simp
+lemma ln_le_zero_iff [simp]: "0 < x \<Longrightarrow> ln x \<le> 0 \<longleftrightarrow> x \<le> 1"
+ for x :: real
+ by (metis less_numeral_extra(1) ln_le_cancel_iff ln_one)
+
lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
for x :: real
using ln_less_cancel_iff [of 1 x] by simp
@@ -2347,6 +2353,10 @@
by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
(auto simp: eventually_at_top_dense)
+lemma filtermap_ln_at_right: "filtermap ln (at_right (0::real)) = at_bot"
+ by (auto intro!: filtermap_fun_inverse[where g="\<lambda>x. exp x"] ln_at_0
+ simp: filterlim_at exp_at_bot)
+
lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) \<longlongrightarrow> (0::real)) at_top"
proof (induct k)
case 0