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

src/HOL/Library/Liminf_Limsup.thy

changeset 56218 | 1c3f1f2431f9 |

parent 56212 | 3253aaf73a01 |

child 58881 | b9556a055632 |

--- a/src/HOL/Library/Liminf_Limsup.thy Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Library/Liminf_Limsup.thy Wed Mar 19 18:47:22 2014 +0100 @@ -43,13 +43,13 @@ abbreviation "limsup \<equiv> Limsup sequentially" lemma Liminf_eqI: - "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow> - (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x" + "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow> + (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x" unfolding Liminf_def by (auto intro!: SUP_eqI) lemma Limsup_eqI: - "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow> - (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x" + "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow> + (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x" unfolding Limsup_def by (auto intro!: INF_eqI) lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)" @@ -93,7 +93,7 @@ proof (safe intro!: SUP_mono) fix P assume "eventually P F" with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) - then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g" + then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g" by (intro bexI[of _ ?Q]) (auto intro!: INF_mono) qed @@ -109,7 +109,7 @@ proof (safe intro!: INF_mono) fix P assume "eventually P F" with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) - then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g" + then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g" by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono) qed @@ -129,13 +129,13 @@ then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj) then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)" using ntriv by (auto simp add: eventually_False) - have "INFI (Collect P) f \<le> INFI (Collect ?C) f" + have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f" by (rule INF_mono) auto - also have "\<dots> \<le> SUPR (Collect ?C) f" + also have "\<dots> \<le> SUPREMUM (Collect ?C) f" using not_False by (intro INF_le_SUP) auto - also have "\<dots> \<le> SUPR (Collect Q) f" + also have "\<dots> \<le> SUPREMUM (Collect Q) f" by (rule SUP_mono) auto - finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" . + finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" . qed lemma Liminf_bounded: @@ -154,22 +154,22 @@ fixes X :: "_ \<Rightarrow> _ :: complete_linorder" shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)" proof - - { fix y P assume "eventually P F" "y < INFI (Collect P) X" + { fix y P assume "eventually P F" "y < INFIMUM (Collect P) X" then have "eventually (\<lambda>x. y < X x) F" by (auto elim!: eventually_elim1 dest: less_INF_D) } moreover { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" - have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X" + have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X" proof (cases "\<exists>z. y < z \<and> z < C") case True then obtain z where z: "y < z \<and> z < C" .. - moreover from z have "z \<le> INFI {x. z < X x} X" + moreover from z have "z \<le> INFIMUM {x. z < X x} X" by (auto intro!: INF_greatest) ultimately show ?thesis using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto next case False - then have "C \<le> INFI {x. y < X x} X" + then have "C \<le> INFIMUM {x. y < X x} X" by (intro INF_greatest) auto with `y < C` show ?thesis using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto @@ -185,17 +185,17 @@ shows "Liminf F f = f0" proof (intro Liminf_eqI) fix P assume P: "eventually P F" - then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F" + then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F" by eventually_elim (auto intro!: INF_lower) - then show "INFI (Collect P) f \<le> f0" + then show "INFIMUM (Collect P) f \<le> f0" by (rule tendsto_le[OF ntriv lim tendsto_const]) next - fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y" + fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y" show "f0 \<le> y" proof cases assume "\<exists>z. y < z \<and> z < f0" then obtain z where "y < z \<and> z < f0" .. - moreover have "z \<le> INFI {x. z < f x} f" + moreover have "z \<le> INFIMUM {x. z < f x} f" by (rule INF_greatest) simp ultimately show ?thesis using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto @@ -208,9 +208,9 @@ using lim[THEN topological_tendstoD, of "{y <..}"] by auto then have "eventually (\<lambda>x. f0 \<le> f x) F" using discrete by (auto elim!: eventually_elim1) - then have "INFI {x. f0 \<le> f x} f \<le> y" + then have "INFIMUM {x. f0 \<le> f x} f \<le> y" by (rule upper) - moreover have "f0 \<le> INFI {x. f0 \<le> f x} f" + moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f" by (intro INF_greatest) simp ultimately show "f0 \<le> y" by simp qed @@ -224,17 +224,17 @@ shows "Limsup F f = f0" proof (intro Limsup_eqI) fix P assume P: "eventually P F" - then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F" + then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F" by eventually_elim (auto intro!: SUP_upper) - then show "f0 \<le> SUPR (Collect P) f" + then show "f0 \<le> SUPREMUM (Collect P) f" by (rule tendsto_le[OF ntriv tendsto_const lim]) next - fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f" + fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f" show "y \<le> f0" proof (cases "\<exists>z. f0 < z \<and> z < y") case True then obtain z where "f0 < z \<and> z < y" .. - moreover have "SUPR {x. f x < z} f \<le> z" + moreover have "SUPREMUM {x. f x < z} f \<le> z" by (rule SUP_least) simp ultimately show ?thesis using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto @@ -247,9 +247,9 @@ using lim[THEN topological_tendstoD, of "{..< y}"] by auto then have "eventually (\<lambda>x. f x \<le> f0) F" using False by (auto elim!: eventually_elim1 simp: not_less) - then have "y \<le> SUPR {x. f x \<le> f0} f" + then have "y \<le> SUPREMUM {x. f x \<le> f0} f" by (rule lower) - moreover have "SUPR {x. f x \<le> f0} f \<le> f0" + moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0" by (intro SUP_least) simp ultimately show "y \<le> f0" by simp qed @@ -264,14 +264,14 @@ proof (rule order_tendstoI) fix a assume "f0 < a" with assms have "Limsup F f < a" by simp - then obtain P where "eventually P F" "SUPR (Collect P) f < a" + then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a" unfolding Limsup_def INF_less_iff by auto then show "eventually (\<lambda>x. f x < a) F" by (auto elim!: eventually_elim1 dest: SUP_lessD) next fix a assume "a < f0" with assms have "a < Liminf F f" by simp - then obtain P where "eventually P F" "a < INFI (Collect P) f" + then obtain P where "eventually P F" "a < INFIMUM (Collect P) f" unfolding Liminf_def less_SUP_iff by auto then show "eventually (\<lambda>x. a < f x) F" by (auto elim!: eventually_elim1 dest: less_INF_D)