author hoelzl Fri Sep 25 16:54:31 2015 +0200 (2015-09-25) changeset 61245 b77bf45efe21 parent 61244 6026c14f5e5d child 61270 28eb608b9b59
prove Liminf_inverse_ereal
```     1.1 --- a/src/HOL/Filter.thy	Thu Sep 24 15:21:12 2015 +0200
1.2 +++ b/src/HOL/Filter.thy	Fri Sep 25 16:54:31 2015 +0200
1.3 @@ -390,6 +390,9 @@
1.4  lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
1.6
1.7 +lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
1.8 +  by (metis frequentlyE eventually_frequently)
1.9 +
1.10  abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
1.11    where "trivial_limit F \<equiv> F = bot"
1.12
```
```     2.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Sep 24 15:21:12 2015 +0200
2.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 25 16:54:31 2015 +0200
2.3 @@ -1732,6 +1732,14 @@
2.4    apply (auto split: ereal.split simp: ereal_uminus_reorder) []
2.5    done
2.6
2.7 +lemma at_infty_ereal_eq_at_top: "at \<infinity> = filtermap ereal at_top"
2.8 +  unfolding filter_eq_iff eventually_at_filter eventually_at_top_linorder eventually_filtermap
2.9 +    top_ereal_def[symmetric]
2.10 +  apply (subst eventually_nhds_top[of 0])
2.11 +  apply (auto simp: top_ereal_def less_le ereal_all_split ereal_ex_split)
2.12 +  apply (metis PInfty_neq_ereal(2) ereal_less_eq(3) ereal_top le_cases order_trans)
2.13 +  done
2.14 +
2.15  lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
2.16    using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
2.17    by auto
2.18 @@ -3589,6 +3597,34 @@
2.19    unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
2.20    using lim_ereal by (simp_all add: comp_def)
2.21
2.22 +lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
2.23 +proof -
2.24 +  have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity"
2.25 +    by (intro tendsto_intros tendsto_inverse_0)
2.26 +
2.27 +  show ?thesis
2.28 +    by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
2.29 +       (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
2.30 +             intro!: filterlim_mono_eventually[OF **])
2.31 +qed
2.32 +
2.33 +lemma inverse_ereal_tendsto_pos:
2.34 +  fixes x :: ereal assumes "0 < x"
2.35 +  shows "inverse -- x --> inverse x"
2.36 +proof (cases x)
2.37 +  case (real r)
2.38 +  with `0 < x` have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
2.39 +    by (auto intro!: tendsto_inverse)
2.40 +  from real \<open>0 < x\<close> show ?thesis
2.41 +    by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
2.42 +             intro!: Lim_transform_eventually[OF _ **] t1_space_nhds)
2.43 +qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)
2.44 +
2.45 +lemma inverse_ereal_tendsto_at_right_0: "(inverse ---> \<infinity>) (at_right (0::ereal))"
2.46 +  unfolding tendsto_compose_filtermap[symmetric] at_right_ereal zero_ereal_def
2.47 +  by (subst filterlim_cong[OF refl refl, where g="\<lambda>x. ereal (inverse x)"])
2.48 +     (auto simp: eventually_at_filter tendsto_PInfty_eq_at_top filterlim_inverse_at_top_right)
2.49 +
2.50  lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
2.51
2.52  lemma continuous_at_iff_ereal:
```
```     3.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Thu Sep 24 15:21:12 2015 +0200
3.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Fri Sep 25 16:54:31 2015 +0200
3.3 @@ -150,6 +150,17 @@
3.4    shows "Limsup F X \<le> C"
3.5    using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
3.6
3.7 +lemma le_Limsup:
3.8 +  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
3.9 +  shows "l \<le> Limsup F f"
3.10 +proof -
3.11 +  have "l = Limsup F (\<lambda>x. l)"
3.12 +    using F by (simp add: Limsup_const)
3.13 +  also have "\<dots> \<le> Limsup F f"
3.14 +    by (intro Limsup_mono x)
3.15 +  finally show ?thesis .
3.16 +qed
3.17 +
3.18  lemma le_Liminf_iff:
3.19    fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
3.20    shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
3.21 @@ -308,4 +319,33 @@
3.22    then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
3.23  qed
3.24
3.25 +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"
3.26 +  unfolding continuous_on_eq_continuous_within by (auto simp: continuous_within intro: tendsto_within_subset)
3.27 +
3.28 +lemma Liminf_compose_continuous_antimono:
3.29 +  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
3.30 +  assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
3.31 +  shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
3.32 +proof -
3.33 +  { fix P assume "eventually P F"
3.34 +    have "\<exists>x. P x"
3.35 +    proof (rule ccontr)
3.36 +      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
3.37 +        by auto
3.38 +      with \<open>eventually P F\<close> F show False
3.39 +        by auto
3.40 +    qed }
3.41 +  note * = this
3.42 +
3.43 +  have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
3.44 +    unfolding Limsup_def INF_def
3.45 +    by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
3.46 +       (auto intro: eventually_True)
3.47 +  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
3.48 +    by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
3.49 +       (auto dest!: eventually_happens simp: F)
3.50 +  finally show ?thesis
3.51 +    by (auto simp: Liminf_def)
3.52 +qed
3.53 +
3.54  end
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 24 15:21:12 2015 +0200
4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Sep 25 16:54:31 2015 +0200
4.3 @@ -2200,18 +2200,35 @@
4.4
4.5  definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
4.6
4.7 -lemma vector_derivative_unique_at:
4.8 -  assumes "(f has_vector_derivative f') (at x)"
4.9 -    and "(f has_vector_derivative f'') (at x)"
4.10 +lemma vector_derivative_unique_within:
4.11 +  assumes not_bot: "at x within s \<noteq> bot"
4.12 +    and f': "(f has_vector_derivative f') (at x within s)"
4.13 +    and f'': "(f has_vector_derivative f'') (at x within s)"
4.14    shows "f' = f''"
4.15  proof -
4.16    have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
4.17 -    using assms [unfolded has_vector_derivative_def]
4.18 -    by (rule frechet_derivative_unique_at)
4.19 +  proof (rule frechet_derivative_unique_within)
4.20 +    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"
4.21 +    proof clarsimp
4.22 +      fix e :: real assume "0 < e"
4.23 +      with islimpt_approachable_real[of x s] not_bot
4.24 +      obtain x' where "x' \<in> s" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
4.25 +        by (auto simp add: trivial_limit_within)
4.26 +      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> s"
4.27 +        by (intro exI[of _ "x' - x"]) auto
4.28 +    qed
4.29 +  qed (insert f' f'', auto simp: has_vector_derivative_def)
4.30    then show ?thesis
4.31      unfolding fun_eq_iff by auto
4.32  qed
4.33
4.34 +lemma vector_derivative_unique_at:
4.35 +  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f'') (at x) \<Longrightarrow> f' = f''"
4.36 +  by (rule vector_derivative_unique_within) auto
4.37 +
4.38 +lemma differentiableI_vector: "(f has_vector_derivative y) F \<Longrightarrow> f differentiable F"
4.39 +  by (auto simp: differentiable_def has_vector_derivative_def)
4.40 +
4.41  lemma vector_derivative_works:
4.42    "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
4.43      (is "?l = ?r")
4.44 @@ -2226,38 +2243,44 @@
4.45      by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
4.46  qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
4.47
4.48 +lemma vector_derivative_within:
4.49 +  assumes not_bot: "at x within s \<noteq> bot" and y: "(f has_vector_derivative y) (at x within s)"
4.50 +  shows "vector_derivative f (at x within s) = y"
4.51 +  using y
4.52 +  by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
4.53 +     (auto simp: differentiable_def has_vector_derivative_def)
4.54 +
4.55 +lemma islimpt_closure_open:
4.56 +  fixes s :: "'a::perfect_space set"
4.57 +  assumes "open s" and t: "t = closure s" "x \<in> t"
4.58 +  shows "x islimpt t"
4.59 +proof cases
4.60 +  assume "x \<in> s"
4.61 +  { fix T assume "x \<in> T" "open T"
4.62 +    then have "open (s \<inter> T)"
4.63 +      using \<open>open s\<close> by auto
4.64 +    then have "s \<inter> T \<noteq> {x}"
4.65 +      using not_open_singleton[of x] by auto
4.66 +    with \<open>x \<in> T\<close> \<open>x \<in> s\<close> have "\<exists>y\<in>t. y \<in> T \<and> y \<noteq> x"
4.67 +      using closure_subset[of s] by (auto simp: t) }
4.68 +  then show ?thesis
4.69 +    by (auto intro!: islimptI)
4.70 +next
4.71 +  assume "x \<notin> s" with t show ?thesis
4.72 +    unfolding t closure_def by (auto intro: islimpt_subset)
4.73 +qed
4.74 +
4.75  lemma vector_derivative_unique_within_closed_interval:
4.76 -  assumes "a < b"
4.77 -    and "x \<in> cbox a b"
4.78 -  assumes "(f has_vector_derivative f') (at x within cbox a b)"
4.79 -  assumes "(f has_vector_derivative f'') (at x within cbox a b)"
4.80 +  assumes ab: "a < b" "x \<in> cbox a b"
4.81 +  assumes D: "(f has_vector_derivative f') (at x within cbox a b)" "(f has_vector_derivative f'') (at x within cbox a b)"
4.82    shows "f' = f''"
4.83 -proof -
4.84 -  have *: "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
4.85 -    apply (rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
4.86 -    using assms(3-)[unfolded has_vector_derivative_def]
4.87 -    using assms(1-2)
4.88 -    apply auto
4.89 -    done
4.90 -  show ?thesis
4.91 -  proof (rule ccontr)
4.92 -    assume **: "f' \<noteq> f''"
4.93 -    with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
4.94 -      by (auto simp: fun_eq_iff)
4.95 -    with ** show False
4.96 -      unfolding o_def by auto
4.97 -  qed
4.98 -qed
4.99 +  using ab
4.100 +  by (intro vector_derivative_unique_within[OF _ D])
4.101 +     (auto simp: trivial_limit_within intro!: islimpt_closure_open[where s="{a <..< b}"])
4.102
4.103  lemma vector_derivative_at:
4.104    "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
4.105 -  apply (rule vector_derivative_unique_at)
4.106 -  defer
4.107 -  apply assumption
4.108 -  unfolding vector_derivative_works[symmetric] differentiable_def
4.109 -  unfolding has_vector_derivative_def
4.110 -  apply auto
4.111 -  done
4.112 +  by (intro vector_derivative_within at_neq_bot)
4.113
4.114  lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
4.116 @@ -2292,15 +2315,12 @@
4.117  done
4.118
4.119  lemma vector_derivative_within_closed_interval:
4.120 -  assumes "a < b"
4.121 -    and "x \<in> cbox a b"
4.122 -  assumes "(f has_vector_derivative f') (at x within cbox a b)"
4.123 +  assumes ab: "a < b" "x \<in> cbox a b"
4.124 +  assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
4.125    shows "vector_derivative f (at x within cbox a b) = f'"
4.126 -  apply (rule vector_derivative_unique_within_closed_interval)
4.127 -  using vector_derivative_works[unfolded differentiable_def]
4.128 -  using assms
4.129 -  apply (auto simp add:has_vector_derivative_def)
4.130 -  done
4.131 +  by (intro vector_derivative_unique_within_closed_interval[OF ab _ f]
4.132 +            vector_derivative_works[THEN iffD1] differentiableI_vector)
4.133 +     fact
4.134
4.135  lemma has_vector_derivative_within_subset:
4.136    "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
```
```     5.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Sep 24 15:21:12 2015 +0200
5.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Sep 25 16:54:31 2015 +0200
5.3 @@ -313,6 +313,46 @@
5.4    apply (metis INF_absorb centre_in_ball)
5.5    done
5.6
5.7 +lemma continuous_on_inverse_ereal: "continuous_on {0::ereal ..} inverse"
5.8 +  unfolding continuous_on_def
5.9 +proof clarsimp
5.10 +  fix x :: ereal assume "0 \<le> x"
5.11 +  moreover have "at 0 within {0 ..} = at_right (0::ereal)"
5.12 +    by (auto simp: filter_eq_iff eventually_at_filter le_less)
5.13 +  moreover have "0 < x \<Longrightarrow> at x within {0 ..} = at x"
5.14 +    using at_within_interior[of x "{0 ..}"] by (simp add: interior_Ici[of "- \<infinity>"])
5.15 +  ultimately show "(inverse ---> inverse x) (at x within {0..})"
5.16 +    by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos)
5.17 +qed
5.18 +
5.19 +
5.20 +lemma Liminf_inverse_ereal:
5.21 +  assumes nneg: "\<forall>\<^sub>F x in F. f x \<ge> (0 :: ereal)" and "F \<noteq> bot"
5.22 +  shows "Liminf F (\<lambda>n. inverse (f n)) = inverse (Limsup F f)"
5.23 +proof -
5.24 +  def I \<equiv> "\<lambda>x::ereal. if x \<le> 0 then \<infinity> else inverse x"
5.25 +  have "Liminf F (\<lambda>n. I (f n)) = I (Limsup F f)"
5.26 +  proof (rule Liminf_compose_continuous_antimono)
5.27 +    have "continuous_on ({.. 0} \<union> {0 ..}) I"
5.28 +      unfolding I_def by (intro continuous_on_cases) (auto intro: continuous_on_const continuous_on_inverse_ereal)
5.29 +    also have "{.. 0} \<union> {0::ereal ..} = UNIV"
5.30 +      by auto
5.31 +    finally show "continuous_on UNIV I" .
5.32 +    show "antimono I"
5.33 +      unfolding antimono_def I_def by (auto intro: ereal_inverse_antimono)
5.34 +  qed fact
5.35 +  also have "Liminf F (\<lambda>n. I (f n)) = Liminf F (\<lambda>n. inverse (f n))"
5.36 +  proof (rule Liminf_eq)
5.37 +    show "\<forall>\<^sub>F x in F. I (f x) = inverse (f x)"
5.38 +      using nneg by eventually_elim (auto simp: I_def)
5.39 +  qed
5.40 +  also have "0 \<le> Limsup F f"
5.41 +    by (intro le_Limsup) fact+
5.42 +  then have "I (Limsup F f) = inverse (Limsup F f)"
5.43 +    by (auto simp: I_def)
5.44 +  finally show ?thesis .
5.45 +qed
5.46 +
5.47  subsection \<open>monoset\<close>
5.48
5.49  definition (in order) mono_set:
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 24 15:21:12 2015 +0200
6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 25 16:54:31 2015 +0200
6.3 @@ -1551,6 +1551,43 @@
6.4    qed
6.5  qed
6.6
6.7 +lemma interior_Ici:
6.8 +  fixes x :: "'a :: {dense_linorder, linorder_topology}"
6.9 +  assumes "b < x"
6.10 +  shows "interior { x ..} = { x <..}"
6.11 +proof (rule interior_unique)
6.12 +  fix T assume "T \<subseteq> {x ..}" "open T"
6.13 +  moreover have "x \<notin> T"
6.14 +  proof
6.15 +    assume "x \<in> T"
6.16 +    obtain y where "y < x" "{y <.. x} \<subseteq> T"
6.17 +      using open_left[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
6.18 +    with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
6.19 +      by (auto simp: subset_eq Ball_def)
6.20 +    with \<open>T \<subseteq> {x ..}\<close> show False by auto
6.21 +  qed
6.22 +  ultimately show "T \<subseteq> {x <..}"
6.23 +    by (auto simp: subset_eq less_le)
6.24 +qed auto
6.25 +
6.26 +lemma interior_Iic:
6.27 +  fixes x :: "'a :: {dense_linorder, linorder_topology}"
6.28 +  assumes "x < b"
6.29 +  shows "interior {.. x} = {..< x}"
6.30 +proof (rule interior_unique)
6.31 +  fix T assume "T \<subseteq> {.. x}" "open T"
6.32 +  moreover have "x \<notin> T"
6.33 +  proof
6.34 +    assume "x \<in> T"
6.35 +    obtain y where "x < y" "{x ..< y} \<subseteq> T"
6.36 +      using open_right[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
6.37 +    with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
6.38 +      by (auto simp: subset_eq Ball_def less_le)
6.39 +    with \<open>T \<subseteq> {.. x}\<close> show False by auto
6.40 +  qed
6.41 +  ultimately show "T \<subseteq> {..< x}"
6.42 +    by (auto simp: subset_eq less_le)
6.43 +qed auto
6.44
6.45  subsection \<open>Closure of a Set\<close>
6.46
6.47 @@ -1763,10 +1800,6 @@
6.48
6.49  text \<open>Some property holds "sufficiently close" to the limit point.\<close>
6.50
6.51 -lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
6.52 -  unfolding trivial_limit_def
6.53 -  by (auto elim: eventually_rev_mp)
6.54 -
6.55  lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
6.56    by simp
6.57
```
```     7.1 --- a/src/HOL/Topological_Spaces.thy	Thu Sep 24 15:21:12 2015 +0200
7.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Sep 25 16:54:31 2015 +0200
7.3 @@ -381,6 +381,17 @@
7.4    "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
7.5    by (simp only: at_within_open)
7.6
7.7 +lemma at_within_nhd:
7.8 +  assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
7.9 +  shows "at x within T = at x within U"
7.10 +  unfolding filter_eq_iff eventually_at_filter
7.11 +proof (intro allI eventually_subst)
7.12 +  have "eventually (\<lambda>x. x \<in> S) (nhds x)"
7.13 +    using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
7.14 +  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
7.15 +    by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
7.16 +qed
7.17 +
7.18  lemma at_within_empty [simp]: "at a within {} = bot"
7.19    unfolding at_within_def by simp
7.20
7.21 @@ -1574,7 +1585,7 @@
7.22    "continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"
7.23    by (simp add: continuous_within filterlim_at_split)
7.24
7.25 -subsubsection\<open>Open-cover compactness\<close>
7.26 +subsubsection \<open>Open-cover compactness\<close>
7.27
7.28  context topological_space
7.29  begin
```