src/HOL/Library/Liminf_Limsup.thy
changeset 63895 9afa979137da
parent 62975 1d066f6ab25d
child 66447 a1f5c5c26fa6
     1.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Fri Sep 16 13:56:51 2016 +0200
     1.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Sep 15 16:07:20 2016 +0200
     1.3 @@ -159,6 +159,14 @@
     1.4    shows "Limsup net f = Limsup net g"
     1.5    by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
     1.6  
     1.7 +lemma Liminf_bot[simp]: "Liminf bot f = top"
     1.8 +  unfolding Liminf_def top_unique[symmetric]
     1.9 +  by (rule SUP_upper2[where i="\<lambda>x. False"]) simp_all
    1.10 +
    1.11 +lemma Limsup_bot[simp]: "Limsup bot f = bot"
    1.12 +  unfolding Limsup_def bot_unique[symmetric]
    1.13 +  by (rule INF_lower2[where i="\<lambda>x. False"]) simp_all
    1.14 +
    1.15  lemma Liminf_le_Limsup:
    1.16    assumes ntriv: "\<not> trivial_limit F"
    1.17    shows "Liminf F f \<le> Limsup F f"
    1.18 @@ -180,27 +188,26 @@
    1.19  qed
    1.20  
    1.21  lemma Liminf_bounded:
    1.22 -  assumes ntriv: "\<not> trivial_limit F"
    1.23    assumes le: "eventually (\<lambda>n. C \<le> X n) F"
    1.24    shows "C \<le> Liminf F X"
    1.25 -  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
    1.26 +  using Liminf_mono[OF le] Liminf_const[of F C]
    1.27 +  by (cases "F = bot") simp_all
    1.28  
    1.29  lemma Limsup_bounded:
    1.30 -  assumes ntriv: "\<not> trivial_limit F"
    1.31    assumes le: "eventually (\<lambda>n. X n \<le> C) F"
    1.32    shows "Limsup F X \<le> C"
    1.33 -  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
    1.34 +  using Limsup_mono[OF le] Limsup_const[of F C]
    1.35 +  by (cases "F = bot") simp_all
    1.36  
    1.37  lemma le_Limsup:
    1.38    assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
    1.39    shows "l \<le> Limsup F f"
    1.40 -proof -
    1.41 -  have "l = Limsup F (\<lambda>x. l)"
    1.42 -    using F by (simp add: Limsup_const)
    1.43 -  also have "\<dots> \<le> Limsup F f"
    1.44 -    by (intro Limsup_mono x)
    1.45 -  finally show ?thesis .
    1.46 -qed
    1.47 +  using F Liminf_bounded Liminf_le_Limsup order.trans x by blast
    1.48 +
    1.49 +lemma Liminf_le:
    1.50 +  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
    1.51 +  shows "Liminf F f \<le> l"
    1.52 +  using F Liminf_le_Limsup Limsup_bounded order.trans x by blast
    1.53  
    1.54  lemma le_Liminf_iff:
    1.55    fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
    1.56 @@ -505,6 +512,46 @@
    1.57      by (auto simp: Limsup_def)
    1.58  qed
    1.59  
    1.60 +lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
    1.61 +  apply (cases "F = bot", simp)
    1.62 +  by (subst Liminf_def)
    1.63 +    (auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least)
    1.64 +
    1.65 +lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g \<ge> Limsup F (\<lambda>x. g (f x))"
    1.66 +  apply (cases "F = bot", simp)
    1.67 +  by (subst Limsup_def)
    1.68 +    (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
    1.69 +
    1.70 +lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x:Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
    1.71 +  by (auto intro!: SUP_least simp: Liminf_def)
    1.72 +
    1.73 +lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x:Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
    1.74 +  by (auto intro!: INF_greatest simp: Limsup_def)
    1.75 +
    1.76 +lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
    1.77 +  apply (cases "F = bot", simp)
    1.78 +  apply (rule Liminf_least)
    1.79 +  subgoal for P
    1.80 +    by (auto simp: eventually_filtermap the_inv_f_f
    1.81 +        intro!: Liminf_bounded INF_lower2 eventually_mono[of P])
    1.82 +  done
    1.83 +
    1.84 +lemma Limsup_filtermap_le: "inj f \<Longrightarrow> Limsup (filtermap f F) g \<le> Limsup F (\<lambda>x. g (f x))"
    1.85 +  apply (cases "F = bot", simp)
    1.86 +  apply (rule Limsup_greatest)
    1.87 +  subgoal for P
    1.88 +    by (auto simp: eventually_filtermap the_inv_f_f
    1.89 +        intro!: Limsup_bounded SUP_upper2 eventually_mono[of P])
    1.90 +  done
    1.91 +
    1.92 +lemma Liminf_filtermap_eq: "inj f \<Longrightarrow> Liminf (filtermap f F) g = Liminf F (\<lambda>x. g (f x))"
    1.93 +  using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g]
    1.94 +  by simp
    1.95 +
    1.96 +lemma Limsup_filtermap_eq: "inj f \<Longrightarrow> Limsup (filtermap f F) g = Limsup F (\<lambda>x. g (f x))"
    1.97 +  using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f]
    1.98 +  by simp
    1.99 +
   1.100  
   1.101  subsection \<open>More Limits\<close>
   1.102