src/HOL/Library/Liminf_Limsup.thy
 changeset 63895 9afa979137da parent 62975 1d066f6ab25d child 66447 a1f5c5c26fa6
equal 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:`
`   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:`
`   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}"`