--- a/src/HOL/Library/Extended_Real.thy Tue Mar 05 15:27:08 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Mar 05 15:43:08 2013 +0100
@@ -8,7 +8,7 @@
header {* Extended real number line *}
theory Extended_Real
-imports Complex_Main Extended_Nat
+imports Complex_Main Extended_Nat Liminf_Limsup
begin
text {*
@@ -18,26 +18,6 @@
*}
-lemma SUPR_pair:
- "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
- by (rule antisym) (auto intro!: SUP_least SUP_upper2)
-
-lemma INFI_pair:
- "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
- by (rule antisym) (auto intro!: INF_greatest INF_lower2)
-
-lemma le_Sup_iff_less:
- fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
- shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
- unfolding le_SUP_iff
- by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
-
-lemma Inf_le_iff_less:
- fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
- shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
- unfolding INF_le_iff
- by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
-
subsection {* Definition and basic properties *}
datatype ereal = ereal real | PInfty | MInfty
@@ -1718,6 +1698,31 @@
show thesis by auto
qed
+instance ereal :: perfect_space
+proof (default, rule)
+ fix a :: ereal assume a: "open {a}"
+ show False
+ proof (cases a)
+ case MInf
+ then obtain y where "{..<ereal y} \<le> {a}" using a open_MInfty2[of "{a}"] by auto
+ then have "ereal (y - 1) \<in> {a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
+ then show False using `a = -\<infinity>` by auto
+ next
+ case PInf
+ then obtain y where "{ereal y<..} \<le> {a}" using a open_PInfty2[of "{a}"] by auto
+ then have "ereal (y + 1) \<in> {a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
+ then show False using `a = \<infinity>` by auto
+ next
+ case (real r)
+ then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
+ from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
+ then obtain b where b_def: "a<b \<and> b<a+e"
+ using fin ereal_between dense[of a "a+e"] by auto
+ then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
+ then show False using b_def e by auto
+ qed
+qed
+
subsubsection {* Convergent sequences *}
lemma lim_ereal[simp]:
@@ -1981,123 +1986,15 @@
using ereal_LimI_finite[of x] assms by auto
qed
-
-subsubsection {* @{text Liminf} and @{text Limsup} *}
-
-definition
- "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
-
-definition
- "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
-
-abbreviation "liminf \<equiv> Liminf sequentially"
-
-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"
- 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"
- unfolding Limsup_def by (auto intro!: INF_eqI)
-
-lemma liminf_SUPR_INFI:
- fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
- shows "liminf f = (SUP n. INF m:{n..}. f m)"
- unfolding Liminf_def eventually_sequentially
- by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
-
-lemma limsup_INFI_SUPR:
- fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
- shows "limsup f = (INF n. SUP m:{n..}. f m)"
- unfolding Limsup_def eventually_sequentially
- by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
-
-lemma Limsup_const:
- assumes ntriv: "\<not> trivial_limit F"
- shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
-proof -
- have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
- have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
- using ntriv by (intro SUP_const) (auto simp: eventually_False *)
- then show ?thesis
- unfolding Limsup_def using eventually_True
- by (subst INF_cong[where D="\<lambda>x. c"])
- (auto intro!: INF_const simp del: eventually_True)
-qed
+lemma ereal_Limsup_uminus:
+ fixes f :: "'a => ereal"
+ shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
+ unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
-lemma Liminf_const:
- assumes ntriv: "\<not> trivial_limit F"
- shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
-proof -
- have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
- have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
- using ntriv by (intro INF_const) (auto simp: eventually_False *)
- then show ?thesis
- unfolding Liminf_def using eventually_True
- by (subst SUP_cong[where D="\<lambda>x. c"])
- (auto intro!: SUP_const simp del: eventually_True)
-qed
-
-lemma Liminf_mono:
- fixes f g :: "'a => 'b :: complete_lattice"
- assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
- shows "Liminf F f \<le> Liminf F g"
- unfolding Liminf_def
-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"
- by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
-qed
-
-lemma Liminf_eq:
- fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
- assumes "eventually (\<lambda>x. f x = g x) F"
- shows "Liminf F f = Liminf F g"
- by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
-
-lemma Limsup_mono:
- fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
- assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
- shows "Limsup F f \<le> Limsup F g"
- unfolding Limsup_def
-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"
- by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
-qed
-
-lemma Limsup_eq:
- fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
- assumes "eventually (\<lambda>x. f x = g x) net"
- shows "Limsup net f = Limsup net g"
- by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
-
-lemma Liminf_le_Limsup:
- fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
- assumes ntriv: "\<not> trivial_limit F"
- shows "Liminf F f \<le> Limsup F f"
- unfolding Limsup_def Liminf_def
- apply (rule complete_lattice_class.SUP_least)
- apply (rule complete_lattice_class.INF_greatest)
-proof safe
- fix P Q assume "eventually P F" "eventually Q F"
- 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"
- by (rule INF_mono) auto
- also have "\<dots> \<le> SUPR (Collect ?C) f"
- using not_False by (intro INF_le_SUP) auto
- also have "\<dots> \<le> SUPR (Collect Q) f"
- by (rule SUP_mono) auto
- finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
-qed
+lemma liminf_bounded_iff:
+ fixes x :: "nat \<Rightarrow> ereal"
+ shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
+ unfolding le_Liminf_iff eventually_sequentially ..
lemma
fixes X :: "nat \<Rightarrow> ereal"
@@ -2105,220 +2002,6 @@
and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
unfolding incseq_def decseq_def by auto
-lemma Liminf_bounded:
- fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
- assumes ntriv: "\<not> trivial_limit F"
- assumes le: "eventually (\<lambda>n. C \<le> X n) F"
- shows "C \<le> Liminf F X"
- using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
-
-lemma Limsup_bounded:
- fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
- assumes ntriv: "\<not> trivial_limit F"
- assumes le: "eventually (\<lambda>n. X n \<le> C) F"
- shows "Limsup F X \<le> C"
- using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
-
-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)"
-proof -
- { fix y P assume "eventually P F" "y < INFI (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"
- proof cases
- assume "\<exists>z. y < z \<and> z < C"
- then guess z ..
- moreover then have "z \<le> INFI {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
- assume "\<not> (\<exists>z. y < z \<and> z < C)"
- then have "C \<le> INFI {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
- qed }
- ultimately show ?thesis
- unfolding Liminf_def le_SUP_iff by auto
-qed
-
-lemma lim_imp_Liminf:
- fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
- assumes ntriv: "\<not> trivial_limit F"
- assumes lim: "(f ---> f0) F"
- 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"
- by eventually_elim (auto intro!: INF_lower)
- then show "INFI (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"
- show "f0 \<le> y"
- proof cases
- assume "\<exists>z. y < z \<and> z < f0"
- then guess z ..
- moreover have "z \<le> INFI {x. z < f x} f"
- by (rule INF_greatest) simp
- ultimately show ?thesis
- using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
- next
- assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
- show ?thesis
- proof (rule classical)
- assume "\<not> f0 \<le> y"
- then have "eventually (\<lambda>x. y < f x) F"
- 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"
- by (rule upper)
- moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
- by (intro INF_greatest) simp
- ultimately show "f0 \<le> y" by simp
- qed
- qed
-qed
-
-lemma lim_imp_Limsup:
- fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
- assumes ntriv: "\<not> trivial_limit F"
- assumes lim: "(f ---> f0) F"
- 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"
- by eventually_elim (auto intro!: SUP_upper)
- then show "f0 \<le> SUPR (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"
- show "y \<le> f0"
- proof cases
- assume "\<exists>z. f0 < z \<and> z < y"
- then guess z ..
- moreover have "SUPR {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
- next
- assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
- show ?thesis
- proof (rule classical)
- assume "\<not> y \<le> f0"
- then have "eventually (\<lambda>x. f x < y) F"
- using lim[THEN topological_tendstoD, of "{..< y}"] by auto
- then have "eventually (\<lambda>x. f x \<le> f0) F"
- using discrete by (auto elim!: eventually_elim1 simp: not_less)
- then have "y \<le> SUPR {x. f x \<le> f0} f"
- by (rule lower)
- moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
- by (intro SUP_least) simp
- ultimately show "y \<le> f0" by simp
- qed
- qed
-qed
-
-lemma Liminf_eq_Limsup:
- fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
- assumes ntriv: "\<not> trivial_limit F"
- and lim: "Liminf F f = f0" "Limsup F f = f0"
- shows "(f ---> f0) F"
-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"
- 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"
- 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)
-qed
-
-lemma tendsto_iff_Liminf_eq_Limsup:
- fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
- shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
- by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
-
-lemma liminf_bounded_iff:
- fixes x :: "nat \<Rightarrow> ereal"
- shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
- unfolding le_Liminf_iff eventually_sequentially ..
-
-lemma liminf_subseq_mono:
- fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
- assumes "subseq r"
- shows "liminf X \<le> liminf (X \<circ> r) "
-proof-
- have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
- proof (safe intro!: INF_mono)
- fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
- using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
- qed
- then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
-qed
-
-lemma limsup_subseq_mono:
- fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
- assumes "subseq r"
- shows "limsup (X \<circ> r) \<le> limsup X"
-proof-
- have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
- proof (safe intro!: SUP_mono)
- fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
- using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
- qed
- then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
-qed
-
-definition (in order) mono_set:
- "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
-
-lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
-lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
-lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
-lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
-
-lemma (in complete_linorder) mono_set_iff:
- fixes S :: "'a set"
- defines "a \<equiv> Inf S"
- shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
-proof
- assume "mono_set S"
- then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
- show ?c
- proof cases
- assume "a \<in> S"
- show ?c
- using mono[OF _ `a \<in> S`]
- by (auto intro: Inf_lower simp: a_def)
- next
- assume "a \<notin> S"
- have "S = {a <..}"
- proof safe
- fix x assume "x \<in> S"
- then have "a \<le> x" unfolding a_def by (rule Inf_lower)
- then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
- next
- fix x assume "a < x"
- then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
- with mono[of y x] show "x \<in> S" by auto
- qed
- then show ?c ..
- qed
-qed auto
-
subsubsection {* Tests for code generator *}
(* A small list of simple arithmetic expressions *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Liminf_Limsup.thy Tue Mar 05 15:43:08 2013 +0100
@@ -0,0 +1,320 @@
+(* Title: HOL/Library/Liminf_Limsup.thy
+ Author: Johannes Hölzl, TU München
+*)
+
+header {* Liminf and Limsup on complete lattices *}
+
+theory Liminf_Limsup
+imports "~~/src/HOL/Complex_Main"
+begin
+
+lemma le_Sup_iff_less:
+ fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
+ unfolding le_SUP_iff
+ by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
+
+lemma Inf_le_iff_less:
+ fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+ unfolding INF_le_iff
+ by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
+
+lemma SUPR_pair:
+ "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
+ by (rule antisym) (auto intro!: SUP_least SUP_upper2)
+
+lemma INFI_pair:
+ "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
+ by (rule antisym) (auto intro!: INF_greatest INF_lower2)
+
+subsubsection {* @{text Liminf} and @{text Limsup} *}
+
+definition
+ "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
+
+definition
+ "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
+
+abbreviation "liminf \<equiv> Liminf sequentially"
+
+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"
+ 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"
+ unfolding Limsup_def by (auto intro!: INF_eqI)
+
+lemma liminf_SUPR_INFI:
+ fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+ shows "liminf f = (SUP n. INF m:{n..}. f m)"
+ unfolding Liminf_def eventually_sequentially
+ by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
+
+lemma limsup_INFI_SUPR:
+ fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+ shows "limsup f = (INF n. SUP m:{n..}. f m)"
+ unfolding Limsup_def eventually_sequentially
+ by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
+
+lemma Limsup_const:
+ assumes ntriv: "\<not> trivial_limit F"
+ shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+ have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+ have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
+ using ntriv by (intro SUP_const) (auto simp: eventually_False *)
+ then show ?thesis
+ unfolding Limsup_def using eventually_True
+ by (subst INF_cong[where D="\<lambda>x. c"])
+ (auto intro!: INF_const simp del: eventually_True)
+qed
+
+lemma Liminf_const:
+ assumes ntriv: "\<not> trivial_limit F"
+ shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+ have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+ have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
+ using ntriv by (intro INF_const) (auto simp: eventually_False *)
+ then show ?thesis
+ unfolding Liminf_def using eventually_True
+ by (subst SUP_cong[where D="\<lambda>x. c"])
+ (auto intro!: SUP_const simp del: eventually_True)
+qed
+
+lemma Liminf_mono:
+ fixes f g :: "'a => 'b :: complete_lattice"
+ assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+ shows "Liminf F f \<le> Liminf F g"
+ unfolding Liminf_def
+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"
+ by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
+qed
+
+lemma Liminf_eq:
+ fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+ assumes "eventually (\<lambda>x. f x = g x) F"
+ shows "Liminf F f = Liminf F g"
+ by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
+
+lemma Limsup_mono:
+ fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+ assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+ shows "Limsup F f \<le> Limsup F g"
+ unfolding Limsup_def
+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"
+ by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
+qed
+
+lemma Limsup_eq:
+ fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+ assumes "eventually (\<lambda>x. f x = g x) net"
+ shows "Limsup net f = Limsup net g"
+ by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
+
+lemma Liminf_le_Limsup:
+ fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
+ assumes ntriv: "\<not> trivial_limit F"
+ shows "Liminf F f \<le> Limsup F f"
+ unfolding Limsup_def Liminf_def
+ apply (rule complete_lattice_class.SUP_least)
+ apply (rule complete_lattice_class.INF_greatest)
+proof safe
+ fix P Q assume "eventually P F" "eventually Q F"
+ 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"
+ by (rule INF_mono) auto
+ also have "\<dots> \<le> SUPR (Collect ?C) f"
+ using not_False by (intro INF_le_SUP) auto
+ also have "\<dots> \<le> SUPR (Collect Q) f"
+ by (rule SUP_mono) auto
+ finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
+qed
+
+lemma Liminf_bounded:
+ fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes le: "eventually (\<lambda>n. C \<le> X n) F"
+ shows "C \<le> Liminf F X"
+ using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
+
+lemma Limsup_bounded:
+ fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes le: "eventually (\<lambda>n. X n \<le> C) F"
+ shows "Limsup F X \<le> C"
+ using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+
+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)"
+proof -
+ { fix y P assume "eventually P F" "y < INFI (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"
+ proof cases
+ assume "\<exists>z. y < z \<and> z < C"
+ then guess z ..
+ moreover then have "z \<le> INFI {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
+ assume "\<not> (\<exists>z. y < z \<and> z < C)"
+ then have "C \<le> INFI {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
+ qed }
+ ultimately show ?thesis
+ unfolding Liminf_def le_SUP_iff by auto
+qed
+
+lemma lim_imp_Liminf:
+ fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ 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"
+ by eventually_elim (auto intro!: INF_lower)
+ then show "INFI (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"
+ show "f0 \<le> y"
+ proof cases
+ assume "\<exists>z. y < z \<and> z < f0"
+ then guess z ..
+ moreover have "z \<le> INFI {x. z < f x} f"
+ by (rule INF_greatest) simp
+ ultimately show ?thesis
+ using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
+ next
+ assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
+ show ?thesis
+ proof (rule classical)
+ assume "\<not> f0 \<le> y"
+ then have "eventually (\<lambda>x. y < f x) F"
+ 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"
+ by (rule upper)
+ moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
+ by (intro INF_greatest) simp
+ ultimately show "f0 \<le> y" by simp
+ qed
+ qed
+qed
+
+lemma lim_imp_Limsup:
+ fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ 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"
+ by eventually_elim (auto intro!: SUP_upper)
+ then show "f0 \<le> SUPR (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"
+ show "y \<le> f0"
+ proof cases
+ assume "\<exists>z. f0 < z \<and> z < y"
+ then guess z ..
+ moreover have "SUPR {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
+ next
+ assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+ show ?thesis
+ proof (rule classical)
+ assume "\<not> y \<le> f0"
+ then have "eventually (\<lambda>x. f x < y) F"
+ using lim[THEN topological_tendstoD, of "{..< y}"] by auto
+ then have "eventually (\<lambda>x. f x \<le> f0) F"
+ using discrete by (auto elim!: eventually_elim1 simp: not_less)
+ then have "y \<le> SUPR {x. f x \<le> f0} f"
+ by (rule lower)
+ moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
+ by (intro SUP_least) simp
+ ultimately show "y \<le> f0" by simp
+ qed
+ qed
+qed
+
+lemma Liminf_eq_Limsup:
+ fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ and lim: "Liminf F f = f0" "Limsup F f = f0"
+ shows "(f ---> f0) F"
+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"
+ 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"
+ 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)
+qed
+
+lemma tendsto_iff_Liminf_eq_Limsup:
+ fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+ shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
+ by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
+
+lemma liminf_subseq_mono:
+ fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+ assumes "subseq r"
+ shows "liminf X \<le> liminf (X \<circ> r) "
+proof-
+ have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
+ proof (safe intro!: INF_mono)
+ fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
+ using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+ qed
+ then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
+qed
+
+lemma limsup_subseq_mono:
+ fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+ assumes "subseq r"
+ shows "limsup (X \<circ> r) \<le> limsup X"
+proof-
+ have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
+ proof (safe intro!: SUP_mono)
+ fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
+ using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+ qed
+ then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
+qed
+
+end
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Mar 05 15:27:08 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Mar 05 15:43:08 2013 +0100
@@ -22,35 +22,13 @@
lemma ereal_open_uminus:
fixes S :: "ereal set"
- assumes "open S"
- shows "open (uminus ` S)"
- unfolding open_ereal_def
-proof (intro conjI impI)
- obtain x y where
- S: "open (ereal -` S)" "\<infinity> \<in> S \<Longrightarrow> {ereal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< ereal y} \<subseteq> S"
- using `open S` unfolding open_ereal_def by auto
- have "ereal -` uminus ` S = uminus ` (ereal -` S)"
- proof safe
- fix x y
- assume "ereal x = - y" "y \<in> S"
- then show "x \<in> uminus ` ereal -` S" by (cases y) auto
- next
- fix x
- assume "ereal x \<in> S"
- then show "- x \<in> ereal -` uminus ` S"
- by (auto intro: image_eqI[of _ _ "ereal x"])
- qed
- then show "open (ereal -` uminus ` S)"
- using S by (auto intro: open_negations)
- { assume "\<infinity> \<in> uminus ` S"
- then have "-\<infinity> \<in> S" by (metis image_iff ereal_uminus_uminus)
- then have "uminus ` {..<ereal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto
- then show "\<exists>x. {ereal x<..} \<subseteq> uminus ` S" using ereal_uminus_lessThan by auto }
- { assume "-\<infinity> \<in> uminus ` S"
- then have "\<infinity> : S" by (metis image_iff ereal_uminus_uminus)
- then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto
- then show "\<exists>y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto }
-qed
+ assumes "open S" shows "open (uminus ` S)"
+ using `open S`[unfolded open_generated_order]
+proof induct
+ have "range uminus = (UNIV :: ereal set)"
+ by (auto simp: image_iff ereal_uminus_eq_reorder)
+ then show "open (range uminus :: ereal set)" by simp
+qed (auto simp add: image_Union image_Int)
lemma ereal_uminus_complement:
fixes S :: "ereal set"
@@ -61,32 +39,7 @@
fixes S :: "ereal set"
assumes "closed S"
shows "closed (uminus ` S)"
- using assms unfolding closed_def
- using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
-
-instance ereal :: perfect_space
-proof (default, rule)
- fix a :: ereal assume a: "open {a}"
- show False
- proof (cases a)
- case MInf
- then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
- then have "ereal(y - 1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
- then show False using `a=(-\<infinity>)` by auto
- next
- case PInf
- then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
- then have "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
- then show False using `a=\<infinity>` by auto
- next
- case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
- from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
- then obtain b where b_def: "a<b & b<a+e"
- using fin ereal_between dense[of a "a+e"] by auto
- then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
- then show False using b_def e by auto
- qed
-qed
+ using assms unfolding closed_def ereal_uminus_complement[symmetric] by (rule ereal_open_uminus)
lemma ereal_closed_contains_Inf:
fixes S :: "ereal set"
@@ -303,113 +256,9 @@
then show "x = -\<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
qed
-lemma ereal_open_mono_set:
- fixes S :: "ereal set"
- shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
- by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
- ereal_open_closed mono_set_iff open_ereal_greaterThan)
-
-lemma ereal_closed_mono_set:
- fixes S :: "ereal set"
- shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
- by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
- ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
-
-lemma ereal_Liminf_Sup_monoset:
- fixes f :: "'a => ereal"
- shows "Liminf net f =
- Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
- (is "_ = Sup ?A")
-proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
- fix P assume P: "eventually P net"
- fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
- { fix x assume "P x"
- then have "INFI (Collect P) f \<le> f x"
- by (intro complete_lattice_class.INF_lower) simp
- with S have "f x \<in> S"
- by (simp add: mono_set) }
- with P show "eventually (\<lambda>x. f x \<in> S) net"
- by (auto elim: eventually_elim1)
-next
- fix y l
- assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
- assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
- show "l \<le> y"
- proof (rule dense_le)
- fix B assume "B < l"
- then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
- by (intro S[rule_format]) auto
- then have "INFI {x. B < f x} f \<le> y"
- using P by auto
- moreover have "B \<le> INFI {x. B < f x} f"
- by (intro INF_greatest) auto
- ultimately show "B \<le> y"
- by simp
- qed
-qed
-
-lemma ereal_Limsup_Inf_monoset:
- fixes f :: "'a => ereal"
- shows "Limsup net f =
- Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
- (is "_ = Inf ?A")
-proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
- fix P assume P: "eventually P net"
- fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
- { fix x assume "P x"
- then have "f x \<le> SUPR (Collect P) f"
- by (intro complete_lattice_class.SUP_upper) simp
- with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
- have "f x \<in> S"
- by (simp add: inj_image_mem_iff) }
- with P show "eventually (\<lambda>x. f x \<in> S) net"
- by (auto elim: eventually_elim1)
-next
- fix y l
- assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
- assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
- show "y \<le> l"
- proof (rule dense_ge)
- fix B assume "l < B"
- then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
- by (intro S[rule_format]) auto
- then have "y \<le> SUPR {x. f x < B} f"
- using P by auto
- moreover have "SUPR {x. f x < B} f \<le> B"
- by (intro SUP_least) auto
- ultimately show "y \<le> B"
- by simp
- qed
-qed
-
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
-lemma ereal_Limsup_uminus:
- fixes f :: "'a => ereal"
- shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
-proof -
- { fix P l
- have "(\<exists>x. (l::ereal) = -x \<and> P x) \<longleftrightarrow> P (-l)"
- by (auto intro!: exI[of _ "-l"]) }
- note Ex_cancel = this
- { fix P :: "ereal set \<Rightarrow> bool"
- have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
- apply auto
- apply (erule_tac x="uminus`S" in allE)
- apply (auto simp: image_image)
- done }
- note add_uminus_image = this
- { fix x S
- have "(x::ereal) \<in> uminus`S \<longleftrightarrow> -x\<in>S"
- by (auto intro!: image_eqI[of _ _ "-x"]) }
- note remove_uminus_image = this
- show ?thesis
- unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset
- unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
- by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
-qed
-
lemma ereal_Liminf_uminus:
fixes f :: "'a => ereal"
shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
@@ -423,14 +272,6 @@
ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
by (auto simp: ereal_uminus_reorder)
-lemma lim_imp_Limsup:
- fixes f :: "'a => ereal"
- assumes "\<not> trivial_limit net"
- and lim: "(f ---> f0) net"
- shows "Limsup net f = f0"
- using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
- ereal_Liminf_uminus[of net f] assms by simp
-
lemma convergent_ereal_limsup:
fixes X :: "nat \<Rightarrow> ereal"
shows "convergent X \<Longrightarrow> limsup X = lim X"
@@ -461,43 +302,10 @@
using assms ereal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)
-lemma ereal_Liminf_eq_Limsup:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes ntriv: "\<not> trivial_limit net"
- and lim: "Liminf net f = f0" "Limsup net f = f0"
- shows "(f ---> f0) net"
-proof (cases f0)
- case PInf
- then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
-next
- case MInf
- then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
-next
- case (real r)
- show "(f ---> f0) net"
- proof (rule topological_tendstoI)
- fix S
- assume "open S" "f0 \<in> S"
- then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
- using ereal_open_cont_interval2[of S f0] real lim by auto
- then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
- unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
- by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
- with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
- by (rule_tac eventually_mono) auto
- qed
-qed
-
-lemma ereal_Liminf_eq_Limsup_iff:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes "\<not> trivial_limit net"
- shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
- by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
-
lemma convergent_ereal:
fixes X :: "nat \<Rightarrow> ereal"
shows "convergent X \<longleftrightarrow> limsup X = liminf X"
- using ereal_Liminf_eq_Limsup_iff[of sequentially]
+ using tendsto_iff_Liminf_eq_Limsup[of sequentially]
by (auto simp: convergent_def)
lemma limsup_INFI_SUPR:
@@ -535,45 +343,6 @@
shows "X N >= L"
using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
-lemma liminf_bounded_open:
- fixes x :: "nat \<Rightarrow> ereal"
- shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
- (is "_ \<longleftrightarrow> ?P x0")
-proof
- assume "?P x0"
- then show "x0 \<le> liminf x"
- unfolding ereal_Liminf_Sup_monoset eventually_sequentially
- by (intro complete_lattice_class.Sup_upper) auto
-next
- assume "x0 \<le> liminf x"
- { fix S :: "ereal set"
- assume om: "open S & mono_set S & x0:S"
- { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
- moreover
- { assume "~(S=UNIV)"
- then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
- then have "B<x0" using om by auto
- then have "EX N. ALL n>=N. x n : S"
- unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
- }
- ultimately have "EX N. (ALL n>=N. x n : S)" by auto
- }
- then show "?P x0" by auto
-qed
-
-lemma limsup_subseq_mono:
- fixes X :: "nat \<Rightarrow> ereal"
- assumes "subseq r"
- shows "limsup (X \<circ> r) \<le> limsup X"
-proof -
- have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
- then have "- limsup X \<le> - limsup (X \<circ> r)"
- using liminf_subseq_mono[of r "(%n. - X n)"]
- ereal_Liminf_uminus[of sequentially X]
- ereal_Liminf_uminus[of sequentially "X o r"] assms by auto
- then show ?thesis by auto
-qed
-
lemma bounded_abs:
assumes "(a::real)<=x" "x<=b"
shows "abs x <= max (abs a) (abs b)"
@@ -652,85 +421,6 @@
show "f ----> x" by auto }
qed
-lemma Liminf_within:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
- shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
- unfolding Liminf_def eventually_within
-proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
- fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
- then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
- by (auto simp: zero_less_dist_iff dist_commute)
- then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
- by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
-next
- fix d :: real assume "0 < d"
- then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
- INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
- by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
- (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
-qed
-
-lemma Limsup_within:
- fixes f :: "'a::metric_space => 'b::complete_lattice"
- shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
- unfolding Limsup_def eventually_within
-proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
- fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
- then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
- by (auto simp: zero_less_dist_iff dist_commute)
- then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
- by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
-next
- fix d :: real assume "0 < d"
- then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
- SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
- by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
- (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
-qed
-
-lemma Liminf_within_UNIV:
- fixes f :: "'a::metric_space => _"
- shows "Liminf (at x) f = Liminf (at x within UNIV) f"
- by simp (* TODO: delete *)
-
-
-lemma Liminf_at:
- fixes f :: "'a::metric_space => _"
- shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
- using Liminf_within[of x UNIV f] by simp
-
-
-lemma Limsup_within_UNIV:
- fixes f :: "'a::metric_space => _"
- shows "Limsup (at x) f = Limsup (at x within UNIV) f"
- by simp (* TODO: delete *)
-
-
-lemma Limsup_at:
- fixes f :: "'a::metric_space => _"
- shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
- using Limsup_within[of x UNIV f] by simp
-
-lemma Lim_within_constant:
- assumes "ALL y:S. f y = C"
- shows "(f ---> C) (at x within S)"
- unfolding tendsto_def Limits.eventually_within eventually_at_topological
- using assms by simp (metis open_UNIV UNIV_I)
-
-lemma Liminf_within_constant:
- fixes f :: "'a::topological_space \<Rightarrow> ereal"
- assumes "ALL y:S. f y = C"
- and "~trivial_limit (at x within S)"
- shows "Liminf (at x within S) f = C"
- by (metis Lim_within_constant assms lim_imp_Liminf)
-
-lemma Limsup_within_constant:
- fixes f :: "'a::topological_space \<Rightarrow> ereal"
- assumes "ALL y:S. f y = C"
- and "~trivial_limit (at x within S)"
- shows "Limsup (at x within S) f = C"
- by (metis Lim_within_constant assms lim_imp_Limsup)
-
lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
unfolding islimpt_def by blast
@@ -1317,4 +1007,205 @@
then show "\<forall>i. f i = 0" by auto
qed simp
+lemma Liminf_within:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
+ shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
+ unfolding Liminf_def eventually_within
+proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+ by (auto simp: zero_less_dist_iff dist_commute)
+ then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
+ by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
+next
+ fix d :: real assume "0 < d"
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
+ by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+ (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
+qed
+
+lemma Limsup_within:
+ fixes f :: "'a::metric_space => 'b::complete_lattice"
+ shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
+ unfolding Limsup_def eventually_within
+proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+ by (auto simp: zero_less_dist_iff dist_commute)
+ then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
+ by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
+next
+ fix d :: real assume "0 < d"
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
+ by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+ (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
+qed
+
+lemma Liminf_at:
+ fixes f :: "'a::metric_space => _"
+ shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
+ using Liminf_within[of x UNIV f] by simp
+
+lemma Limsup_at:
+ fixes f :: "'a::metric_space => _"
+ shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
+ using Limsup_within[of x UNIV f] by simp
+
+lemma min_Liminf_at:
+ fixes f :: "'a::metric_space => 'b::complete_linorder"
+ shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
+ unfolding inf_min[symmetric] Liminf_at
+ apply (subst inf_commute)
+ apply (subst SUP_inf)
+ apply (intro SUP_cong[OF refl])
+ apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
+ apply (simp add: INF_def del: inf_ereal_def)
+ done
+
+subsection {* monoset *}
+
+definition (in order) mono_set:
+ "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
+
+lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
+lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
+lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
+lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
+
+lemma (in complete_linorder) mono_set_iff:
+ fixes S :: "'a set"
+ defines "a \<equiv> Inf S"
+ shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
+proof
+ assume "mono_set S"
+ then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
+ show ?c
+ proof cases
+ assume "a \<in> S"
+ show ?c
+ using mono[OF _ `a \<in> S`]
+ by (auto intro: Inf_lower simp: a_def)
+ next
+ assume "a \<notin> S"
+ have "S = {a <..}"
+ proof safe
+ fix x assume "x \<in> S"
+ then have "a \<le> x" unfolding a_def by (rule Inf_lower)
+ then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
+ next
+ fix x assume "a < x"
+ then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
+ with mono[of y x] show "x \<in> S" by auto
+ qed
+ then show ?c ..
+ qed
+qed auto
+
+lemma ereal_open_mono_set:
+ fixes S :: "ereal set"
+ shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
+ by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
+ ereal_open_closed mono_set_iff open_ereal_greaterThan)
+
+lemma ereal_closed_mono_set:
+ fixes S :: "ereal set"
+ shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
+ by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
+ ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
+
+lemma ereal_Liminf_Sup_monoset:
+ fixes f :: "'a => ereal"
+ shows "Liminf net f =
+ Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
+ (is "_ = Sup ?A")
+proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
+ fix P assume P: "eventually P net"
+ fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
+ { fix x assume "P x"
+ then have "INFI (Collect P) f \<le> f x"
+ by (intro complete_lattice_class.INF_lower) simp
+ with S have "f x \<in> S"
+ by (simp add: mono_set) }
+ with P show "eventually (\<lambda>x. f x \<in> S) net"
+ by (auto elim: eventually_elim1)
+next
+ fix y l
+ assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
+ assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
+ show "l \<le> y"
+ proof (rule dense_le)
+ fix B assume "B < l"
+ then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
+ by (intro S[rule_format]) auto
+ then have "INFI {x. B < f x} f \<le> y"
+ using P by auto
+ moreover have "B \<le> INFI {x. B < f x} f"
+ by (intro INF_greatest) auto
+ ultimately show "B \<le> y"
+ by simp
+ qed
+qed
+
+lemma ereal_Limsup_Inf_monoset:
+ fixes f :: "'a => ereal"
+ shows "Limsup net f =
+ Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
+ (is "_ = Inf ?A")
+proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
+ fix P assume P: "eventually P net"
+ fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
+ { fix x assume "P x"
+ then have "f x \<le> SUPR (Collect P) f"
+ by (intro complete_lattice_class.SUP_upper) simp
+ with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
+ have "f x \<in> S"
+ by (simp add: inj_image_mem_iff) }
+ with P show "eventually (\<lambda>x. f x \<in> S) net"
+ by (auto elim: eventually_elim1)
+next
+ fix y l
+ assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
+ assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
+ show "y \<le> l"
+ proof (rule dense_ge)
+ fix B assume "l < B"
+ then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
+ by (intro S[rule_format]) auto
+ then have "y \<le> SUPR {x. f x < B} f"
+ using P by auto
+ moreover have "SUPR {x. f x < B} f \<le> B"
+ by (intro SUP_least) auto
+ ultimately show "y \<le> B"
+ by simp
+ qed
+qed
+
+lemma liminf_bounded_open:
+ fixes x :: "nat \<Rightarrow> ereal"
+ shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
+ (is "_ \<longleftrightarrow> ?P x0")
+proof
+ assume "?P x0"
+ then show "x0 \<le> liminf x"
+ unfolding ereal_Liminf_Sup_monoset eventually_sequentially
+ by (intro complete_lattice_class.Sup_upper) auto
+next
+ assume "x0 \<le> liminf x"
+ { fix S :: "ereal set"
+ assume om: "open S & mono_set S & x0:S"
+ { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
+ moreover
+ { assume "~(S=UNIV)"
+ then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
+ then have "B<x0" using om by auto
+ then have "EX N. ALL n>=N. x n : S"
+ unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
+ }
+ ultimately have "EX N. (ALL n>=N. x n : S)" by auto
+ }
+ then show "?P x0" by auto
+qed
+
end
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 05 15:27:08 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 05 15:43:08 2013 +0100
@@ -2190,7 +2190,7 @@
using diff positive_integral_positive[of M]
by (subst integral_eq_positive_integral[of _ M]) (auto simp: ereal_real integrable_def)
then show ?lim_diff
- using ereal_Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
+ using Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
by simp
show ?lim