--- a/src/HOL/Library/Extended_Nat.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Thu Jan 31 11:31:30 2013 +0100
@@ -6,7 +6,7 @@
header {* Extended natural numbers (i.e. with infinity) *}
theory Extended_Nat
-imports Main
+imports "~~/src/HOL/Main"
begin
class infinity =
--- a/src/HOL/Library/Extended_Real.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy Thu Jan 31 11:31:30 2013 +0100
@@ -8,9 +8,32 @@
header {* Extended real number line *}
theory Extended_Real
-imports Complex_Main Extended_Nat
+imports "~~/src/HOL/Complex_Main" Extended_Nat
begin
+lemma LIMSEQ_SUP:
+ fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
+ assumes "incseq X"
+ shows "X ----> (SUP i. X i)"
+ using `incseq X`
+ by (intro increasing_tendsto)
+ (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
+
+lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
+ by (cases P) (simp_all add: eventually_False)
+
+lemma (in complete_lattice) Inf_le_Sup:
+ assumes "A \<noteq> {}" shows "Inf A \<le> Sup A"
+proof -
+ from `A \<noteq> {}` obtain x where "x \<in> A" by auto
+ then show ?thesis
+ by (metis Sup_upper2 Inf_lower)
+qed
+
+lemma (in complete_lattice) INF_le_SUP:
+ "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+ unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
+
text {*
For more lemmas about the extended real numbers go to
@@ -18,6 +41,26 @@
*}
+lemma (in complete_lattice) Sup_eqI:
+ assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
+ assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
+ shows "Sup A = x"
+ by (metis antisym Sup_least Sup_upper assms)
+
+lemma (in complete_lattice) Inf_eqI:
+ assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
+ assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
+ shows "Inf A = x"
+ by (metis antisym Inf_greatest Inf_lower assms)
+
+lemma (in complete_lattice) SUP_eqI:
+ "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (SUP i:A. f i) = x"
+ unfolding SUP_def by (rule Sup_eqI) auto
+
+lemma (in complete_lattice) INF_eqI:
+ "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (INF i:A. f i) = x"
+ unfolding INF_def by (rule Inf_eqI) auto
+
lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
proof
assume "{x..} = UNIV"
@@ -1353,22 +1396,6 @@
unfolding Sup_ereal_def
by (auto intro!: Least_equality)
-lemma ereal_SUPI:
- fixes x :: ereal
- assumes "!!i. i : A ==> f i <= x"
- assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y"
- shows "(SUP i:A. f i) = x"
- unfolding SUP_def Sup_ereal_def
- using assms by (auto intro!: Least_equality)
-
-lemma ereal_INFI:
- fixes x :: ereal
- assumes "!!i. i : A ==> f i >= x"
- assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y"
- shows "(INF i:A. f i) = x"
- unfolding INF_def Inf_ereal_def
- using assms by (auto intro!: Greatest_equality)
-
lemma Sup_ereal_close:
fixes e :: ereal
assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
@@ -1476,6 +1503,17 @@
using assms by (metis SUP_least SUP_upper2)
qed
+lemma INFI_eq:
+ assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<ge> g j"
+ assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<ge> f i"
+ shows "(INF i:A. f i) = (INF j:B. g j)"
+proof (intro antisym)
+ show "(INF i:A. f i) \<le> (INF j:B. g j)"
+ using assms by (metis INF_greatest INF_lower2)
+ show "(INF i:B. g i) \<le> (INF j:A. f j)"
+ using assms by (metis INF_greatest INF_lower2)
+qed
+
lemma SUP_ereal_le_addI:
fixes f :: "'i \<Rightarrow> ereal"
assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
@@ -1491,7 +1529,7 @@
fixes f g :: "nat \<Rightarrow> ereal"
assumes "incseq f" "incseq g" and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
-proof (rule ereal_SUPI)
+proof (rule SUP_eqI)
fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
@@ -1531,7 +1569,7 @@
lemma SUPR_ereal_cmult:
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
shows "(SUP i. c * f i) = c * SUPR UNIV f"
-proof (rule ereal_SUPI)
+proof (rule SUP_eqI)
fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
then show "c * f i \<le> c * SUPR UNIV f"
using `0 \<le> c` by (rule ereal_mult_left_mono)
@@ -1598,7 +1636,7 @@
qed
from choice[OF this] guess f .. note f = this
have "SUPR UNIV f = Sup A"
- proof (rule ereal_SUPI)
+ proof (rule SUP_eqI)
fix i show "f i \<le> Sup A" using f
by (auto intro!: complete_lattice_class.Sup_upper)
next
@@ -1801,18 +1839,84 @@
subsubsection "Topological space"
-instantiation ereal :: topological_space
+instantiation ereal :: linorder_topology
begin
-definition "open A \<longleftrightarrow> open (ereal -` A)
- \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A))
- \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
+definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
+ open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
+
+instance
+ by default (simp add: open_ereal_generated)
+end
lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
- unfolding open_ereal_def by auto
+ unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+ case (Int A B)
+ moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
+ by auto
+ ultimately show ?case
+ by (intro exI[of _ "max x z"]) fastforce
+next
+ { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
+ moreover case (Basis S)
+ ultimately show ?case
+ by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
- unfolding open_ereal_def by auto
+ unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+ case (Int A B)
+ moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
+ by auto
+ ultimately show ?case
+ by (intro exI[of _ "min x z"]) fastforce
+next
+ { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
+ moreover case (Basis S)
+ ultimately show ?case
+ by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
+
+lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
+ unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+ case (Int A B) then show ?case by auto
+next
+ { fix x have
+ "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
+ "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
+ by (induct x) auto }
+ moreover case (Basis S)
+ ultimately show ?case
+ by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
+
+lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
+ unfolding open_generated_order[where 'a=real]
+proof (induct rule: generate_topology.induct)
+ case (Basis S)
+ moreover { fix x have "ereal ` {..< x} = { -\<infinity> <..< ereal x }" by auto (case_tac xa, auto) }
+ moreover { fix x have "ereal ` {x <..} = { ereal x <..< \<infinity> }" by auto (case_tac xa, auto) }
+ ultimately show ?case
+ by auto
+qed (auto simp add: image_Union image_Int)
+
+lemma open_ereal_def: "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
+ (is "open A \<longleftrightarrow> ?rhs")
+proof
+ assume "open A" then show ?rhs
+ using open_PInfty open_MInfty open_ereal_vimage by auto
+next
+ assume "?rhs"
+ then obtain x y where A: "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..< ereal y} \<subseteq> A"
+ by auto
+ have *: "A = ereal ` (ereal -` A) \<union> (if \<infinity> \<in> A then {ereal x<..} else {}) \<union> (if -\<infinity> \<in> A then {..< ereal y} else {})"
+ using A(2,3) by auto
+ from open_ereal[OF A(1)] show "open A"
+ by (subst *) (auto simp: open_Un)
+qed
lemma open_PInfty2: assumes "open A" "\<infinity> \<in> A" obtains x where "{ereal x<..} \<subseteq> A"
using open_PInfty[OF assms] by auto
@@ -1821,85 +1925,17 @@
using open_MInfty[OF assms] by auto
lemma ereal_openE: assumes "open A" obtains x y where
- "open (ereal -` A)"
- "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
- "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
+ "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
using assms open_ereal_def by auto
-instance
-proof
- let ?U = "UNIV::ereal set"
- show "open ?U" unfolding open_ereal_def
- by (auto intro!: exI[of _ 0])
-next
- fix S T::"ereal set" assume "open S" and "open T"
- from `open S`[THEN ereal_openE] guess xS yS .
- moreover from `open T`[THEN ereal_openE] guess xT yT .
- ultimately have
- "open (ereal -` (S \<inter> T))"
- "\<infinity> \<in> S \<inter> T \<Longrightarrow> {ereal (max xS xT) <..} \<subseteq> S \<inter> T"
- "-\<infinity> \<in> S \<inter> T \<Longrightarrow> {..< ereal (min yS yT)} \<subseteq> S \<inter> T"
- by auto
- then show "open (S Int T)" unfolding open_ereal_def by blast
-next
- fix K :: "ereal set set" assume "\<forall>S\<in>K. open S"
- then have *: "\<forall>S. \<exists>x y. S \<in> K \<longrightarrow> open (ereal -` S) \<and>
- (\<infinity> \<in> S \<longrightarrow> {ereal x <..} \<subseteq> S) \<and> (-\<infinity> \<in> S \<longrightarrow> {..< ereal y} \<subseteq> S)"
- by (auto simp: open_ereal_def)
- then show "open (Union K)" unfolding open_ereal_def
- proof (intro conjI impI)
- show "open (ereal -` \<Union>K)"
- using *[THEN choice] by (auto simp: vimage_Union)
- qed ((metis UnionE Union_upper subset_trans *)+)
-qed
-end
-
-lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
- by (auto simp: inj_vimage_image_eq open_ereal_def)
-
-lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
- unfolding open_ereal_def by auto
-
-lemma open_ereal_lessThan[intro, simp]: "open {..< a :: ereal}"
-proof -
- have "\<And>x. ereal -` {..<ereal x} = {..< x}"
- "ereal -` {..< \<infinity>} = UNIV" "ereal -` {..< -\<infinity>} = {}" by auto
- then show ?thesis by (cases a) (auto simp: open_ereal_def)
-qed
-
-lemma open_ereal_greaterThan[intro, simp]:
- "open {a :: ereal <..}"
-proof -
- have "\<And>x. ereal -` {ereal x<..} = {x<..}"
- "ereal -` {\<infinity><..} = {}" "ereal -` {-\<infinity><..} = UNIV" by auto
- then show ?thesis by (cases a) (auto simp: open_ereal_def)
-qed
-
-lemma ereal_open_greaterThanLessThan[intro, simp]: "open {a::ereal <..< b}"
- unfolding greaterThanLessThan_def by auto
-
-lemma closed_ereal_atLeast[simp, intro]: "closed {a :: ereal ..}"
-proof -
- have "- {a ..} = {..< a}" by auto
- then show "closed {a ..}"
- unfolding closed_def using open_ereal_lessThan by auto
-qed
-
-lemma closed_ereal_atMost[simp, intro]: "closed {.. b :: ereal}"
-proof -
- have "- {.. b} = {b <..}" by auto
- then show "closed {.. b}"
- unfolding closed_def using open_ereal_greaterThan by auto
-qed
-
-lemma closed_ereal_atLeastAtMost[simp, intro]:
- shows "closed {a :: ereal .. b}"
- unfolding atLeastAtMost_def by auto
-
-lemma closed_ereal_singleton:
- "closed {a :: ereal}"
-by (metis atLeastAtMost_singleton closed_ereal_atLeastAtMost)
-
+lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
+lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
+lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
+lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
+lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
+lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
+lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
+
lemma ereal_open_cont_interval:
fixes S :: "ereal set"
assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
@@ -1928,28 +1964,6 @@
show thesis by auto
qed
-instance ereal :: t2_space
-proof
- fix x y :: ereal assume "x ~= y"
- let "?P x (y::ereal)" = "EX U V. open U & open V & x : U & y : V & U Int V = {}"
-
- { fix x y :: ereal assume "x < y"
- from ereal_dense[OF this] obtain z where z: "x < z" "z < y" by auto
- have "?P x y"
- apply (rule exI[of _ "{..<z}"])
- apply (rule exI[of _ "{z<..}"])
- using z by auto }
- note * = this
-
- from `x ~= y`
- show "EX U V. open U & open V & x : U & y : V & U Int V = {}"
- proof (cases rule: linorder_cases)
- assume "x = y" with `x ~= y` show ?thesis by simp
- next assume "x < y" from *[OF this] show ?thesis by auto
- next assume "y < x" from *[OF this] show ?thesis by auto
- qed
-qed
-
subsubsection {* Convergent sequences *}
lemma lim_ereal[simp]:
@@ -1979,152 +1993,72 @@
by (rule eventually_mono)
qed
-lemma Lim_PInfty: "f ----> \<infinity> <-> (ALL B. EX N. ALL n>=N. f n >= ereal B)" (is "?l = ?r")
-proof
- assume ?r
- show ?l
- apply(rule topological_tendstoI)
- unfolding eventually_sequentially
- proof-
- fix S :: "ereal set" assume "open S" "\<infinity> : S"
- from open_PInfty[OF this] guess B .. note B=this
- from `?r`[rule_format,of "B+1"] guess N .. note N=this
- show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
- proof safe case goal1
- have "ereal B < ereal (B + 1)" by auto
- also have "... <= f n" using goal1 N by auto
- finally show ?case using B by fastforce
- qed
- qed
+lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
+ unfolding tendsto_def
+proof safe
+ fix S :: "ereal set" assume "open S" "\<infinity> \<in> S"
+ from open_PInfty[OF this] guess B .. note B = this
+ moreover
+ assume "\<forall>r::real. eventually (\<lambda>z. r < f z) F"
+ then have "eventually (\<lambda>z. f z \<in> {B <..}) F" by auto
+ ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
next
- assume ?l
- show ?r
- proof fix B::real have "open {ereal B<..}" "\<infinity> : {ereal B<..}" by auto
- from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
- guess N .. note N=this
- show "EX N. ALL n>=N. ereal B <= f n" apply(rule_tac x=N in exI) using N by auto
- qed
+ fix x assume "\<forall>S. open S \<longrightarrow> \<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
+ from this[rule_format, of "{ereal x <..}"]
+ show "eventually (\<lambda>y. ereal x < f y) F" by auto
qed
-
-lemma Lim_MInfty: "f ----> (-\<infinity>) <-> (ALL B. EX N. ALL n>=N. f n <= ereal B)" (is "?l = ?r")
-proof
- assume ?r
- show ?l
- apply(rule topological_tendstoI)
- unfolding eventually_sequentially
- proof-
- fix S :: "ereal set"
- assume "open S" "(-\<infinity>) : S"
- from open_MInfty[OF this] guess B .. note B=this
- from `?r`[rule_format,of "B-(1::real)"] guess N .. note N=this
- show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
- proof safe case goal1
- have "ereal (B - 1) >= f n" using goal1 N by auto
- also have "... < ereal B" by auto
- finally show ?case using B by fastforce
- qed
- qed
-next assume ?l show ?r
- proof fix B::real have "open {..<ereal B}" "(-\<infinity>) : {..<ereal B}" by auto
- from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
- guess N .. note N=this
- show "EX N. ALL n>=N. ereal B >= f n" apply(rule_tac x=N in exI) using N by auto
- qed
+lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
+ unfolding tendsto_def
+proof safe
+ fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
+ from open_MInfty[OF this] guess B .. note B = this
+ moreover
+ assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
+ then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
+ ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
+next
+ fix x assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
+ from this[rule_format, of "{..< ereal x}"]
+ show "eventually (\<lambda>y. f y < ereal x) F" by auto
qed
-
-lemma Lim_bounded_PInfty: assumes lim:"f ----> l" and "!!n. f n <= ereal B" shows "l ~= \<infinity>"
-proof(rule ccontr,unfold not_not) let ?B = "B + 1" assume as:"l=\<infinity>"
- from lim[unfolded this Lim_PInfty,rule_format,of "?B"]
- guess N .. note N=this[rule_format,OF le_refl]
- hence "ereal ?B <= ereal B" using assms(2)[of N] by(rule order_trans)
- hence "ereal ?B < ereal ?B" apply (rule le_less_trans) by auto
- thus False by auto
-qed
+lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
+ unfolding tendsto_PInfty eventually_sequentially
+proof safe
+ fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
+ from this[rule_format, of "r+1"] guess N ..
+ moreover have "ereal r < ereal (r + 1)" by auto
+ ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
+ by (blast intro: less_le_trans)
+qed (blast intro: less_imp_le)
+lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
+ unfolding tendsto_MInfty eventually_sequentially
+proof safe
+ fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
+ from this[rule_format, of "r - 1"] guess N ..
+ moreover have "ereal (r - 1) < ereal r" by auto
+ ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
+ by (blast intro: le_less_trans)
+qed (blast intro: less_imp_le)
-lemma Lim_bounded_MInfty: assumes lim:"f ----> l" and "!!n. f n >= ereal B" shows "l ~= (-\<infinity>)"
-proof(rule ccontr,unfold not_not) let ?B = "B - 1" assume as:"l=(-\<infinity>)"
- from lim[unfolded this Lim_MInfty,rule_format,of "?B"]
- guess N .. note N=this[rule_format,OF le_refl]
- hence "ereal B <= ereal ?B" using assms(2)[of N] order_trans[of "ereal B" "f N" "ereal(B - 1)"] by blast
- thus False by auto
-qed
+lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
+ using LIMSEQ_le_const2[of f l "ereal B"] by auto
+lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
+ using LIMSEQ_le_const[of f l "ereal B"] by auto
lemma tendsto_explicit:
"f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
unfolding tendsto_def eventually_sequentially by auto
-
-lemma tendsto_obtains_N:
- assumes "f ----> f0"
- assumes "open S" "f0 : S"
- obtains N where "ALL n>=N. f n : S"
- using tendsto_explicit[of f f0] assms by auto
-
-
-lemma tail_same_limit:
- fixes X Y N
- assumes "X ----> L" "ALL n>=N. X n = Y n"
- shows "Y ----> L"
-proof-
-{ fix S assume "open S" and "L:S"
- then obtain N1 where "ALL n>=N1. X n : S"
- using assms unfolding tendsto_def eventually_sequentially by auto
- hence "ALL n>=max N N1. Y n : S" using assms by auto
- hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
-}
-thus ?thesis using tendsto_explicit by auto
-qed
-
-
lemma Lim_bounded_PInfty2:
-assumes lim:"f ----> l" and "ALL n>=N. f n <= ereal B"
-shows "l ~= \<infinity>"
-proof-
- def g == "(%n. if n>=N then f n else ereal B)"
- hence "g ----> l" using tail_same_limit[of f l N g] lim by auto
- moreover have "!!n. g n <= ereal B" using g_def assms by auto
- ultimately show ?thesis using Lim_bounded_PInfty by auto
-qed
+ "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
+ using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
-lemma Lim_bounded_ereal:
- assumes lim:"f ----> (l :: ereal)"
- and "ALL n>=M. f n <= C"
- shows "l<=C"
-proof-
-{ assume "l=(-\<infinity>)" hence ?thesis by auto }
-moreover
-{ assume "~(l=(-\<infinity>))"
- { assume "C=\<infinity>" hence ?thesis by auto }
- moreover
- { assume "C=(-\<infinity>)" hence "ALL n>=M. f n = (-\<infinity>)" using assms by auto
- hence "l=(-\<infinity>)" using assms
- tendsto_unique[OF trivial_limit_sequentially] tail_same_limit[of "\<lambda>n. -\<infinity>" "-\<infinity>" M f, OF tendsto_const] by auto
- hence ?thesis by auto }
- moreover
- { assume "EX B. C = ereal B"
- then obtain B where B_def: "C=ereal B" by auto
- hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
- then obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
- then obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
- apply (subst tendsto_obtains_N[of f l "{ereal(m - 1) <..< ereal(m+1)}"]) using assms by auto
- { fix n assume "n>=N"
- hence "EX r. ereal r = f n" using N_def by (cases "f n") auto
- } then obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
- hence "(%n. ereal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
- hence *: "(%n. g n) ----> m" using m_def by auto
- { fix n assume "n>=max N M"
- hence "ereal (g n) <= ereal B" using assms g_def B_def by auto
- hence "g n <= B" by auto
- } hence "EX N. ALL n>=N. g n <= B" by blast
- hence "m<=B" using * LIMSEQ_le_const2[of g m B] by auto
- hence ?thesis using m_def B_def by auto
- } ultimately have ?thesis by (cases C) auto
-} ultimately show ?thesis by blast
-qed
+lemma Lim_bounded_ereal: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
+ by (intro LIMSEQ_le_const2) auto
lemma real_of_ereal_mult[simp]:
fixes a b :: ereal shows "real (a * b) = real a * real b"
@@ -2204,349 +2138,6 @@
lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
by (cases x) auto
-lemma ereal_LimI_finite:
- fixes x :: ereal
- assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
- shows "u ----> x"
-proof (rule topological_tendstoI, unfold eventually_sequentially)
- obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
- fix S assume "open S" "x : S"
- then have "open (ereal -` S)" unfolding open_ereal_def by auto
- with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
- unfolding open_real_def rx_def by auto
- then obtain n where
- upper: "!!N. n <= N ==> u N < x + ereal r" and
- lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
- show "EX N. ALL n>=N. u n : S"
- proof (safe intro!: exI[of _ n])
- fix N assume "n <= N"
- from upper[OF this] lower[OF this] assms `0 < r`
- have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
- then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
- hence "rx < ra + r" and "ra < rx + r"
- using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
- hence "dist (real (u N)) rx < r"
- using rx_def ra_def
- by (auto simp: dist_real_def abs_diff_less_iff field_simps)
- from dist[OF this] show "u N : S" using `u N ~: {\<infinity>, -\<infinity>}`
- by (auto simp: ereal_real split: split_if_asm)
- qed
-qed
-
-lemma ereal_LimI_finite_iff:
- fixes x :: ereal
- assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
- (is "?lhs <-> ?rhs")
-proof
- assume lim: "u ----> x"
- { fix r assume "(r::ereal)>0"
- then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
- apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
- using lim ereal_between[of x r] assms `r>0` by auto
- hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
- using ereal_minus_less[of r x] by (cases r) auto
- } then show "?rhs" by auto
-next
- assume ?rhs then show "u ----> x"
- using ereal_LimI_finite[of x] assms by auto
-qed
-
-
-subsubsection {* @{text Liminf} and @{text Limsup} *}
-
-definition
- "Liminf net f = (GREATEST l. \<forall>y<l. eventually (\<lambda>x. y < f x) net)"
-
-definition
- "Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
-
-lemma Liminf_Sup:
- fixes f :: "'a => 'b::complete_linorder"
- shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
- by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
-
-lemma Limsup_Inf:
- fixes f :: "'a => 'b::complete_linorder"
- shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
- by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
-
-lemma ereal_SupI:
- fixes x :: ereal
- assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
- assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
- shows "Sup A = x"
- unfolding Sup_ereal_def
- using assms by (auto intro!: Least_equality)
-
-lemma ereal_InfI:
- fixes x :: ereal
- assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
- assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
- shows "Inf A = x"
- unfolding Inf_ereal_def
- using assms by (auto intro!: Greatest_equality)
-
-lemma Limsup_const:
- fixes c :: "'a::complete_linorder"
- assumes ntriv: "\<not> trivial_limit net"
- shows "Limsup net (\<lambda>x. c) = c"
- unfolding Limsup_Inf
-proof (safe intro!: antisym complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower)
- fix x assume *: "\<forall>y>x. eventually (\<lambda>_. c < y) net"
- show "c \<le> x"
- proof (rule ccontr)
- assume "\<not> c \<le> x" then have "x < c" by auto
- then show False using ntriv * by (auto simp: trivial_limit_def)
- qed
-qed auto
-
-lemma Liminf_const:
- fixes c :: "'a::complete_linorder"
- assumes ntriv: "\<not> trivial_limit net"
- shows "Liminf net (\<lambda>x. c) = c"
- unfolding Liminf_Sup
-proof (safe intro!: antisym complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
- fix x assume *: "\<forall>y<x. eventually (\<lambda>_. y < c) net"
- show "x \<le> c"
- proof (rule ccontr)
- assume "\<not> x \<le> c" then have "c < x" by auto
- then show False using ntriv * by (auto simp: trivial_limit_def)
- qed
-qed auto
-
-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 lim_imp_Liminf:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes ntriv: "\<not> trivial_limit net"
- assumes lim: "(f ---> f0) net"
- shows "Liminf net f = f0"
- unfolding Liminf_Sup
-proof (safe intro!: ereal_SupI)
- fix y assume *: "\<forall>y'<y. eventually (\<lambda>x. y' < f x) net"
- show "y \<le> f0"
- proof (rule ereal_le_ereal)
- fix B assume "B < y"
- { assume "f0 < B"
- then have "eventually (\<lambda>x. f x < B \<and> B < f x) net"
- using topological_tendstoD[OF lim, of "{..<B}"] *[rule_format, OF `B < y`]
- by (auto intro: eventually_conj)
- also have "(\<lambda>x. f x < B \<and> B < f x) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
- finally have False using ntriv[unfolded trivial_limit_def] by auto
- } then show "B \<le> f0" by (metis linorder_le_less_linear)
- qed
-next
- fix y assume *: "\<forall>z. z \<in> {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net} \<longrightarrow> z \<le> y"
- show "f0 \<le> y"
- proof (safe intro!: *[rule_format])
- fix y assume "y < f0" then show "eventually (\<lambda>x. y < f x) net"
- using lim[THEN topological_tendstoD, of "{y <..}"] by auto
- qed
-qed
-
-lemma ereal_Liminf_le_Limsup:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes ntriv: "\<not> trivial_limit net"
- shows "Liminf net f \<le> Limsup net f"
- unfolding Limsup_Inf Liminf_Sup
-proof (safe intro!: complete_lattice_class.Inf_greatest complete_lattice_class.Sup_least)
- fix u v assume *: "\<forall>y<u. eventually (\<lambda>x. y < f x) net" "\<forall>y>v. eventually (\<lambda>x. f x < y) net"
- show "u \<le> v"
- proof (rule ccontr)
- assume "\<not> u \<le> v"
- then obtain t where "t < u" "v < t"
- using ereal_dense[of v u] by (auto simp: not_le)
- then have "eventually (\<lambda>x. t < f x \<and> f x < t) net"
- using * by (auto intro: eventually_conj)
- also have "(\<lambda>x. t < f x \<and> f x < t) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
- finally show False using ntriv by (auto simp: trivial_limit_def)
- qed
-qed
-
-lemma Liminf_mono:
- fixes f g :: "'a => ereal"
- assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
- shows "Liminf net f \<le> Liminf net g"
- unfolding Liminf_Sup
-proof (safe intro!: Sup_mono bexI)
- fix a y assume "\<forall>y<a. eventually (\<lambda>x. y < f x) net" and "y < a"
- then have "eventually (\<lambda>x. y < f x) net" by auto
- then show "eventually (\<lambda>x. y < g x) net"
- by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
-qed simp
-
-lemma Liminf_eq:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes "eventually (\<lambda>x. f x = g x) net"
- shows "Liminf net f = Liminf net g"
- by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
-
-lemma Liminf_mono_all:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes "\<And>x. f x \<le> g x"
- shows "Liminf net f \<le> Liminf net g"
- using assms by (intro Liminf_mono always_eventually) auto
-
-lemma Limsup_mono:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
- shows "Limsup net f \<le> Limsup net g"
- unfolding Limsup_Inf
-proof (safe intro!: Inf_mono bexI)
- fix a y assume "\<forall>y>a. eventually (\<lambda>x. g x < y) net" and "a < y"
- then have "eventually (\<lambda>x. g x < y) net" by auto
- then show "eventually (\<lambda>x. f x < y) net"
- by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
-qed simp
-
-lemma Limsup_mono_all:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes "\<And>x. f x \<le> g x"
- shows "Limsup net f \<le> Limsup net g"
- using assms by (intro Limsup_mono always_eventually) auto
-
-lemma Limsup_eq:
- fixes f g :: "'a \<Rightarrow> ereal"
- 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
-
-abbreviation "liminf \<equiv> Liminf sequentially"
-
-abbreviation "limsup \<equiv> Limsup sequentially"
-
-lemma liminf_SUPR_INFI:
- fixes f :: "nat \<Rightarrow> ereal"
- shows "liminf f = (SUP n. INF m:{n..}. f m)"
- unfolding Liminf_Sup eventually_sequentially
-proof (safe intro!: antisym complete_lattice_class.Sup_least)
- fix x assume *: "\<forall>y<x. \<exists>N. \<forall>n\<ge>N. y < f n" show "x \<le> (SUP n. INF m:{n..}. f m)"
- proof (rule ereal_le_ereal)
- fix y assume "y < x"
- with * obtain N where "\<And>n. N \<le> n \<Longrightarrow> y < f n" by auto
- then have "y \<le> (INF m:{N..}. f m)" by (force simp: le_INF_iff)
- also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro SUP_upper) auto
- finally show "y \<le> (SUP n. INF m:{n..}. f m)" .
- qed
-next
- show "(SUP n. INF m:{n..}. f m) \<le> Sup {l. \<forall>y<l. \<exists>N. \<forall>n\<ge>N. y < f n}"
- proof (unfold SUP_def, safe intro!: Sup_mono bexI)
- fix y n assume "y < INFI {n..} f"
- from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
- qed (rule order_refl)
-qed
-
-lemma tail_same_limsup:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
- shows "limsup X = limsup Y"
- using Limsup_eq[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma tail_same_liminf:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
- shows "liminf X = liminf Y"
- using Liminf_eq[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma liminf_mono:
- fixes X Y :: "nat \<Rightarrow> ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
- shows "liminf X \<le> liminf Y"
- using Liminf_mono[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma limsup_mono:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
- shows "limsup X \<le> limsup Y"
- using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma
- fixes X :: "nat \<Rightarrow> ereal"
- shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
- 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 :: "nat \<Rightarrow> ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> C \<le> X n"
- shows "C \<le> liminf X"
- using liminf_mono[of N "\<lambda>n. C" X] assms Liminf_const[of sequentially C] by simp
-
-lemma limsup_bounded:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= C"
- shows "limsup X \<le> C"
- using limsup_mono[of N X "\<lambda>n. C"] assms Limsup_const[of sequentially C] by simp
-
-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")
-proof safe
- fix B assume "B < C" "C \<le> liminf x"
- then have "B < liminf x" by auto
- then obtain N where "B < (INF m:{N..}. x m)"
- unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
- from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
-next
- assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
- { fix B assume "B<C"
- then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
- hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
- also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
- finally have "B \<le> liminf x" .
- } then show "?lhs" by (metis * leD liminf_bounded linorder_le_less_linear)
-qed
-
-lemma liminf_subseq_mono:
- fixes X :: "nat \<Rightarrow> ereal"
- 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 ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
using assms by auto
@@ -2618,6 +2209,333 @@
"[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
by (metis sup_ereal_def sup_least)
+
+lemma ereal_LimI_finite:
+ fixes x :: ereal
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
+ shows "u ----> x"
+proof (rule topological_tendstoI, unfold eventually_sequentially)
+ obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
+ fix S assume "open S" "x : S"
+ then have "open (ereal -` S)" unfolding open_ereal_def by auto
+ with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
+ unfolding open_real_def rx_def by auto
+ then obtain n where
+ upper: "!!N. n <= N ==> u N < x + ereal r" and
+ lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
+ show "EX N. ALL n>=N. u n : S"
+ proof (safe intro!: exI[of _ n])
+ fix N assume "n <= N"
+ from upper[OF this] lower[OF this] assms `0 < r`
+ have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
+ then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
+ hence "rx < ra + r" and "ra < rx + r"
+ using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
+ hence "dist (real (u N)) rx < r"
+ using rx_def ra_def
+ by (auto simp: dist_real_def abs_diff_less_iff field_simps)
+ from dist[OF this] show "u N : S" using `u N ~: {\<infinity>, -\<infinity>}`
+ by (auto simp: ereal_real split: split_if_asm)
+ qed
+qed
+
+lemma tendsto_obtains_N:
+ assumes "f ----> f0"
+ assumes "open S" "f0 : S"
+ obtains N where "ALL n>=N. f n : S"
+ using tendsto_explicit[of f f0] assms by auto
+
+lemma ereal_LimI_finite_iff:
+ fixes x :: ereal
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
+ (is "?lhs <-> ?rhs")
+proof
+ assume lim: "u ----> x"
+ { fix r assume "(r::ereal)>0"
+ then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
+ apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
+ using lim ereal_between[of x r] assms `r>0` by auto
+ hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
+ using ereal_minus_less[of r x] by (cases r) auto
+ } then show "?rhs" by auto
+next
+ assume ?rhs then show "u ----> x"
+ 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 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
+ fixes X :: "nat \<Rightarrow> ereal"
+ shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
+ 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 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")
+proof safe
+ fix B assume "B < C" "C \<le> liminf x"
+ then have "B < liminf x" by auto
+ then obtain N where "B < (INF m:{N..}. x m)"
+ unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
+ from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
+next
+ assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
+ { fix B assume "B<C"
+ then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
+ hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
+ also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
+ finally have "B \<le> liminf x" .
+ } then show "?lhs"
+ by (metis * leD Liminf_bounded[OF sequentially_bot] linorder_le_less_linear eventually_sequentially)
+qed
+
+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
+
+lemma lim_imp_Liminf:
+ fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ shows "Liminf F f = f0"
+proof (rule Liminf_eqI)
+ fix y assume *: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+ show "f0 \<le> y"
+ proof (rule ereal_le_ereal)
+ fix B
+ assume "B < f0"
+ have "B \<le> INFI {x. B < f x} f"
+ by (rule INF_greatest) simp
+ also have "INFI {x. B < f x} f \<le> y"
+ using lim[THEN topological_tendstoD, of "{B <..}"] `B < f0` * by auto
+ finally show "B \<le> y" .
+ qed
+next
+ 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])
+qed
+
+lemma lim_imp_Limsup:
+ fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ shows "Limsup F f = f0"
+proof (rule Limsup_eqI)
+ fix y assume *: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
+ show "y \<le> f0"
+ proof (rule ereal_ge_ereal, safe)
+ fix B
+ assume "f0 < B"
+ have "y \<le> SUPR {x. f x < B} f"
+ using lim[THEN topological_tendstoD, of "{..< B}"] `f0 < B` * by auto
+ also have "SUPR {x. f x < B} f \<le> B"
+ by (rule SUP_least) simp
+ finally show "y \<le> B" .
+ qed
+next
+ 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])
+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 *)
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Jan 31 11:31:30 2013 +0100
@@ -288,16 +288,9 @@
assumes lim:"f ----> (l :: ereal)"
and ge: "ALL n>=N. f n >= C"
shows "l>=C"
-proof -
- def g == "(%i. -(f i))"
- { fix n
- assume "n>=N"
- then have "g n <= -C" using assms ereal_minus_le_minus g_def by auto }
- then have "ALL n>=N. g n <= -C" by auto
- moreover have limg: "g ----> (-l)" using g_def ereal_lim_uminus lim by auto
- ultimately have "-l <= -C" using Lim_bounded_ereal[of g "-l" _ "-C"] by auto
- then show ?thesis using ereal_minus_le_minus by auto
-qed
+ using ge
+ by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+ (auto simp: eventually_sequentially)
lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
proof
@@ -326,54 +319,69 @@
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}"
- unfolding Liminf_Sup
-proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
- fix l S
- assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
- then have "S = UNIV \<or> S = {Inf S <..}"
- using ereal_open_mono_set[of S] by auto
- then show "eventually (\<lambda>x. f x \<in> S) net"
- proof
- assume S: "S = {Inf S<..}"
- then have "Inf S < l" using `l \<in> S` by auto
- then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
- then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
- qed auto
+ (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 l y
- assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "y < l"
- have "eventually (\<lambda>x. f x \<in> {y <..}) net"
- using `y < l` by (intro S[rule_format]) auto
- then show "eventually (\<lambda>x. y < f x) net" by auto
+ 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 ereal_le_ereal)
+ 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}"
- unfolding Limsup_Inf
-proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
- fix l S
- assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
- then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
- then have "S = UNIV \<or> S = {..< Sup S}"
- unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
- then show "eventually (\<lambda>x. f x \<in> S) net"
- proof
- assume S: "S = {..< Sup S}"
- then have "l < Sup S" using `l \<in> S` by auto
- then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
- then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
- qed auto
+ (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 l y
- assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "l < y"
- have "eventually (\<lambda>x. f x \<in> {..< y}) net"
- using `l < y` by (intro S[rule_format]) auto
- then show "eventually (\<lambda>x. f x < y) net" by auto
+ 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 ereal_ge_ereal, safe)
+ 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
@@ -434,21 +442,16 @@
shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
proof (intro lim_imp_Liminf iffI assms)
assume rhs: "Liminf net f = \<infinity>"
- { fix S :: "ereal set"
- assume "open S & \<infinity> : S"
- then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto
- moreover
- have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net"
- using rhs
- unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff
- by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def)
- ultimately
- have "eventually (%x. f x : S) net"
- apply (subst eventually_mono)
- apply auto
- done
- }
- then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
+ show "(f ---> \<infinity>) net"
+ unfolding tendsto_PInfty
+ proof
+ fix r :: real
+ have "ereal r < top" unfolding top_ereal_def by simp
+ with rhs obtain P where "eventually P net" "r < INFI (Collect P) f"
+ unfolding Liminf_def SUP_eq_top_iff top_ereal_def[symmetric] by auto
+ then show "eventually (\<lambda>x. ereal r < f x) net"
+ by (auto elim!: eventually_elim1 dest: less_INF_D)
+ qed
qed
lemma Limsup_MInfty:
@@ -474,12 +477,12 @@
show "(f ---> f0) net"
proof (rule topological_tendstoI)
fix S
- assume "open S""f0 \<in> 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_Sup Limsup_Inf less_Sup_iff Inf_less_iff
- by (auto intro!: eventually_conj)
+ 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
@@ -518,7 +521,7 @@
assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
and "X ----> x" "Y ----> y"
shows "x <= y"
- by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
+ using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
lemma incseq_le_ereal:
fixes X :: "nat \<Rightarrow> ereal"
@@ -577,114 +580,24 @@
by (metis abs_less_iff assms leI le_max_iff_disj
less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-lemma bounded_increasing_convergent2:
- fixes f::"nat => real"
- assumes "ALL n. f n <= B" "ALL n m. n>=m --> f n >= f m"
- shows "EX l. (f ---> l) sequentially"
-proof -
- def N == "max (abs (f 0)) (abs B)"
- { fix n
- have "abs (f n) <= N"
- unfolding N_def
- apply (subst bounded_abs)
- using assms apply auto
- done }
- then have "bounded {f n| n::nat. True}"
- unfolding bounded_real by auto
- then show ?thesis
- apply (rule Topology_Euclidean_Space.bounded_increasing_convergent)
- using assms apply auto
- done
-qed
-
lemma lim_ereal_increasing:
- assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
- obtains l where "f ----> (l::ereal)"
-proof (cases "f = (\<lambda>x. - \<infinity>)")
- case True
- then show thesis
- using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
-next
- case False
- then obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
- have "ALL n>=N. f n >= f N" using assms by auto
- then have minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
- def Y == "(%n. (if n>=N then f n else f N))"
- then have incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
- from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
- show thesis
- proof (cases "EX B. ALL n. f n < ereal B")
- case False
- then show thesis
- apply -
- apply (rule that[of \<infinity>])
- unfolding Lim_PInfty not_ex not_all
- apply safe
- apply (erule_tac x=B in allE, safe)
- apply (rule_tac x=x in exI, safe)
- apply (rule order_trans[OF _ assms[rule_format]])
- apply auto
- done
- next
- case True
- then guess B ..
- then have "ALL n. Y n < ereal B" using Y_def by auto
- note B = this[rule_format]
- { fix n
- have "Y n < \<infinity>"
- using B[of n]
- apply (subst less_le_trans)
- apply auto
- done
- then have "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
- }
- then have *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
- { fix n
- have "real (Y n) < B"
- proof -
- case goal1
- then show ?case
- using B[of n] apply-apply(subst(asm) ereal_real'[THEN sym]) defer defer
- unfolding ereal_less using * by auto
- qed
- }
- then have B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
- have "EX l. (%n. real (Y n)) ----> l"
- apply (rule bounded_increasing_convergent2)
- proof safe
- show "\<And>n. real (Y n) <= B" using B' by auto
- fix n m :: nat
- assume "n<=m"
- then have "ereal (real (Y n)) <= ereal (real (Y m))"
- using incy[rule_format,of n m] apply(subst ereal_real)+
- using *[rule_format, of n] *[rule_format, of m] by auto
- then show "real (Y n) <= real (Y m)" by auto
- qed
- then guess l .. note l=this
- have "Y ----> ereal l"
- using l
- apply -
- apply (subst(asm) lim_ereal[THEN sym])
- unfolding ereal_real
- using * apply auto
- done
- then show thesis
- apply -
- apply (rule that[of "ereal l"])
- apply (subst tail_same_limit[of Y _ N])
- using Y_def apply auto
- done
- qed
+ assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
+ obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
+proof
+ show "f ----> (SUP n. f n)"
+ using assms
+ by (intro increasing_tendsto)
+ (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
qed
lemma lim_ereal_decreasing:
- assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
- obtains l where "f ----> (l::ereal)"
-proof -
- from lim_ereal_increasing[of "\<lambda>x. - f x"] assms
- obtain l where "(\<lambda>x. - f x) ----> l" by auto
- from ereal_lim_mult[OF this, of "- 1"] show thesis
- by (intro that[of "-l"]) (simp add: ereal_uminus_eq_reorder)
+ assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
+ obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
+proof
+ show "f ----> (INF n. f n)"
+ using assms
+ by (intro decreasing_tendsto)
+ (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
qed
lemma compact_ereal:
@@ -711,37 +624,17 @@
by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
lemma SUP_Lim_ereal:
- fixes X :: "nat \<Rightarrow> ereal"
- assumes "incseq X" "X ----> l"
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+ assumes inc: "incseq X" and l: "X ----> l"
shows "(SUP n. X n) = l"
-proof (rule ereal_SUPI)
- fix n from assms show "X n \<le> l"
- by (intro incseq_le_ereal) (simp add: incseq_def)
-next
- fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
- with ereal_Sup_lim[OF _ `X ----> l`, of "{..y}"] show "l \<le> y" by auto
-qed
-
-lemma LIMSEQ_ereal_SUPR:
- fixes X :: "nat \<Rightarrow> ereal"
- assumes "incseq X"
- shows "X ----> (SUP n. X n)"
-proof (rule lim_ereal_increasing)
- fix n m :: nat
- assume "m \<le> n"
- then show "X m \<le> X n" using `incseq X` by (simp add: incseq_def)
-next
- fix l
- assume "X ----> l"
- with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simp
-qed
+ using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
- using LIMSEQ_ereal_SUPR[of "\<lambda>i. - X i"]
+ using LIMSEQ_SUP[of "\<lambda>i. - X i"]
by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
lemma SUP_eq_LIMSEQ:
@@ -755,165 +648,66 @@
from SUP_Lim_ereal[OF inc this]
show "(SUP n. ereal (f n)) = ereal x" . }
{ assume "(SUP n. ereal (f n)) = ereal x"
- with LIMSEQ_ereal_SUPR[OF inc]
+ with LIMSEQ_SUP[OF inc]
show "f ----> x" by auto }
qed
lemma Liminf_within:
- fixes f :: "'a::metric_space => ereal"
- shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
-proof -
- let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
- { fix T
- assume T_def: "open T & mono_set T & ?l:T"
- have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
- proof -
- { assume "T=UNIV" then have ?thesis by (simp add: gt_ex) }
- moreover
- { assume "~(T=UNIV)"
- then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto
- then have "B<?l" using T_def by auto
- then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
- unfolding less_SUP_iff by auto
- { fix y assume "y:S & 0 < dist y x & dist y x < d"
- then have "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
- then have "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
- } then have ?thesis apply(rule_tac x="d" in exI) using d_def by auto
- }
- ultimately show ?thesis by auto
- qed
- }
- moreover
- { fix z
- assume a: "ALL T. open T --> mono_set T --> z : T -->
- (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
- { fix B
- assume "B<z"
- then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
- using a[rule_format, of "{B<..}"] mono_greaterThan by auto
- { fix y
- assume "y:(S Int ball x d - {x})"
- then have "y:S & 0 < dist y x & dist y x < d"
- unfolding ball_def
- apply (simp add: dist_commute)
- apply (metis dist_eq_0_iff less_le zero_le_dist)
- done
- then have "B <= f y" using d_def by auto
- }
- then have "B <= INFI (S Int ball x d - {x}) f"
- apply (subst INF_greatest)
- apply auto
- done
- also have "...<=?l"
- apply (subst SUP_upper)
- using d_def apply auto
- done
- finally have "B<=?l" by auto
- }
- then have "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
- }
- ultimately show ?thesis
- unfolding ereal_Liminf_Sup_monoset eventually_within
- apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"])
- apply auto
- done
+ 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 => ereal"
- shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
-proof -
- let ?l = "(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
- { fix T
- assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
- have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
- proof -
- { assume "T = UNIV"
- then have ?thesis by (simp add: gt_ex) }
- moreover
- { assume "T \<noteq> UNIV"
- then have "~(uminus ` T = UNIV)"
- by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV)
- then have "uminus ` T = {Inf (uminus ` T)<..}"
- using T_def ereal_open_mono_set[of "uminus ` T"] ereal_open_uminus[of T] by auto
- then obtain B where "T={..<B}"
- unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric]
- unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp
- then have "?l<B" using T_def by auto
- then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
- unfolding INF_less_iff by auto
- { fix y
- assume "y:S & 0 < dist y x & dist y x < d"
- then have "y:(S Int ball x d - {x})"
- unfolding ball_def by (auto simp add: dist_commute)
- then have "f y:T"
- using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
- }
- then have ?thesis
- apply (rule_tac x="d" in exI)
- using d_def apply auto
- done
- }
- ultimately show ?thesis by auto
- qed
- }
- moreover
- { fix z
- assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
- (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
- { fix B
- assume "z<B"
- then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
- using a[rule_format, of "{..<B}"] by auto
- { fix y
- assume "y:(S Int ball x d - {x})"
- then have "y:S & 0 < dist y x & dist y x < d"
- unfolding ball_def
- apply (simp add: dist_commute)
- apply (metis dist_eq_0_iff less_le zero_le_dist)
- done
- then have "f y <= B" using d_def by auto
- }
- then have "SUPR (S Int ball x d - {x}) f <= B"
- apply (subst SUP_least)
- apply auto
- done
- moreover
- have "?l<=SUPR (S Int ball x d - {x}) f"
- apply (subst INF_lower)
- using d_def apply auto
- done
- ultimately have "?l<=B" by auto
- } then have "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
- }
- ultimately show ?thesis
- unfolding ereal_Limsup_Inf_monoset eventually_within
- apply (subst ereal_InfI)
- apply auto
- done
+ 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 => ereal"
+ 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 => ereal"
+ 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 => ereal"
+ 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 => ereal"
+ 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
@@ -1295,7 +1089,7 @@
proof -
have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
- from LIMSEQ_ereal_SUPR[OF this]
+ from LIMSEQ_SUP[OF this]
show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
qed
--- a/src/HOL/Probability/Discrete_Topology.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy Thu Jan 31 11:31:30 2013 +0100
@@ -3,7 +3,7 @@
*)
theory Discrete_Topology
-imports Multivariate_Analysis
+imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin
text {* Copy of discrete types with discrete topology. This space is polish. *}
--- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Jan 31 11:31:30 2013 +0100
@@ -297,7 +297,7 @@
qed
next
fix x show "(SUP i. ?g i x) = max 0 (u x)"
- proof (rule ereal_SUPI)
+ proof (rule SUP_eqI)
fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
mult_nonpos_nonneg mult_nonneg_nonneg)
@@ -2147,7 +2147,7 @@
assume neq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
have "0 = limsup (\<lambda>n. 0 :: ereal)" by (simp add: Limsup_const)
also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
- by (intro limsup_mono positive_integral_positive)
+ by (simp add: Limsup_mono positive_integral_positive)
finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)" .
have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (ereal (?diff n x))) \<partial>M)"
using u'
@@ -2178,11 +2178,11 @@
qed
have "liminf ?f \<le> limsup ?f"
- by (intro ereal_Liminf_le_Limsup trivial_limit_sequentially)
+ by (intro Liminf_le_Limsup trivial_limit_sequentially)
moreover
{ have "0 = liminf (\<lambda>n. 0 :: ereal)" by (simp add: Liminf_const)
also have "\<dots> \<le> liminf ?f"
- by (intro liminf_mono positive_integral_positive)
+ by (simp add: Liminf_mono positive_integral_positive)
finally have "0 \<le> liminf ?f" . }
ultimately have liminf_limsup_eq: "liminf ?f = ereal 0" "limsup ?f = ereal 0"
using `limsup ?f = 0` by auto
--- a/src/HOL/Probability/Lebesgue_Measure.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Thu Jan 31 11:31:30 2013 +0100
@@ -698,7 +698,7 @@
have "integral\<^isup>P lebesgue f = ereal (integral UNIV f')"
proof (rule tendsto_unique[OF trivial_limit_sequentially])
have "(\<lambda>i. integral\<^isup>S lebesgue (u i)) ----> (SUP i. integral\<^isup>P lebesgue (u i))"
- unfolding u_eq by (intro LIMSEQ_ereal_SUPR incseq_positive_integral u)
+ unfolding u_eq by (intro LIMSEQ_SUP incseq_positive_integral u)
also note positive_integral_monotone_convergence_SUP
[OF u(2) borel_measurable_simple_function[OF u(1)] u(5), symmetric]
finally show "(\<lambda>k. integral\<^isup>S lebesgue (u k)) ----> integral\<^isup>P lebesgue f"
--- a/src/HOL/Probability/Measure_Space.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Thu Jan 31 11:31:30 2013 +0100
@@ -50,7 +50,7 @@
then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
by (auto simp: setsum_cases)
moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
- proof (rule ereal_SUPI)
+ proof (rule SUP_eqI)
fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
from this[of "Suc i"] show "f i \<le> y" by auto
qed (insert assms, simp)
@@ -523,7 +523,7 @@
lemma SUP_emeasure_incseq:
assumes A: "range A \<subseteq> sets M" "incseq A"
shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
- using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
+ using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
by (simp add: LIMSEQ_unique)
lemma decseq_emeasure:
@@ -1570,7 +1570,7 @@
have "incseq (\<lambda>i. ?M (F i))"
using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
- by (rule LIMSEQ_ereal_SUPR)
+ by (rule LIMSEQ_SUP)
moreover have "(SUP n. ?M (F n)) = \<infinity>"
proof (rule SUP_PInfty)
--- a/src/HOL/Probability/Regularity.thy Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy Thu Jan 31 11:31:30 2013 +0100
@@ -16,7 +16,7 @@
assumes f_nonneg: "\<And>i. 0 \<le> f i"
assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
shows "x = (SUP i : A. f i)"
-proof (subst eq_commute, rule ereal_SUPI)
+proof (subst eq_commute, rule SUP_eqI)
show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
@@ -45,7 +45,7 @@
assumes f_nonneg: "\<And>i. 0 \<le> f i"
assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
shows "x = (INF i : A. f i)"
-proof (subst eq_commute, rule ereal_INFI)
+proof (subst eq_commute, rule INF_eqI)
show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
@@ -79,7 +79,7 @@
from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
ultimately
have "(INF i : A. f i) = x + e" using `e > 0`
- by (intro ereal_INFI)
+ by (intro INF_eqI)
(force, metis add.comm_neutral add_left_mono ereal_less(1)
linorder_not_le not_less_iff_gr_or_eq)
thus False using assms by auto
@@ -97,7 +97,7 @@
from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
ultimately
have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
- by (intro ereal_SUPI)
+ by (intro SUP_eqI)
(metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
thus False using assms by auto
@@ -290,7 +290,7 @@
have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
ultimately show ?thesis by simp
- qed (auto intro!: ereal_INFI)
+ qed (auto intro!: INF_eqI)
note `?inner A` `?outer A` }
note closed_in_D = this
from `B \<in> sets borel`
@@ -299,8 +299,8 @@
then show "?inner B" "?outer B"
proof (induct B rule: sigma_sets_induct_disjoint)
case empty
- { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
- { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
+ { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
+ { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
next
case (basic B)
{ case 1 from basic closed_in_D show ?case by auto }