--- a/src/HOL/Filter.thy Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Filter.thy Fri Sep 25 16:54:31 2015 +0200
@@ -390,6 +390,9 @@
lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
by (simp add: frequently_const_iff)
+lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
+ by (metis frequentlyE eventually_frequently)
+
abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
where "trivial_limit F \<equiv> F = bot"
--- a/src/HOL/Library/Extended_Real.thy Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Sep 25 16:54:31 2015 +0200
@@ -1732,6 +1732,14 @@
apply (auto split: ereal.split simp: ereal_uminus_reorder) []
done
+lemma at_infty_ereal_eq_at_top: "at \<infinity> = filtermap ereal at_top"
+ unfolding filter_eq_iff eventually_at_filter eventually_at_top_linorder eventually_filtermap
+ top_ereal_def[symmetric]
+ apply (subst eventually_nhds_top[of 0])
+ apply (auto simp: top_ereal_def less_le ereal_all_split ereal_ex_split)
+ apply (metis PInfty_neq_ereal(2) ereal_less_eq(3) ereal_top le_cases order_trans)
+ done
+
lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
by auto
@@ -3589,6 +3597,34 @@
unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
using lim_ereal by (simp_all add: comp_def)
+lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
+proof -
+ have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity"
+ by (intro tendsto_intros tendsto_inverse_0)
+
+ show ?thesis
+ by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
+ (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
+ intro!: filterlim_mono_eventually[OF **])
+qed
+
+lemma inverse_ereal_tendsto_pos:
+ fixes x :: ereal assumes "0 < x"
+ shows "inverse -- x --> inverse x"
+proof (cases x)
+ case (real r)
+ with `0 < x` have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
+ by (auto intro!: tendsto_inverse)
+ from real \<open>0 < x\<close> show ?thesis
+ by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
+ intro!: Lim_transform_eventually[OF _ **] t1_space_nhds)
+qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)
+
+lemma inverse_ereal_tendsto_at_right_0: "(inverse ---> \<infinity>) (at_right (0::ereal))"
+ unfolding tendsto_compose_filtermap[symmetric] at_right_ereal zero_ereal_def
+ by (subst filterlim_cong[OF refl refl, where g="\<lambda>x. ereal (inverse x)"])
+ (auto simp: eventually_at_filter tendsto_PInfty_eq_at_top filterlim_inverse_at_top_right)
+
lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
lemma continuous_at_iff_ereal:
--- a/src/HOL/Library/Liminf_Limsup.thy Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Fri Sep 25 16:54:31 2015 +0200
@@ -150,6 +150,17 @@
shows "Limsup F X \<le> C"
using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+lemma le_Limsup:
+ assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
+ shows "l \<le> Limsup F f"
+proof -
+ have "l = Limsup F (\<lambda>x. l)"
+ using F by (simp add: Limsup_const)
+ also have "\<dots> \<le> Limsup F f"
+ by (intro Limsup_mono x)
+ finally show ?thesis .
+qed
+
lemma le_Liminf_iff:
fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
@@ -308,4 +319,33 @@
then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
qed
+lemma continuous_on_imp_continuous_within: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
+ unfolding continuous_on_eq_continuous_within by (auto simp: continuous_within intro: tendsto_within_subset)
+
+lemma Liminf_compose_continuous_antimono:
+ fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
+ assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
+ shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
+proof -
+ { fix P assume "eventually P F"
+ have "\<exists>x. P x"
+ proof (rule ccontr)
+ assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
+ by auto
+ with \<open>eventually P F\<close> F show False
+ by auto
+ qed }
+ note * = this
+
+ have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
+ unfolding Limsup_def INF_def
+ by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
+ (auto intro: eventually_True)
+ also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+ by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
+ (auto dest!: eventually_happens simp: F)
+ finally show ?thesis
+ by (auto simp: Liminf_def)
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Sep 25 16:54:31 2015 +0200
@@ -2200,18 +2200,35 @@
definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
-lemma vector_derivative_unique_at:
- assumes "(f has_vector_derivative f') (at x)"
- and "(f has_vector_derivative f'') (at x)"
+lemma vector_derivative_unique_within:
+ assumes not_bot: "at x within s \<noteq> bot"
+ and f': "(f has_vector_derivative f') (at x within s)"
+ and f'': "(f has_vector_derivative f'') (at x within s)"
shows "f' = f''"
proof -
have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
- using assms [unfolded has_vector_derivative_def]
- by (rule frechet_derivative_unique_at)
+ proof (rule frechet_derivative_unique_within)
+ show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> s"
+ proof clarsimp
+ fix e :: real assume "0 < e"
+ with islimpt_approachable_real[of x s] not_bot
+ obtain x' where "x' \<in> s" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
+ by (auto simp add: trivial_limit_within)
+ then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> s"
+ by (intro exI[of _ "x' - x"]) auto
+ qed
+ qed (insert f' f'', auto simp: has_vector_derivative_def)
then show ?thesis
unfolding fun_eq_iff by auto
qed
+lemma vector_derivative_unique_at:
+ "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f'') (at x) \<Longrightarrow> f' = f''"
+ by (rule vector_derivative_unique_within) auto
+
+lemma differentiableI_vector: "(f has_vector_derivative y) F \<Longrightarrow> f differentiable F"
+ by (auto simp: differentiable_def has_vector_derivative_def)
+
lemma vector_derivative_works:
"f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
(is "?l = ?r")
@@ -2226,38 +2243,44 @@
by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
+lemma vector_derivative_within:
+ assumes not_bot: "at x within s \<noteq> bot" and y: "(f has_vector_derivative y) (at x within s)"
+ shows "vector_derivative f (at x within s) = y"
+ using y
+ by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
+ (auto simp: differentiable_def has_vector_derivative_def)
+
+lemma islimpt_closure_open:
+ fixes s :: "'a::perfect_space set"
+ assumes "open s" and t: "t = closure s" "x \<in> t"
+ shows "x islimpt t"
+proof cases
+ assume "x \<in> s"
+ { fix T assume "x \<in> T" "open T"
+ then have "open (s \<inter> T)"
+ using \<open>open s\<close> by auto
+ then have "s \<inter> T \<noteq> {x}"
+ using not_open_singleton[of x] by auto
+ with \<open>x \<in> T\<close> \<open>x \<in> s\<close> have "\<exists>y\<in>t. y \<in> T \<and> y \<noteq> x"
+ using closure_subset[of s] by (auto simp: t) }
+ then show ?thesis
+ by (auto intro!: islimptI)
+next
+ assume "x \<notin> s" with t show ?thesis
+ unfolding t closure_def by (auto intro: islimpt_subset)
+qed
+
lemma vector_derivative_unique_within_closed_interval:
- assumes "a < b"
- and "x \<in> cbox a b"
- assumes "(f has_vector_derivative f') (at x within cbox a b)"
- assumes "(f has_vector_derivative f'') (at x within cbox a b)"
+ assumes ab: "a < b" "x \<in> cbox a b"
+ assumes D: "(f has_vector_derivative f') (at x within cbox a b)" "(f has_vector_derivative f'') (at x within cbox a b)"
shows "f' = f''"
-proof -
- have *: "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
- apply (rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
- using assms(3-)[unfolded has_vector_derivative_def]
- using assms(1-2)
- apply auto
- done
- show ?thesis
- proof (rule ccontr)
- assume **: "f' \<noteq> f''"
- with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
- by (auto simp: fun_eq_iff)
- with ** show False
- unfolding o_def by auto
- qed
-qed
+ using ab
+ by (intro vector_derivative_unique_within[OF _ D])
+ (auto simp: trivial_limit_within intro!: islimpt_closure_open[where s="{a <..< b}"])
lemma vector_derivative_at:
"(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
- apply (rule vector_derivative_unique_at)
- defer
- apply assumption
- unfolding vector_derivative_works[symmetric] differentiable_def
- unfolding has_vector_derivative_def
- apply auto
- done
+ by (intro vector_derivative_within at_neq_bot)
lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
by (simp add: vector_derivative_at)
@@ -2292,15 +2315,12 @@
done
lemma vector_derivative_within_closed_interval:
- assumes "a < b"
- and "x \<in> cbox a b"
- assumes "(f has_vector_derivative f') (at x within cbox a b)"
+ assumes ab: "a < b" "x \<in> cbox a b"
+ assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
shows "vector_derivative f (at x within cbox a b) = f'"
- apply (rule vector_derivative_unique_within_closed_interval)
- using vector_derivative_works[unfolded differentiable_def]
- using assms
- apply (auto simp add:has_vector_derivative_def)
- done
+ by (intro vector_derivative_unique_within_closed_interval[OF ab _ f]
+ vector_derivative_works[THEN iffD1] differentiableI_vector)
+ fact
lemma has_vector_derivative_within_subset:
"(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Sep 25 16:54:31 2015 +0200
@@ -313,6 +313,46 @@
apply (metis INF_absorb centre_in_ball)
done
+lemma continuous_on_inverse_ereal: "continuous_on {0::ereal ..} inverse"
+ unfolding continuous_on_def
+proof clarsimp
+ fix x :: ereal assume "0 \<le> x"
+ moreover have "at 0 within {0 ..} = at_right (0::ereal)"
+ by (auto simp: filter_eq_iff eventually_at_filter le_less)
+ moreover have "0 < x \<Longrightarrow> at x within {0 ..} = at x"
+ using at_within_interior[of x "{0 ..}"] by (simp add: interior_Ici[of "- \<infinity>"])
+ ultimately show "(inverse ---> inverse x) (at x within {0..})"
+ by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos)
+qed
+
+
+lemma Liminf_inverse_ereal:
+ assumes nneg: "\<forall>\<^sub>F x in F. f x \<ge> (0 :: ereal)" and "F \<noteq> bot"
+ shows "Liminf F (\<lambda>n. inverse (f n)) = inverse (Limsup F f)"
+proof -
+ def I \<equiv> "\<lambda>x::ereal. if x \<le> 0 then \<infinity> else inverse x"
+ have "Liminf F (\<lambda>n. I (f n)) = I (Limsup F f)"
+ proof (rule Liminf_compose_continuous_antimono)
+ have "continuous_on ({.. 0} \<union> {0 ..}) I"
+ unfolding I_def by (intro continuous_on_cases) (auto intro: continuous_on_const continuous_on_inverse_ereal)
+ also have "{.. 0} \<union> {0::ereal ..} = UNIV"
+ by auto
+ finally show "continuous_on UNIV I" .
+ show "antimono I"
+ unfolding antimono_def I_def by (auto intro: ereal_inverse_antimono)
+ qed fact
+ also have "Liminf F (\<lambda>n. I (f n)) = Liminf F (\<lambda>n. inverse (f n))"
+ proof (rule Liminf_eq)
+ show "\<forall>\<^sub>F x in F. I (f x) = inverse (f x)"
+ using nneg by eventually_elim (auto simp: I_def)
+ qed
+ also have "0 \<le> Limsup F f"
+ by (intro le_Limsup) fact+
+ then have "I (Limsup F f) = inverse (Limsup F f)"
+ by (auto simp: I_def)
+ finally show ?thesis .
+qed
+
subsection \<open>monoset\<close>
definition (in order) mono_set:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 25 16:54:31 2015 +0200
@@ -1551,6 +1551,43 @@
qed
qed
+lemma interior_Ici:
+ fixes x :: "'a :: {dense_linorder, linorder_topology}"
+ assumes "b < x"
+ shows "interior { x ..} = { x <..}"
+proof (rule interior_unique)
+ fix T assume "T \<subseteq> {x ..}" "open T"
+ moreover have "x \<notin> T"
+ proof
+ assume "x \<in> T"
+ obtain y where "y < x" "{y <.. x} \<subseteq> T"
+ using open_left[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
+ with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
+ by (auto simp: subset_eq Ball_def)
+ with \<open>T \<subseteq> {x ..}\<close> show False by auto
+ qed
+ ultimately show "T \<subseteq> {x <..}"
+ by (auto simp: subset_eq less_le)
+qed auto
+
+lemma interior_Iic:
+ fixes x :: "'a :: {dense_linorder, linorder_topology}"
+ assumes "x < b"
+ shows "interior {.. x} = {..< x}"
+proof (rule interior_unique)
+ fix T assume "T \<subseteq> {.. x}" "open T"
+ moreover have "x \<notin> T"
+ proof
+ assume "x \<in> T"
+ obtain y where "x < y" "{x ..< y} \<subseteq> T"
+ using open_right[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
+ with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
+ by (auto simp: subset_eq Ball_def less_le)
+ with \<open>T \<subseteq> {.. x}\<close> show False by auto
+ qed
+ ultimately show "T \<subseteq> {..< x}"
+ by (auto simp: subset_eq less_le)
+qed auto
subsection \<open>Closure of a Set\<close>
@@ -1763,10 +1800,6 @@
text \<open>Some property holds "sufficiently close" to the limit point.\<close>
-lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
- unfolding trivial_limit_def
- by (auto elim: eventually_rev_mp)
-
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
by simp
--- a/src/HOL/Topological_Spaces.thy Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Fri Sep 25 16:54:31 2015 +0200
@@ -381,6 +381,17 @@
"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:
+ 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
+proof (intro allI eventually_subst)
+ have "eventually (\<lambda>x. x \<in> S) (nhds x)"
+ using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
+ then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P
+ 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"
unfolding at_within_def by simp
@@ -1574,7 +1585,7 @@
"continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"
by (simp add: continuous_within filterlim_at_split)
-subsubsection\<open>Open-cover compactness\<close>
+subsubsection \<open>Open-cover compactness\<close>
context topological_space
begin