--- a/src/HOL/Filter.thy Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Filter.thy Tue Jul 14 19:08:40 2015 +0200
@@ -602,8 +602,10 @@
finally show ?thesis .
qed
-lemma eventually_gt_at_top:
- "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
+lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
+ unfolding eventually_at_top_dense by auto
+
+lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
unfolding eventually_at_top_dense by auto
definition at_bot :: "('a::order) filter"
@@ -631,6 +633,9 @@
finally show ?thesis .
qed
+lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
+ unfolding eventually_at_bot_dense by auto
+
lemma eventually_gt_at_bot:
"eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
unfolding eventually_at_bot_dense by auto
@@ -778,6 +783,21 @@
lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
by (simp add: filtermap_mono_strong eq_iff)
+lemma filtermap_fun_inverse:
+ assumes g: "filterlim g F G"
+ assumes f: "filterlim f G F"
+ assumes ev: "eventually (\<lambda>x. f (g x) = x) G"
+ shows "filtermap f F = G"
+proof (rule antisym)
+ show "filtermap f F \<le> G"
+ using f unfolding filterlim_def .
+ have "G = filtermap f (filtermap g G)"
+ using ev by (auto elim: eventually_elim2 simp: filter_eq_iff eventually_filtermap)
+ also have "\<dots> \<le> filtermap f F"
+ using g by (intro filtermap_mono) (simp add: filterlim_def)
+ finally show "G \<le> filtermap f F" .
+qed
+
lemma filterlim_principal:
"(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
unfolding filterlim_def eventually_filtermap le_principal ..
--- a/src/HOL/Library/Extended_Real.thy Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue Jul 14 19:08:40 2015 +0200
@@ -1697,6 +1697,7 @@
show "\<exists>a b::ereal. a \<noteq> b"
using zero_neq_one by blast
qed
+
subsubsection "Topological space"
instantiation ereal :: linear_continuum_topology
@@ -1710,14 +1711,17 @@
end
+lemma continuous_on_compose':
+ "continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> f`s \<subseteq> t \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
+ using continuous_on_compose[of s f g] continuous_on_subset[of t g "f`s"] by auto
+
+lemma continuous_on_ereal[continuous_intros]:
+ assumes f: "continuous_on s f" shows "continuous_on s (\<lambda>x. ereal (f x))"
+ by (rule continuous_on_compose'[OF f continuous_onI_mono[of ereal UNIV]]) auto
+
lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
- apply (rule tendsto_compose[where g=ereal])
- apply (auto intro!: order_tendstoI simp: eventually_at_topological)
- apply (rule_tac x="case a of MInfty \<Rightarrow> UNIV | ereal x \<Rightarrow> {x <..} | PInfty \<Rightarrow> {}" in exI)
- apply (auto split: ereal.split) []
- apply (rule_tac x="case a of MInfty \<Rightarrow> {} | ereal x \<Rightarrow> {..< x} | PInfty \<Rightarrow> UNIV" in exI)
- apply (auto split: ereal.split) []
- done
+ using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"]
+ by (simp add: continuous_on_eq_continuous_at)
lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) ---> - x) F"
apply (rule tendsto_compose[where g=uminus])
@@ -1808,9 +1812,6 @@
lemma continuous_at_ereal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ereal (f x))"
unfolding continuous_def by auto
-lemma continuous_on_ereal[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. ereal (f x))"
- unfolding continuous_on_def by auto
-
lemma ereal_Sup:
assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
shows "ereal (Sup A) = (SUP a:A. ereal a)"
--- a/src/HOL/Limits.thy Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Limits.thy Tue Jul 14 19:08:40 2015 +0200
@@ -901,30 +901,13 @@
lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
-lemma filtermap_homeomorph:
- assumes f: "continuous (at a) f"
- assumes g: "continuous (at (f a)) g"
- assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
- shows "filtermap f (nhds a) = nhds (f a)"
- unfolding filter_eq_iff eventually_filtermap eventually_nhds
-proof safe
- fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
- from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
- show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
-next
- fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
- with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
- obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
- by (metis UNIV_I)
- with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
- by (force intro!: exI[of _ A])
-qed
-
lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
- by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
+ by (rule filtermap_fun_inverse[where g="\<lambda>x. x + d"])
+ (auto intro!: tendsto_eq_intros filterlim_ident)
lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
- by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
+ by (rule filtermap_fun_inverse[where g=uminus])
+ (auto intro!: tendsto_eq_intros filterlim_ident)
lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
@@ -960,9 +943,17 @@
"eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
+lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
+ unfolding filterlim_at_top eventually_at_bot_dense
+ by (metis leI minus_less_iff order_less_asym)
+
+lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
+ unfolding filterlim_at_bot eventually_at_top_dense
+ by (metis leI less_minus_iff order_less_asym)
+
lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
- unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
- by (metis le_minus_iff minus_minus)
+ by (rule filtermap_fun_inverse[symmetric, of uminus])
+ (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
@@ -973,14 +964,6 @@
lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \<longleftrightarrow> (LIM x at_top. f (-x::real) :> F)"
unfolding filterlim_def at_bot_mirror filtermap_filtermap ..
-lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
- unfolding filterlim_at_top eventually_at_bot_dense
- by (metis leI minus_less_iff order_less_asym)
-
-lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
- unfolding filterlim_at_bot eventually_at_top_dense
- by (metis leI less_minus_iff order_less_asym)
-
lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_bot)"
using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F]
using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
@@ -999,20 +982,6 @@
by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
qed
-lemma filterlim_inverse_at_top:
- "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
- by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
- (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
-
-lemma filterlim_inverse_at_bot_neg:
- "LIM x (at_left (0::real)). inverse x :> at_bot"
- by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
-
-lemma filterlim_inverse_at_bot:
- "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
- unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
- by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
-
lemma tendsto_inverse_0:
fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
shows "(inverse ---> (0::'a)) at_infinity"
@@ -1029,18 +998,28 @@
qed
qed
+lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)"
+ unfolding filterlim_at
+ by (auto simp: eventually_at_top_dense)
+ (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
+
+lemma filterlim_inverse_at_top:
+ "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
+ by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
+ (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
+
+lemma filterlim_inverse_at_bot_neg:
+ "LIM x (at_left (0::real)). inverse x :> at_bot"
+ by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
+
+lemma filterlim_inverse_at_bot:
+ "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
+ unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
+ by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
+
lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
-proof (rule antisym)
- have "(inverse ---> (0::real)) at_top"
- by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
- then show "filtermap inverse at_top \<le> at_right (0::real)"
- by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
-next
- have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
- using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
- then show "at_right (0::real) \<le> filtermap inverse at_top"
- by (simp add: filtermap_ident filtermap_filtermap)
-qed
+ by (intro filtermap_fun_inverse[symmetric, where g=inverse])
+ (auto intro: filterlim_inverse_at_top_right filterlim_inverse_at_right_top)
lemma eventually_at_right_to_top:
"eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top"
--- a/src/HOL/Topological_Spaces.thy Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Jul 14 19:08:40 2015 +0200
@@ -1423,6 +1423,61 @@
"continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
using continuous_on_compose[of s f g] by (simp add: comp_def)
+lemma continuous_on_generate_topology:
+ assumes *: "open = generate_topology X"
+ assumes **: "\<And>B. B \<in> X \<Longrightarrow> \<exists>C. open C \<and> C \<inter> A = f -` B \<inter> A"
+ shows "continuous_on A f"
+ unfolding continuous_on_open_invariant
+proof safe
+ fix B :: "'a set" assume "open B" then show "\<exists>C. open C \<and> C \<inter> A = f -` B \<inter> A"
+ unfolding *
+ proof induction
+ case (UN K)
+ then obtain C where "\<And>k. k \<in> K \<Longrightarrow> open (C k)" "\<And>k. k \<in> K \<Longrightarrow> C k \<inter> A = f -` k \<inter> A"
+ by metis
+ then show ?case
+ by (intro exI[of _ "\<Union>k\<in>K. C k"]) blast
+ qed (auto intro: **)
+qed
+
+lemma continuous_onI_mono:
+ fixes f :: "'a::linorder_topology \<Rightarrow> 'b::{dense_order, linorder_topology}"
+ assumes "open (f`A)"
+ assumes mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+ shows "continuous_on A f"
+proof (rule continuous_on_generate_topology[OF open_generated_order], safe)
+ have monoD: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x < f y \<Longrightarrow> x < y"
+ by (auto simp: not_le[symmetric] mono)
+
+ { fix a b assume "a \<in> A" "f a < b"
+ moreover
+ with open_right[OF \<open>open (f`A)\<close>, of "f a" b] obtain y where "f a < y" "{f a ..< y} \<subseteq> f`A"
+ by auto
+ moreover then obtain z where "f a < z" "z < min b y"
+ using dense[of "f a" "min b y"] \<open>f a < y\<close> \<open>f a < b\<close> by auto
+ moreover then obtain c where "z = f c" "c \<in> A"
+ using \<open>{f a ..< y} \<subseteq> f`A\<close>[THEN subsetD, of z] by (auto simp: less_imp_le)
+ ultimately have "\<exists>x. x \<in> A \<and> f x < b \<and> a < x"
+ by (auto intro!: exI[of _ c] simp: monoD) }
+ then show "\<exists>C. open C \<and> C \<inter> A = f -` {..<b} \<inter> A" for b
+ by (intro exI[of _ "(\<Union>x\<in>{x\<in>A. f x < b}. {..< x})"])
+ (auto intro: le_less_trans[OF mono] less_imp_le)
+
+ { fix a b assume "a \<in> A" "b < f a"
+ moreover
+ with open_left[OF \<open>open (f`A)\<close>, of "f a" b] obtain y where "y < f a" "{y <.. f a} \<subseteq> f`A"
+ by auto
+ moreover then obtain z where "max b y < z" "z < f a"
+ using dense[of "max b y" "f a"] \<open>y < f a\<close> \<open>b < f a\<close> by auto
+ moreover then obtain c where "z = f c" "c \<in> A"
+ using \<open>{y <.. f a} \<subseteq> f`A\<close>[THEN subsetD, of z] by (auto simp: less_imp_le)
+ ultimately have "\<exists>x. x \<in> A \<and> b < f x \<and> x < a"
+ by (auto intro!: exI[of _ c] simp: monoD) }
+ then show "\<exists>C. open C \<and> C \<inter> A = f -` {b <..} \<inter> A" for b
+ by (intro exI[of _ "(\<Union>x\<in>{x\<in>A. b < f x}. {x <..})"])
+ (auto intro: less_le_trans[OF _ mono] less_imp_le)
+qed
+
subsubsection {* Continuity at a point *}
definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
--- a/src/HOL/Transcendental.thy Tue Jul 14 19:08:27 2015 +0200
+++ b/src/HOL/Transcendental.thy Tue Jul 14 19:08:40 2015 +0200
@@ -2016,6 +2016,13 @@
by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
(auto intro: eventually_gt_at_top)
+lemma filtermap_ln_at_top: "filtermap (ln::real \<Rightarrow> real) at_top = at_top"
+ by (intro filtermap_fun_inverse[of exp] exp_at_top ln_at_top) auto
+
+lemma filtermap_exp_at_top: "filtermap (exp::real \<Rightarrow> real) at_top = at_top"
+ by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
+ (auto simp: eventually_at_top_dense)
+
lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
proof (induct k)
case 0