src/HOL/Library/Liminf_Limsup.thy
 changeset 66447 a1f5c5c26fa6 parent 63895 9afa979137da child 68860 f443ec10447d
equal inserted replaced
66445:407de0768126 66447:a1f5c5c26fa6
`   377   shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"`
`   377   shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"`
`   378   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)`
`   378   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)`
`   379 `
`   379 `
`   380 lemma liminf_subseq_mono:`
`   380 lemma liminf_subseq_mono:`
`   381   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"`
`   381   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"`
`   382   assumes "subseq r"`
`   382   assumes "strict_mono r"`
`   383   shows "liminf X \<le> liminf (X \<circ> r) "`
`   383   shows "liminf X \<le> liminf (X \<circ> r) "`
`   384 proof-`
`   384 proof-`
`   385   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"`
`   385   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"`
`   386   proof (safe intro!: INF_mono)`
`   386   proof (safe intro!: INF_mono)`
`   387     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"`
`   387     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"`
`   388       using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto`
`   388       using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto`
`   389   qed`
`   389   qed`
`   390   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)`
`   390   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)`
`   391 qed`
`   391 qed`
`   392 `
`   392 `
`   393 lemma limsup_subseq_mono:`
`   393 lemma limsup_subseq_mono:`
`   394   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"`
`   394   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"`
`   395   assumes "subseq r"`
`   395   assumes "strict_mono r"`
`   396   shows "limsup (X \<circ> r) \<le> limsup X"`
`   396   shows "limsup (X \<circ> r) \<le> limsup X"`
`   397 proof-`
`   397 proof-`
`   398   have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n`
`   398   have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n`
`   399   proof (safe intro!: SUP_mono)`
`   399   proof (safe intro!: SUP_mono)`
`   400     fix m :: nat`
`   400     fix m :: nat`
`   401     assume "n \<le> m"`
`   401     assume "n \<le> m"`
`   402     then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"`
`   402     then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"`
`   403       using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto`
`   403       using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto`
`   404   qed`
`   404   qed`
`   405   then show ?thesis`
`   405   then show ?thesis`
`   406     by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)`
`   406     by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)`
`   407 qed`
`   407 qed`
`   408 `
`   408 `
`   585        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)`
`   585        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)`
`   586 qed`
`   586 qed`
`   587 `
`   587 `
`   588 lemma compact_complete_linorder:`
`   588 lemma compact_complete_linorder:`
`   589   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"`
`   589   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"`
`   590   shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"`
`   590   shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"`
`   591 proof -`
`   591 proof -`
`   592   obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"`
`   592   obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"`
`   593     using seq_monosub[of X]`
`   593     using seq_monosub[of X]`
`   594     unfolding comp_def`
`   594     unfolding comp_def`
`   595     by auto`
`   595     by auto`
`   596   then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"`
`   596   then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"`
`   597     by (auto simp add: monoseq_def)`
`   597     by (auto simp add: monoseq_def)`
`   598   then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"`
`   598   then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"`
`   599      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]`
`   599      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]`
`   600      by auto`
`   600      by auto`
`   601   then show ?thesis`
`   601   then show ?thesis`
`   602     using \<open>subseq r\<close> by auto`
`   602     using \<open>strict_mono r\<close> by auto`
`   603 qed`
`   603 qed`
`   604 `
`   604 `
`   605 lemma tendsto_Limsup:`
`   605 lemma tendsto_Limsup:`
`   606   fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"`
`   606   fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"`
`   607   shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F"`
`   607   shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F"`