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>}"