# HG changeset patch
# User hoelzl
# Date 1443192871 -7200
# Node ID b77bf45efe21c9da659a94d4bdcd19b0b8d90cda
# Parent  6026c14f5e5dc3dc127b62a10bf49660bb343b48
prove Liminf_inverse_ereal

diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Filter.thy
--- 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"
 
diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Library/Extended_Real.thy
--- 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:
diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Library/Liminf_Limsup.thy
--- 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
diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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)"
diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- 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:
diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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
 
diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Topological_Spaces.thy
--- 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