summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Liminf_Limsup.thy

changeset 61245 | b77bf45efe21 |

parent 60500 | 903bb1495239 |

child 61585 | a9599d3d7610 |

--- a/src/HOL/Library/Liminf_Limsup.thy Thu Sep 24 15:21:12 2015 +0200 +++ b/src/HOL/Library/Liminf_Limsup.thy Fri Sep 25 16:54:31 2015 +0200 @@ -150,6 +150,17 @@ shows "Limsup F X \<le> C" using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp +lemma le_Limsup: + assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x" + shows "l \<le> Limsup F f" +proof - + have "l = Limsup F (\<lambda>x. l)" + using F by (simp add: Limsup_const) + also have "\<dots> \<le> Limsup F f" + by (intro Limsup_mono x) + finally show ?thesis . +qed + lemma le_Liminf_iff: fixes X :: "_ \<Rightarrow> _ :: complete_linorder" shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)" @@ -308,4 +319,33 @@ then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def) qed +lemma continuous_on_imp_continuous_within: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f" + unfolding continuous_on_eq_continuous_within by (auto simp: continuous_within intro: tendsto_within_subset) + +lemma Liminf_compose_continuous_antimono: + fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}" + assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot" + shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)" +proof - + { fix P assume "eventually P F" + have "\<exists>x. P x" + proof (rule ccontr) + assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" + by auto + with \<open>eventually P F\<close> F show False + by auto + qed } + note * = this + + have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" + unfolding Limsup_def INF_def + by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) + (auto intro: eventually_True) + also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" + by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) + (auto dest!: eventually_happens simp: F) + finally show ?thesis + by (auto simp: Liminf_def) +qed + end