src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
 changeset 57447 87429bdecad5 parent 57446 06e195515deb child 57865 dcfb33c26f50
```     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Jun 30 15:45:03 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Jun 30 15:45:21 2014 +0200
1.3 @@ -439,6 +439,27 @@
1.4    using tendsto_iff_Liminf_eq_Limsup[of sequentially]
1.5    by (auto simp: convergent_def)
1.6
1.7 +lemma limsup_le_liminf_real:
1.8 +  fixes X :: "nat \<Rightarrow> real" and L :: real
1.9 +  assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
1.10 +  shows "X ----> L"
1.11 +proof -
1.12 +  from 1 2 have "limsup X \<le> liminf X" by auto
1.13 +  hence 3: "limsup X = liminf X"
1.14 +    apply (subst eq_iff, rule conjI)
1.15 +    by (rule Liminf_le_Limsup, auto)
1.16 +  hence 4: "convergent (\<lambda>n. ereal (X n))"
1.17 +    by (subst convergent_ereal)
1.18 +  hence "limsup X = lim (\<lambda>n. ereal(X n))"
1.19 +    by (rule convergent_limsup_cl)
1.20 +  also from 1 2 3 have "limsup X = L" by auto
1.21 +  finally have "lim (\<lambda>n. ereal(X n)) = L" ..
1.22 +  hence "(\<lambda>n. ereal (X n)) ----> L"
1.23 +    apply (elim subst)
1.24 +    by (subst convergent_LIMSEQ_iff [symmetric], rule 4)
1.25 +  thus ?thesis by simp
1.26 +qed
1.27 +
1.28  lemma liminf_PInfty:
1.29    fixes X :: "nat \<Rightarrow> ereal"
1.30    shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
1.31 @@ -572,38 +593,52 @@
1.32      unfolding continuous_at_open by blast
1.33  qed
1.34
1.35 +lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
1.36 +  by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
1.37 +
1.38 +lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
1.39 +  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
1.40 +
1.41 +lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
1.42 +  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
1.43 +
1.44 +lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
1.45 +  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
1.46 +
1.47 +lemma
1.48 +  shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
1.49 +    and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
1.50 +  unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
1.51 +    eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
1.52 +  by (auto simp add: ereal_all_split ereal_ex_split)
1.53 +
1.54 +lemma ereal_tendsto_simps1:
1.55 +  "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
1.56 +  "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
1.57 +  "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
1.58 +  "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
1.59 +  unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
1.60 +  by (auto simp: filtermap_filtermap filtermap_ident)
1.61 +
1.62 +lemma ereal_tendsto_simps2:
1.63 +  "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
1.64 +  "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
1.65 +  "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
1.66 +  unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
1.67 +  using lim_ereal by (simp_all add: comp_def)
1.68 +
1.69 +lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
1.70 +
1.71  lemma continuous_at_iff_ereal:
1.72    fixes f :: "'a::t2_space \<Rightarrow> real"
1.73 -  shows "continuous (at x0) f \<longleftrightarrow> continuous (at x0) (ereal \<circ> f)"
1.74 -proof -
1.75 -  {
1.76 -    assume "continuous (at x0) f"
1.77 -    then have "continuous (at x0) (ereal \<circ> f)"
1.78 -      using continuous_at_ereal continuous_at_compose[of x0 f ereal]
1.79 -      by auto
1.80 -  }
1.81 -  moreover
1.82 -  {
1.83 -    assume "continuous (at x0) (ereal \<circ> f)"
1.84 -    then have "continuous (at x0) (real \<circ> (ereal \<circ> f))"
1.85 -      using continuous_at_of_ereal
1.86 -      by (intro continuous_at_compose[of x0 "ereal \<circ> f"]) auto
1.87 -    moreover have "real \<circ> (ereal \<circ> f) = f"
1.88 -      using real_ereal_id by (simp add: o_assoc)
1.89 -    ultimately have "continuous (at x0) f"
1.90 -      by auto
1.91 -  }
1.92 -  ultimately show ?thesis
1.93 -    by auto
1.94 -qed
1.95 -
1.96 +  shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
1.97 +  unfolding continuous_within comp_def lim_ereal ..
1.98
1.99  lemma continuous_on_iff_ereal:
1.100    fixes f :: "'a::t2_space => real"
1.101    assumes "open A"
1.102    shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
1.103 -  using continuous_at_iff_ereal assms
1.104 -  by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
1.105 +  unfolding continuous_on_def comp_def lim_ereal ..
1.106
1.107  lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
1.108    using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
1.109 @@ -611,7 +646,7 @@
1.110
1.111  lemma continuous_on_iff_real:
1.112    fixes f :: "'a::t2_space \<Rightarrow> ereal"
1.113 -  assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
1.114 +  assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
1.115    shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
1.116  proof -
1.117    have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
```