src/HOL/Library/Liminf_Limsup.thy
changeset 63895 9afa979137da
parent 62975 1d066f6ab25d
child 66447 a1f5c5c26fa6
equal deleted inserted replaced
63886:685fb01256af 63895:9afa979137da
   156 
   156 
   157 lemma Limsup_eq:
   157 lemma Limsup_eq:
   158   assumes "eventually (\<lambda>x. f x = g x) net"
   158   assumes "eventually (\<lambda>x. f x = g x) net"
   159   shows "Limsup net f = Limsup net g"
   159   shows "Limsup net f = Limsup net g"
   160   by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
   160   by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
       
   161 
       
   162 lemma Liminf_bot[simp]: "Liminf bot f = top"
       
   163   unfolding Liminf_def top_unique[symmetric]
       
   164   by (rule SUP_upper2[where i="\<lambda>x. False"]) simp_all
       
   165 
       
   166 lemma Limsup_bot[simp]: "Limsup bot f = bot"
       
   167   unfolding Limsup_def bot_unique[symmetric]
       
   168   by (rule INF_lower2[where i="\<lambda>x. False"]) simp_all
   161 
   169 
   162 lemma Liminf_le_Limsup:
   170 lemma Liminf_le_Limsup:
   163   assumes ntriv: "\<not> trivial_limit F"
   171   assumes ntriv: "\<not> trivial_limit F"
   164   shows "Liminf F f \<le> Limsup F f"
   172   shows "Liminf F f \<le> Limsup F f"
   165   unfolding Limsup_def Liminf_def
   173   unfolding Limsup_def Liminf_def
   178     by (rule SUP_mono) auto
   186     by (rule SUP_mono) auto
   179   finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
   187   finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
   180 qed
   188 qed
   181 
   189 
   182 lemma Liminf_bounded:
   190 lemma Liminf_bounded:
   183   assumes ntriv: "\<not> trivial_limit F"
       
   184   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   191   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   185   shows "C \<le> Liminf F X"
   192   shows "C \<le> Liminf F X"
   186   using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
   193   using Liminf_mono[OF le] Liminf_const[of F C]
       
   194   by (cases "F = bot") simp_all
   187 
   195 
   188 lemma Limsup_bounded:
   196 lemma Limsup_bounded:
   189   assumes ntriv: "\<not> trivial_limit F"
       
   190   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   197   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   191   shows "Limsup F X \<le> C"
   198   shows "Limsup F X \<le> C"
   192   using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
   199   using Limsup_mono[OF le] Limsup_const[of F C]
       
   200   by (cases "F = bot") simp_all
   193 
   201 
   194 lemma le_Limsup:
   202 lemma le_Limsup:
   195   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
   203   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
   196   shows "l \<le> Limsup F f"
   204   shows "l \<le> Limsup F f"
   197 proof -
   205   using F Liminf_bounded Liminf_le_Limsup order.trans x by blast
   198   have "l = Limsup F (\<lambda>x. l)"
   206 
   199     using F by (simp add: Limsup_const)
   207 lemma Liminf_le:
   200   also have "\<dots> \<le> Limsup F f"
   208   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
   201     by (intro Limsup_mono x)
   209   shows "Liminf F f \<le> l"
   202   finally show ?thesis .
   210   using F Liminf_le_Limsup Limsup_bounded order.trans x by blast
   203 qed
       
   204 
   211 
   205 lemma le_Liminf_iff:
   212 lemma le_Liminf_iff:
   206   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   213   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   207   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   214   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   208 proof -
   215 proof -
   503        (auto dest!: eventually_happens simp: F)
   510        (auto dest!: eventually_happens simp: F)
   504   finally show ?thesis
   511   finally show ?thesis
   505     by (auto simp: Limsup_def)
   512     by (auto simp: Limsup_def)
   506 qed
   513 qed
   507 
   514 
       
   515 lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
       
   516   apply (cases "F = bot", simp)
       
   517   by (subst Liminf_def)
       
   518     (auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least)
       
   519 
       
   520 lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g \<ge> Limsup F (\<lambda>x. g (f x))"
       
   521   apply (cases "F = bot", simp)
       
   522   by (subst Limsup_def)
       
   523     (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
       
   524 
       
   525 lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x:Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
       
   526   by (auto intro!: SUP_least simp: Liminf_def)
       
   527 
       
   528 lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x:Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
       
   529   by (auto intro!: INF_greatest simp: Limsup_def)
       
   530 
       
   531 lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
       
   532   apply (cases "F = bot", simp)
       
   533   apply (rule Liminf_least)
       
   534   subgoal for P
       
   535     by (auto simp: eventually_filtermap the_inv_f_f
       
   536         intro!: Liminf_bounded INF_lower2 eventually_mono[of P])
       
   537   done
       
   538 
       
   539 lemma Limsup_filtermap_le: "inj f \<Longrightarrow> Limsup (filtermap f F) g \<le> Limsup F (\<lambda>x. g (f x))"
       
   540   apply (cases "F = bot", simp)
       
   541   apply (rule Limsup_greatest)
       
   542   subgoal for P
       
   543     by (auto simp: eventually_filtermap the_inv_f_f
       
   544         intro!: Limsup_bounded SUP_upper2 eventually_mono[of P])
       
   545   done
       
   546 
       
   547 lemma Liminf_filtermap_eq: "inj f \<Longrightarrow> Liminf (filtermap f F) g = Liminf F (\<lambda>x. g (f x))"
       
   548   using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g]
       
   549   by simp
       
   550 
       
   551 lemma Limsup_filtermap_eq: "inj f \<Longrightarrow> Limsup (filtermap f F) g = Limsup F (\<lambda>x. g (f x))"
       
   552   using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f]
       
   553   by simp
       
   554 
   508 
   555 
   509 subsection \<open>More Limits\<close>
   556 subsection \<open>More Limits\<close>
   510 
   557 
   511 lemma convergent_limsup_cl:
   558 lemma convergent_limsup_cl:
   512   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   559   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"