--- a/src/HOL/Conditionally_Complete_Lattices.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Jan 27 16:12:40 2015 +0100
@@ -102,15 +102,25 @@
lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
by (rule bdd_belowI[of _ bot]) simp
-lemma bdd_above_uminus[simp]:
- fixes X :: "'a::ordered_ab_group_add set"
- shows "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
- by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
+lemma bdd_above_image_mono: "mono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_above (f`A)"
+ by (auto simp: bdd_above_def mono_def)
+
+lemma bdd_below_image_mono: "mono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_below (f`A)"
+ by (auto simp: bdd_below_def mono_def)
+
+lemma bdd_above_image_antimono: "antimono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_above (f`A)"
+ by (auto simp: bdd_above_def bdd_below_def antimono_def)
-lemma bdd_below_uminus[simp]:
+lemma bdd_below_image_antimono: "antimono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below (f`A)"
+ by (auto simp: bdd_above_def bdd_below_def antimono_def)
+
+lemma
fixes X :: "'a::ordered_ab_group_add set"
- shows"bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
- by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
+ shows bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
+ and bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
+ using bdd_above_image_antimono[of uminus X] bdd_below_image_antimono[of uminus "uminus`X"]
+ using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"]
+ by (auto simp: antimono_def image_image)
context lattice
begin
--- a/src/HOL/Library/Extended_Real.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Jan 27 16:12:40 2015 +0100
@@ -568,6 +568,9 @@
lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
+lemma ereal_less_uminus_reorder: "a < - b \<longleftrightarrow> b < - (a::ereal)"
+ by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
+
lemma ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (a::ereal)"
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus)
@@ -1605,39 +1608,142 @@
show "\<exists>a b::ereal. a \<noteq> b"
using zero_neq_one by blast
qed
+subsubsection "Topological space"
+
+instantiation ereal :: linear_continuum_topology
+begin
+
+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 tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
+ apply (rule tendsto_compose[where g=ereal])
+ apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+ apply (rule_tac x="case a of MInfty \<Rightarrow> UNIV | ereal x \<Rightarrow> {x <..} | PInfty \<Rightarrow> {}" in exI)
+ apply (auto split: ereal.split) []
+ apply (rule_tac x="case a of MInfty \<Rightarrow> {} | ereal x \<Rightarrow> {..< x} | PInfty \<Rightarrow> UNIV" in exI)
+ apply (auto split: ereal.split) []
+ done
+
+lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) ---> - x) F"
+ apply (rule tendsto_compose[where g=uminus])
+ apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+ apply (rule_tac x="{..< -a}" in exI)
+ apply (auto split: ereal.split simp: ereal_less_uminus_reorder) []
+ apply (rule_tac x="{- a <..}" in exI)
+ apply (auto split: ereal.split simp: ereal_uminus_reorder) []
+ done
+
+lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
+ using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
+ by auto
+
+lemma ereal_divide_less_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a / c < b \<longleftrightarrow> a < b * c"
+ by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
+
+lemma ereal_less_divide_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b"
+ by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
+
+lemma tendsto_cmult_ereal[tendsto_intros, simp, intro]:
+ assumes c: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+proof -
+ { fix c :: ereal assume "0 < c" "c < \<infinity>"
+ then have "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+ apply (intro tendsto_compose[OF _ f])
+ apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+ apply (rule_tac x="{a/c <..}" in exI)
+ apply (auto split: ereal.split simp: ereal_divide_less_iff mult.commute) []
+ apply (rule_tac x="{..< a/c}" in exI)
+ apply (auto split: ereal.split simp: ereal_less_divide_iff mult.commute) []
+ done }
+ note * = this
+
+ have "((0 < c \<and> c < \<infinity>) \<or> (-\<infinity> < c \<and> c < 0) \<or> c = 0)"
+ using c by (cases c) auto
+ then show ?thesis
+ proof (elim disjE conjE)
+ assume "- \<infinity> < c" "c < 0"
+ then have "0 < - c" "- c < \<infinity>"
+ by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
+ then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F"
+ by (rule *)
+ from tendsto_uminus_ereal[OF this] show ?thesis
+ by simp
+ qed (auto intro!: *)
+qed
+
+lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]:
+ assumes "x \<noteq> 0" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+proof cases
+ assume "\<bar>c\<bar> = \<infinity>"
+ show ?thesis
+ proof (rule filterlim_cong[THEN iffD1, OF refl refl _ tendsto_const])
+ have "0 < x \<or> x < 0"
+ using `x \<noteq> 0` by (auto simp add: neq_iff)
+ then show "eventually (\<lambda>x'. c * x = c * f x') F"
+ proof
+ assume "0 < x" from order_tendstoD(1)[OF f this] show ?thesis
+ by eventually_elim (insert `0<x` `\<bar>c\<bar> = \<infinity>`, auto)
+ next
+ assume "x < 0" from order_tendstoD(2)[OF f this] show ?thesis
+ by eventually_elim (insert `x<0` `\<bar>c\<bar> = \<infinity>`, auto)
+ qed
+ qed
+qed (rule tendsto_cmult_ereal[OF _ f])
+
+lemma tendsto_cadd_ereal[tendsto_intros, simp, intro]:
+ assumes c: "y \<noteq> - \<infinity>" "x \<noteq> - \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
+ apply (intro tendsto_compose[OF _ f])
+ apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+ apply (rule_tac x="{a - y <..}" in exI)
+ apply (auto split: ereal.split simp: ereal_minus_less_iff c) []
+ apply (rule_tac x="{..< a - y}" in exI)
+ apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
+ done
+
+lemma tendsto_add_left_ereal[tendsto_intros, simp, intro]:
+ assumes c: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
+ apply (intro tendsto_compose[OF _ f])
+ apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+ apply (rule_tac x="{a - y <..}" in exI)
+ apply (insert c, auto split: ereal.split simp: ereal_minus_less_iff) []
+ apply (rule_tac x="{..< a - y}" in exI)
+ apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
+ done
+
+lemma continuous_at_ereal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ereal (f x))"
+ unfolding continuous_def by auto
+
+lemma continuous_on_ereal[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. ereal (f x))"
+ unfolding continuous_on_def by auto
lemma ereal_Sup:
assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
shows "ereal (Sup A) = (SUP a:A. ereal a)"
-proof (rule antisym)
+proof (rule continuous_at_Sup_mono)
obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
using * by (force simp: bot_ereal_def)
- then have upper: "\<And>a. a \<in> A \<Longrightarrow> a \<le> r"
- by (auto intro!: SUP_upper simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
-
- show "ereal (Sup A) \<le> (SUP a:A. ereal a)"
- using upper by (simp add: r[symmetric] cSup_least[OF `A \<noteq> {}`])
- show "(SUP a:A. ereal a) \<le> ereal (Sup A)"
- using upper `A \<noteq> {}` by (intro SUP_least) (auto intro!: cSup_upper bdd_aboveI)
-qed
+ then show "bdd_above A" "A \<noteq> {}"
+ by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
using ereal_Sup[of "f`A"] by auto
-
+
lemma ereal_Inf:
assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
shows "ereal (Inf A) = (INF a:A. ereal a)"
-proof (rule antisym)
+proof (rule continuous_at_Inf_mono)
obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
using * by (force simp: top_ereal_def)
- then have lower: "\<And>a. a \<in> A \<Longrightarrow> r \<le> a"
- by (auto intro!: INF_lower simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
-
- show "(INF a:A. ereal a) \<le> ereal (Inf A)"
- using lower by (simp add: r[symmetric] cInf_greatest[OF `A \<noteq> {}`])
- show "ereal (Inf A) \<le> (INF a:A. ereal a)"
- using lower `A \<noteq> {}` by (intro INF_greatest) (auto intro!: cInf_lower bdd_belowI)
-qed
+ then show "bdd_below A" "A \<noteq> {}"
+ by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
using ereal_Inf[of "f`A"] by auto
@@ -1660,9 +1766,15 @@
lemma ereal_INF_uminus_eq:
fixes f :: "'a \<Rightarrow> ereal"
- shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)"
+ shows "(INF x:S. - f x) = - (SUP x:S. f x)"
using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
+lemma ereal_SUP_uminus:
+ fixes f :: "'a \<Rightarrow> ereal"
+ shows "(SUP i : R. - f i) = - (INF i : R. f i)"
+ using ereal_Sup_uminus_image_eq[of "f`R"]
+ by (simp add: image_image)
+
lemma ereal_SUP_not_infty:
fixes f :: "_ \<Rightarrow> ereal"
shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPREMUM A f\<bar> \<noteq> \<infinity>"
@@ -1675,17 +1787,6 @@
using INF_lower2[of _ A f u] INF_greatest[of A l f]
by (cases "INFIMUM A f") auto
-lemma ereal_SUP_uminus:
- fixes f :: "'a \<Rightarrow> ereal"
- shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
- using ereal_Sup_uminus_image_eq[of "f`R"]
- by (simp add: image_image)
-
-lemma ereal_INF_uminus:
- fixes f :: "'a \<Rightarrow> ereal"
- shows "(INF i : R. - f i) = - (SUP i : R. f i)"
- using ereal_SUP_uminus [of _ "\<lambda>x. - f x"] by simp
-
lemma ereal_image_uminus_shift:
fixes X Y :: "ereal set"
shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
@@ -1697,12 +1798,6 @@
by (simp add: image_image)
qed (simp add: image_image)
-lemma Inf_ereal_iff:
- fixes z :: ereal
- shows "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x < y) \<longleftrightarrow> Inf X < y"
- by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower
- less_le_not_le linear order_less_le_trans)
-
lemma Sup_eq_MInfty:
fixes S :: "ereal set"
shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
@@ -1742,101 +1837,108 @@
qed
lemma SUP_PInfty:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
- shows "(SUP i:A. f i) = \<infinity>"
- unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
- apply simp
-proof safe
- fix x :: ereal
- assume "x \<noteq> \<infinity>"
- show "\<exists>i\<in>A. x < f i"
- proof (cases x)
- case PInf
- with `x \<noteq> \<infinity>` show ?thesis
- by simp
- next
- case MInf
- with assms[of "0"] show ?thesis
- by force
- next
- case (real r)
- with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
- by auto
- moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
- using assms ..
- ultimately show ?thesis
- by (auto intro!: bexI[of _ i])
- qed
-qed
+ "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i:A. f i :: ereal) = \<infinity>"
+ unfolding top_ereal_def[symmetric] SUP_eq_top_iff
+ by (metis MInfty_neq_PInfty(2) PInfty_neq_ereal(2) less_PInf_Ex_of_nat less_ereal.elims(2) less_le_trans)
lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
by (rule SUP_PInfty) auto
-lemma Inf_less:
- fixes x :: ereal
- assumes "(INF i:A. f i) < x"
- shows "\<exists>i. i \<in> A \<and> f i \<le> x"
-proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "\<forall>i\<in>A. f i > x"
- by auto
- then have "(INF i:A. f i) \<ge> x"
- by (subst INF_greatest) auto
- then show False
- using assms by auto
+lemma SUP_ereal_add_left:
+ assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
+ shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
+proof cases
+ assume "(SUP i:I. f i) = - \<infinity>"
+ moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
+ unfolding Sup_eq_MInfty Sup_image_eq[symmetric] by auto
+ ultimately show ?thesis
+ by (cases c) (auto simp: `I \<noteq> {}`)
+next
+ assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
+ unfolding Sup_image_eq[symmetric]
+ by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
+ (auto simp: continuous_at_within continuous_at mono_def ereal_add_mono `I \<noteq> {}` `c \<noteq> -\<infinity>`)
+qed
+
+lemma SUP_ereal_add_right:
+ fixes c :: ereal
+ shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)"
+ using SUP_ereal_add_left[of I c f] by (simp add: add.commute)
+
+lemma SUP_ereal_minus_right:
+ assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
+ shows "(SUP i:I. c - f i :: ereal) = c - (INF i:I. f i)"
+ using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
+ by (simp add: ereal_SUP_uminus minus_ereal_def)
+
+lemma SUP_ereal_minus_left:
+ assumes "I \<noteq> {}" "c \<noteq> \<infinity>"
+ shows "(SUP i:I. f i - c:: ereal) = (SUP i:I. f i) - c"
+ using SUP_ereal_add_left[OF `I \<noteq> {}`, of "-c" f] by (simp add: `c \<noteq> \<infinity>` minus_ereal_def)
+
+lemma INF_ereal_minus_right:
+ assumes "I \<noteq> {}" and "\<bar>c\<bar> \<noteq> \<infinity>"
+ shows "(INF i:I. c - f i) = c - (SUP i:I. f i::ereal)"
+proof -
+ { fix b have "(-c) + b = - (c - b)"
+ using `\<bar>c\<bar> \<noteq> \<infinity>` by (cases c b rule: ereal2_cases) auto }
+ note * = this
+ show ?thesis
+ using SUP_ereal_add_right[OF `I \<noteq> {}`, of "-c" f] `\<bar>c\<bar> \<noteq> \<infinity>`
+ by (auto simp add: * ereal_SUP_uminus_eq)
qed
lemma SUP_ereal_le_addI:
fixes f :: "'i \<Rightarrow> ereal"
- assumes "\<And>i. f i + y \<le> z"
- and "y \<noteq> -\<infinity>"
+ assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
shows "SUPREMUM UNIV f + y \<le> z"
-proof (cases y)
- case (real r)
- then have "\<And>i. f i \<le> z - y"
- using assms by (simp add: ereal_le_minus_iff)
- then have "SUPREMUM UNIV f \<le> z - y"
- by (rule SUP_least)
- then show ?thesis
- using real by (simp add: ereal_le_minus_iff)
-qed (insert assms, auto)
+ unfolding SUP_ereal_add_left[OF UNIV_not_empty `y \<noteq> -\<infinity>`, symmetric]
+ by (rule SUP_least assms)+
+
+lemma SUP_combine:
+ fixes f :: "'a::semilattice_sup \<Rightarrow> 'a::semilattice_sup \<Rightarrow> 'b::complete_lattice"
+ assumes mono: "\<And>a b c d. a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> f a c \<le> f b d"
+ shows "(SUP i:UNIV. SUP j:UNIV. f i j) = (SUP i. f i i)"
+proof (rule antisym)
+ show "(SUP i j. f i j) \<le> (SUP i. f i i)"
+ by (rule SUP_least SUP_upper2[where i="sup i j" for i j] UNIV_I mono sup_ge1 sup_ge2)+
+ show "(SUP i. f i i) \<le> (SUP i j. f i j)"
+ by (rule SUP_least SUP_upper2 UNIV_I mono order_refl)+
+qed
lemma SUP_ereal_add:
fixes f g :: "nat \<Rightarrow> ereal"
- assumes "incseq f"
- and "incseq g"
+ assumes inc: "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) = SUPREMUM UNIV f + SUPREMUM UNIV g"
-proof (rule SUP_eqI)
- fix y
- assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
- have f: "SUPREMUM UNIV f \<noteq> -\<infinity>"
- using pos
- unfolding SUP_def Sup_eq_MInfty
- by (auto dest: image_eqD)
- {
- fix j
- {
- fix i
- have "f i + g j \<le> f i + g (max i j)"
- using `incseq g`[THEN incseqD]
- by (rule add_left_mono) auto
- also have "\<dots> \<le> f (max i j) + g (max i j)"
- using `incseq f`[THEN incseqD]
- by (rule add_right_mono) auto
- also have "\<dots> \<le> y" using * by auto
- finally have "f i + g j \<le> y" .
- }
- then have "SUPREMUM UNIV f + g j \<le> y"
- using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
- then have "g j + SUPREMUM UNIV f \<le> y" by (simp add: ac_simps)
- }
- then have "SUPREMUM UNIV g + SUPREMUM UNIV f \<le> y"
- using f by (rule SUP_ereal_le_addI)
- then show "SUPREMUM UNIV f + SUPREMUM UNIV g \<le> y"
- by (simp add: ac_simps)
-qed (auto intro!: add_mono SUP_upper)
+ apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty])
+ apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
+ apply (subst (2) add.commute)
+ apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)])
+ apply (subst (2) add.commute)
+ apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+
+ done
+
+lemma INF_ereal_add:
+ fixes f :: "nat \<Rightarrow> ereal"
+ assumes "decseq f" "decseq g"
+ and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
+ shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
+proof -
+ have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
+ using assms unfolding INF_less_iff by auto
+ { fix a b :: ereal assume "a \<noteq> \<infinity>" "b \<noteq> \<infinity>"
+ then have "- ((- a) + (- b)) = a + b"
+ by (cases a b rule: ereal2_cases) auto }
+ note * = this
+ have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
+ by (simp add: fin *)
+ also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
+ unfolding ereal_INF_uminus_eq
+ using assms INF_less
+ by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus fin *)
+ finally show ?thesis .
+qed
lemma SUP_ereal_add_pos:
fixes f g :: "nat \<Rightarrow> ereal"
@@ -1863,313 +1965,85 @@
then show ?thesis by simp
qed
-lemma SUP_ereal_cmult:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- and "0 \<le> c"
- shows "(SUP i. c * f i) = c * SUPREMUM UNIV f"
-proof (rule SUP_eqI)
- fix i
- have "f i \<le> SUPREMUM UNIV f"
- by (rule SUP_upper) auto
- then show "c * f i \<le> c * SUPREMUM UNIV f"
- using `0 \<le> c` by (rule ereal_mult_left_mono)
-next
- fix y
- assume "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
- then have *: "\<And>i. c * f i \<le> y" by simp
- show "c * SUPREMUM UNIV f \<le> y"
- proof (cases "0 < c \<and> c \<noteq> \<infinity>")
- case True
- with * have "SUPREMUM UNIV f \<le> y / c"
- by (intro SUP_least) (auto simp: ereal_le_divide_pos)
- with True show ?thesis
- by (auto simp: ereal_le_divide_pos)
- next
- case False
- {
- assume "c = \<infinity>"
- have ?thesis
- proof (cases "\<forall>i. f i = 0")
- case True
- then have "range f = {0}"
- by auto
- with True show "c * SUPREMUM UNIV f \<le> y"
- using * by auto
- next
- case False
- then obtain i where "f i \<noteq> 0"
- by auto
- with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis
- by (auto split: split_if_asm)
- qed
- }
- moreover note False
- ultimately show ?thesis
- using * `0 \<le> c` by auto
- qed
-qed
-
-lemma SUP_ereal_mult_right:
+lemma SUP_ereal_mult_left:
fixes f :: "'a \<Rightarrow> ereal"
assumes "I \<noteq> {}"
- assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
- and "0 \<le> c"
+ assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
-proof (rule SUP_eqI)
- fix i assume "i \<in> I"
- then have "f i \<le> SUPREMUM I f"
- by (rule SUP_upper)
- then show "c * f i \<le> c * SUPREMUM I f"
- using `0 \<le> c` by (rule ereal_mult_left_mono)
+proof cases
+ assume "(SUP i:I. f i) = 0"
+ moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
+ by (metis SUP_upper f antisym)
+ ultimately show ?thesis
+ by simp
next
- fix y assume *: "\<And>i. i \<in> I \<Longrightarrow> c * f i \<le> y"
- { assume "c = \<infinity>" have "c * SUPREMUM I f \<le> y"
- proof cases
- assume "\<forall>i\<in>I. f i = 0"
- then show ?thesis
- using * `c = \<infinity>` by (auto simp: SUP_constant bot_ereal_def)
- next
- assume "\<not> (\<forall>i\<in>I. f i = 0)"
- then obtain i where "f i \<noteq> 0" "i \<in> I"
- by auto
- with *[of i] `c = \<infinity>` `i \<in> I \<Longrightarrow> 0 \<le> f i` show ?thesis
- by (auto split: split_if_asm)
- qed }
- moreover
- { assume "c \<noteq> 0" "c \<noteq> \<infinity>"
- moreover with `0 \<le> c` * have "SUPREMUM I f \<le> y / c"
- by (intro SUP_least) (auto simp: ereal_le_divide_pos)
- ultimately have "c * SUPREMUM I f \<le> y"
- using `0 \<le> c` * by (auto simp: ereal_le_divide_pos) }
- moreover { assume "c = 0" with * `I \<noteq> {}` have "c * SUPREMUM I f \<le> y" by auto }
- ultimately show "c * SUPREMUM I f \<le> y"
- by blast
+ assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
+ unfolding SUP_def
+ by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
+ (auto simp: mono_def continuous_at continuous_at_within `I \<noteq> {}`
+ intro!: ereal_mult_left_mono c)
qed
-lemma SUP_ereal_add_left:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes "I \<noteq> {}"
- assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
- and "0 \<le> c"
- shows "(SUP i:I. f i + c) = SUPREMUM I f + c"
-proof (intro SUP_eqI)
- fix B assume *: "\<And>i. i \<in> I \<Longrightarrow> f i + c \<le> B"
- show "SUPREMUM I f + c \<le> B"
- proof cases
- assume "c = \<infinity>" with `I \<noteq> {}` * show ?thesis
- by auto
- next
- assume "c \<noteq> \<infinity>"
- with `0 \<le> c` have [simp]: "\<bar>c\<bar> \<noteq> \<infinity>"
- by simp
- have "SUPREMUM I f \<le> B - c"
- by (simp add: SUP_le_iff ereal_le_minus *)
- then show ?thesis
- by (simp add: ereal_le_minus)
- qed
-qed (auto intro: ereal_add_mono SUP_upper)
-
-lemma SUP_ereal_add_right:
- fixes c :: ereal
- shows "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> 0 \<le> c \<Longrightarrow> (SUP i:I. c + f i) = c + SUPREMUM I f"
- using SUP_ereal_add_left[of I f c] by (simp add: add_ac)
+lemma countable_approach:
+ fixes x :: ereal
+ assumes "x \<noteq> -\<infinity>"
+ shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)"
+proof (cases x)
+ case (real r)
+ moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0"
+ by (intro tendsto_intros LIMSEQ_inverse_real_of_nat)
+ ultimately show ?thesis
+ by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def)
+next
+ case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis
+ by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty)
+qed (simp add: assms)
lemma Sup_countable_SUP:
assumes "A \<noteq> {}"
- shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
-proof (cases "Sup A")
- case (real r)
- have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
- proof
- fix n :: nat
- have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
- using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
- then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
- then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
- by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
- qed
- from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
- where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
- have "SUPREMUM UNIV f = Sup A"
- proof (rule SUP_eqI)
- fix i
- show "f i \<le> Sup A"
- using f by (auto intro!: complete_lattice_class.Sup_upper)
- next
- fix y
- assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
- show "Sup A \<le> y"
- proof (rule ereal_le_epsilon, intro allI impI)
- fix e :: ereal
- assume "0 < e"
- show "Sup A \<le> y + e"
- proof (cases e)
- case (real r)
- then have "0 < r"
- using `0 < e` by auto
- then obtain n :: nat where *: "1 / real n < r" "0 < n"
- using ex_inverse_of_nat_less
- by (auto simp: real_eq_of_nat inverse_eq_divide)
- have "Sup A \<le> f n + 1 / ereal (real n)"
- using f[THEN spec, of n]
- by auto
- also have "1 / ereal (real n) \<le> e"
- using real *
- by (auto simp: one_ereal_def )
- with bound have "f n + 1 / ereal (real n) \<le> y + e"
- by (rule add_mono) simp
- finally show "Sup A \<le> y + e" .
- qed (insert `0 < e`, auto)
- qed
- qed
- with f show ?thesis
- by (auto intro!: exI[of _ f])
-next
- case PInf
- from `A \<noteq> {}` obtain x where "x \<in> A"
- by auto
- show ?thesis
- proof (cases "\<infinity> \<in> A")
- case True
- then have "\<infinity> \<le> Sup A"
- by (intro complete_lattice_class.Sup_upper)
- with True show ?thesis
- by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
- next
- case False
- have "\<exists>x\<in>A. 0 \<le> x"
- by (metis Infty_neq_0(2) PInf complete_lattice_class.Sup_least ereal_infty_less_eq2(1) linorder_linear)
- then obtain x where "x \<in> A" and "0 \<le> x"
- by auto
- have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "\<exists>n::nat. Sup A \<le> x + ereal (real n)"
- by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
- then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
- by (cases x) auto
- qed
- from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
- where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
- have "SUPREMUM UNIV f = \<infinity>"
- proof (rule SUP_PInfty)
- fix n :: nat
- show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
- using f[THEN spec, of n] `0 \<le> x`
- by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
- qed
- then show ?thesis
- using f PInf by (auto intro!: exI[of _ f])
- qed
-next
- case MInf
+ shows "\<exists>f::nat \<Rightarrow> ereal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
+proof cases
+ assume "Sup A = -\<infinity>"
with `A \<noteq> {}` have "A = {-\<infinity>}"
by (auto simp: Sup_eq_MInfty)
then show ?thesis
- using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
+ by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
+next
+ assume "Sup A \<noteq> -\<infinity>"
+ then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l ----> Sup A"
+ by (auto dest: countable_approach)
+
+ have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
+ proof (rule dependent_nat_choice)
+ show "\<exists>x. x \<in> A \<and> l 0 \<le> x"
+ using l[of 0] by (auto simp: less_Sup_iff)
+ next
+ fix x n assume "x \<in> A \<and> l n \<le> x"
+ moreover from l[of "Suc n"] obtain y where "y \<in> A" "l (Suc n) < y"
+ by (auto simp: less_Sup_iff)
+ ultimately show "\<exists>y. (y \<in> A \<and> l (Suc n) \<le> y) \<and> x \<le> y"
+ by (auto intro!: exI[of _ "max x y"] split: split_max)
+ qed
+ then guess f .. note f = this
+ then have "range f \<subseteq> A" "incseq f"
+ by (auto simp: incseq_Suc_iff)
+ moreover
+ have "(SUP i. f i) = Sup A"
+ proof (rule tendsto_unique)
+ show "f ----> (SUP i. f i)"
+ by (rule LIMSEQ_SUP `incseq f`)+
+ show "f ----> Sup A"
+ using l f
+ by (intro tendsto_sandwich[OF _ _ l_Sup tendsto_const])
+ (auto simp: Sup_upper)
+ qed simp
+ ultimately show ?thesis
+ by auto
qed
lemma SUP_countable_SUP:
"A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
- using Sup_countable_SUP [of "g`A"]
- by auto
-
-lemma Sup_ereal_cadd:
- fixes A :: "ereal set"
- assumes "A \<noteq> {}"
- and "a \<noteq> -\<infinity>"
- shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
-proof (rule antisym)
- have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
- by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
- then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
- show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
- proof (cases a)
- case PInf with `A \<noteq> {}`
- show ?thesis
- by (auto simp: image_constant max.absorb1)
- next
- case (real r)
- then have **: "op + (- a) ` op + a ` A = A"
- by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
- from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis
- unfolding **
- by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
- qed (insert `a \<noteq> -\<infinity>`, auto)
-qed
-
-lemma Sup_ereal_cminus:
- fixes A :: "ereal set"
- assumes "A \<noteq> {}"
- and "a \<noteq> -\<infinity>"
- shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
- using Sup_ereal_cadd [of "uminus ` A" a] assms
- unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
-
-lemma SUP_ereal_cminus:
- fixes f :: "'i \<Rightarrow> ereal"
- fixes A
- assumes "A \<noteq> {}"
- and "a \<noteq> -\<infinity>"
- shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
- using Sup_ereal_cminus[of "f`A" a] assms
- unfolding SUP_def INF_def image_image by auto
-
-lemma Inf_ereal_cminus:
- fixes A :: "ereal set"
- assumes "A \<noteq> {}"
- and "\<bar>a\<bar> \<noteq> \<infinity>"
- shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
-proof -
- {
- fix x
- have "-a - -x = -(a - x)"
- using assms by (cases x) auto
- } note * = this
- then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
- by (auto simp: image_image)
- with * show ?thesis
- using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
- by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
-qed
-
-lemma INF_ereal_cminus:
- fixes a :: ereal
- assumes "A \<noteq> {}"
- and "\<bar>a\<bar> \<noteq> \<infinity>"
- shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
- using Inf_ereal_cminus[of "f`A" a] assms
- unfolding SUP_def INF_def image_image
- by auto
-
-lemma uminus_ereal_add_uminus_uminus:
- fixes a b :: ereal
- shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
- by (cases rule: ereal2_cases[of a b]) auto
-
-lemma INF_ereal_add:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "decseq f" "decseq g"
- and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
- shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
-proof -
- have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
- using assms unfolding INF_less_iff by auto
- {
- fix i
- from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
- by (rule uminus_ereal_add_uminus_uminus)
- }
- then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
- by simp
- also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
- unfolding ereal_INF_uminus
- using assms INF_less
- by (subst SUP_ereal_add)
- (auto simp: ereal_SUP_uminus intro!: uminus_ereal_add_uminus_uminus)
- finally show ?thesis .
-qed
+ using Sup_countable_SUP [of "g`A"] by auto
subsection "Relation to @{typ enat}"
@@ -2225,19 +2099,6 @@
subsection "Limits on @{typ ereal}"
-subsubsection "Topological space"
-
-instantiation ereal :: linear_continuum_topology
-begin
-
-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_generated
proof (induct rule: generate_topology.induct)
@@ -2279,23 +2140,7 @@
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
- case (Basis S)
- {
- 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 note Basis
- ultimately show ?case
- by (auto split: ereal.split)
-qed (fastforce simp add: vimage_Union)+
+ by (intro open_vimage continuous_intros)
lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
unfolding open_generated_order[where 'a=real]
@@ -2422,23 +2267,6 @@
subsubsection {* Convergent sequences *}
-lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
- (is "?l = ?r")
-proof (intro iffI topological_tendstoI)
- fix S
- assume "?l" and "open S" and "x \<in> S"
- then show "eventually (\<lambda>x. f x \<in> S) net"
- using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
- by (simp add: inj_image_mem_iff)
-next
- fix S
- assume "?r" and "open S" and "ereal x \<in> S"
- show "eventually (\<lambda>x. ereal (f x) \<in> S) net"
- using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
- using `ereal x \<in> S`
- by auto
-qed
-
lemma lim_real_of_ereal[simp]:
assumes lim: "(f ---> ereal x) net"
shows "((\<lambda>x. real (f x)) ---> x) net"
@@ -2454,6 +2282,9 @@
by (rule eventually_mono)
qed
+lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
+ by (auto dest!: lim_real_of_ereal)
+
lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
proof -
{
@@ -2763,7 +2594,7 @@
lemma ereal_Limsup_uminus:
fixes f :: "'a \<Rightarrow> ereal"
shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
- unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus ..
+ unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus_eq ..
lemma liminf_bounded_iff:
fixes x :: "nat \<Rightarrow> ereal"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Jan 27 16:12:40 2015 +0100
@@ -250,71 +250,22 @@
and t: "\<bar>t\<bar> \<noteq> \<infinity>"
shows "open ((\<lambda>x. m * x + t) ` S)"
proof -
- obtain r where r[simp]: "m = ereal r"
- using m by (cases m) auto
- obtain p where p[simp]: "t = ereal p"
- using t by auto
- have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0"
- using m by auto
- from `open S` [THEN ereal_openE]
- obtain l u where T:
- "open (ereal -` S)"
- "\<infinity> \<in> S \<Longrightarrow> {ereal l<..} \<subseteq> S"
- "- \<infinity> \<in> S \<Longrightarrow> {..<ereal u} \<subseteq> S"
- by blast
- let ?f = "(\<lambda>x. m * x + t)"
- show ?thesis
- unfolding open_ereal_def
- proof (intro conjI impI exI subsetI)
- have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
- proof safe
- fix x y
- assume "ereal y = m * x + t" "x \<in> S"
- then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
- using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
- qed force
- then show "open (ereal -` ?f ` S)"
- using open_affinity[OF T(1) `r \<noteq> 0`]
- by (auto simp: ac_simps)
- next
- assume "\<infinity> \<in> ?f`S"
- with `0 < r` have "\<infinity> \<in> S"
- by auto
- fix x
- assume "x \<in> {ereal (r * l + p)<..}"
- then have [simp]: "ereal (r * l + p) < x"
- by auto
- show "x \<in> ?f`S"
- proof (rule image_eqI)
- show "x = m * ((x - t) / m) + t"
- using m t
- by (cases rule: ereal3_cases[of m x t]) auto
- have "ereal l < (x - t) / m"
- using m t
- by (simp add: ereal_less_divide_pos ereal_less_minus)
- then show "(x - t) / m \<in> S"
- using T(2)[OF `\<infinity> \<in> S`] by auto
- qed
- next
- assume "-\<infinity> \<in> ?f ` S"
- with `0 < r` have "-\<infinity> \<in> S"
- by auto
- fix x assume "x \<in> {..<ereal (r * u + p)}"
- then have [simp]: "x < ereal (r * u + p)"
- by auto
- show "x \<in> ?f`S"
- proof (rule image_eqI)
- show "x = m * ((x - t) / m) + t"
- using m t
- by (cases rule: ereal3_cases[of m x t]) auto
- have "(x - t)/m < ereal u"
- using m t
- by (simp add: ereal_divide_less_pos ereal_minus_less)
- then show "(x - t)/m \<in> S"
- using T(3)[OF `-\<infinity> \<in> S`]
- by auto
- qed
- qed
+ have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
+ using m t
+ apply (intro open_vimage `open S`)
+ apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
+ tendsto_ident_at tendsto_add_left_ereal)
+ apply auto
+ done
+ also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
+ using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
+ simp del: uminus_ereal.simps)
+ also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
+ using m t
+ by (simp add: set_eq_iff image_iff)
+ (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
+ ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
+ finally show ?thesis .
qed
lemma ereal_open_affinity:
@@ -340,45 +291,6 @@
unfolding image_image by simp
qed
-lemma ereal_lim_mult:
- fixes X :: "'a \<Rightarrow> ereal"
- assumes lim: "(X ---> L) net"
- and a: "\<bar>a\<bar> \<noteq> \<infinity>"
- shows "((\<lambda>i. a * X i) ---> a * L) net"
-proof cases
- assume "a \<noteq> 0"
- show ?thesis
- proof (rule topological_tendstoI)
- fix S
- assume "open S" and "a * L \<in> S"
- have "a * L / a = L"
- using `a \<noteq> 0` a
- by (cases rule: ereal2_cases[of a L]) auto
- then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
- using `a * L \<in> S`
- by (force simp: image_iff)
- moreover have "open ((\<lambda>x. x / a) ` S)"
- using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
- by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
- note * = lim[THEN topological_tendstoD, OF this L]
- {
- fix x
- from a `a \<noteq> 0` have "a * (x / a) = x"
- by (cases rule: ereal2_cases[of a x]) auto
- }
- note this[simp]
- show "eventually (\<lambda>x. a * X x \<in> S) net"
- by (rule eventually_mono[OF _ *]) auto
- qed
-qed auto
-
-lemma ereal_lim_uminus:
- fixes X :: "'a \<Rightarrow> ereal"
- shows "((\<lambda>i. - X i) ---> - L) net \<longleftrightarrow> (X ---> L) net"
- using ereal_lim_mult[of X L net "ereal (-1)"]
- ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
- by (auto simp add: algebra_simps)
-
lemma ereal_open_atLeast:
fixes x :: ereal
shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
@@ -409,14 +321,6 @@
shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
-lemma ereal_Lim_uminus:
- fixes f :: "'a \<Rightarrow> ereal"
- shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
- using
- ereal_lim_mult[of f f0 net "- 1"]
- ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
- by (auto simp: ereal_uminus_reorder)
-
lemma Liminf_PInfty:
fixes f :: "'a \<Rightarrow> ereal"
assumes "\<not> trivial_limit net"
@@ -559,9 +463,9 @@
case (real r)
then show ?thesis
unfolding liminf_SUP_INF limsup_INF_SUP
- apply (subst INF_ereal_cminus)
+ apply (subst INF_ereal_minus_right)
apply auto
- apply (subst SUP_ereal_cminus)
+ apply (subst SUP_ereal_minus_right)
apply auto
done
qed (insert `c \<noteq> -\<infinity>`, simp)
@@ -889,7 +793,7 @@
shows "(\<Sum>i. a * f i) = a * suminf f"
by (auto simp: setsum_ereal_right_distrib[symmetric] assms
ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
- intro!: SUP_ereal_cmult)
+ intro!: SUP_ereal_mult_left)
lemma suminf_PInfty:
fixes f :: "nat \<Rightarrow> ereal"
--- a/src/HOL/Probability/Bochner_Integration.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Tue Jan 27 16:12:40 2015 +0100
@@ -641,7 +641,7 @@
finally show "?f i \<le> ?g i" .
qed
show "?g ----> 0"
- using ereal_lim_mult[OF f_s, of "ereal K"] by simp
+ using tendsto_cmult_ereal[OF _ f_s, of "ereal K"] by simp
qed
assume "(\<lambda>i. simple_bochner_integral M (s i)) ----> x"
--- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy Tue Jan 27 16:12:40 2015 +0100
@@ -566,7 +566,7 @@
(auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
intro!: ereal_mult_right_mono)
also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
- by (subst mult.assoc, subst mult.commute, subst SUP_ereal_cmult)
+ by (subst mult.assoc, subst mult.commute, subst SUP_ereal_mult_left)
(auto split: split_indicator simp: derivg_nonneg mult_ac)
finally show ?case by simp
qed
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Jan 27 16:12:40 2015 +0100
@@ -944,11 +944,11 @@
next
show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
using measure_conv u_range B_u unfolding simple_integral_def
- by (auto intro!: setsum.cong SUP_ereal_cmult [symmetric])
+ by (auto intro!: setsum.cong SUP_ereal_mult_left [symmetric])
qed
moreover
have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
- apply (subst SUP_ereal_cmult [symmetric])
+ apply (subst SUP_ereal_mult_left [symmetric])
proof (safe intro!: SUP_mono bexI)
fix i
have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
@@ -1115,7 +1115,7 @@
by auto }
then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
- by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
+ by (subst SUP_ereal_mult_left [symmetric, OF _ u(6) `0 \<le> a`])
(auto intro!: SUP_ereal_add
simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono) }
then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
@@ -1127,8 +1127,10 @@
finally have "(\<integral>\<^sup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^sup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+x. max 0 (g x) \<partial>M)"
unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
- apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
- apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
+ apply (subst SUP_ereal_mult_left [symmetric, OF _ pos(1) `0 \<le> a`])
+ apply simp
+ apply (subst SUP_ereal_add [symmetric, OF inc not_MInf])
+ .
then show ?thesis by (simp add: nn_integral_max_0)
qed
@@ -2120,7 +2122,7 @@
next
case (seq U)
from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
- by eventually_elim (simp add: SUP_ereal_cmult seq)
+ by eventually_elim (simp add: SUP_ereal_mult_left seq)
from seq f show ?case
apply (simp add: nn_integral_monotone_convergence_SUP)
apply (subst nn_integral_cong_AE[OF eq])
--- a/src/HOL/Probability/Regularity.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Regularity.thy Tue Jan 27 16:12:40 2015 +0100
@@ -312,7 +312,7 @@
case 2
have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)"
- unfolding inner by (subst INF_ereal_cminus) force+
+ unfolding inner by (subst INF_ereal_minus_right) force+
also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
@@ -331,7 +331,7 @@
case 1
have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)"
- unfolding outer by (subst SUP_ereal_cminus) auto
+ unfolding outer by (subst SUP_ereal_minus_right) auto
also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
--- a/src/HOL/Topological_Spaces.thy Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Jan 27 16:12:40 2015 +0100
@@ -2789,6 +2789,154 @@
using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
qed
+lemma continuous_at_Sup_mono:
+ fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+ assumes "mono f"
+ assumes cont: "continuous (at_left (Sup S)) f"
+ assumes S: "S \<noteq> {}" "bdd_above S"
+ shows "f (Sup S) = (SUP s:S. f s)"
+proof (rule antisym)
+ have f: "(f ---> f (Sup S)) (at_left (Sup S))"
+ using cont unfolding continuous_within .
+
+ show "f (Sup S) \<le> (SUP s:S. f s)"
+ proof cases
+ assume "Sup S \<in> S" then show ?thesis
+ by (rule cSUP_upper) (auto intro: bdd_above_image_mono S `mono f`)
+ next
+ assume "Sup S \<notin> S"
+ from `S \<noteq> {}` obtain s where "s \<in> S"
+ by auto
+ with `Sup S \<notin> S` S have "s < Sup S"
+ unfolding less_le by (blast intro: cSup_upper)
+ show ?thesis
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "b < Sup S"
+ and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> (SUP s:S. f s) < f y"
+ by (auto simp: not_le eventually_at_left[OF `s < Sup S`])
+ with `S \<noteq> {}` obtain c where "c \<in> S" "b < c"
+ using less_cSupD[of S b] by auto
+ with `Sup S \<notin> S` S have "c < Sup S"
+ unfolding less_le by (blast intro: cSup_upper)
+ from *[OF `b < c` `c < Sup S`] cSUP_upper[OF `c \<in> S` bdd_above_image_mono[of f]]
+ show False
+ by (auto simp: assms)
+ qed
+ qed
+qed (intro cSUP_least `mono f`[THEN monoD] cSup_upper S)
+
+lemma continuous_at_Sup_antimono:
+ fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+ assumes "antimono f"
+ assumes cont: "continuous (at_left (Sup S)) f"
+ assumes S: "S \<noteq> {}" "bdd_above S"
+ shows "f (Sup S) = (INF s:S. f s)"
+proof (rule antisym)
+ have f: "(f ---> f (Sup S)) (at_left (Sup S))"
+ using cont unfolding continuous_within .
+
+ show "(INF s:S. f s) \<le> f (Sup S)"
+ proof cases
+ assume "Sup S \<in> S" then show ?thesis
+ by (intro cINF_lower) (auto intro: bdd_below_image_antimono S `antimono f`)
+ next
+ assume "Sup S \<notin> S"
+ from `S \<noteq> {}` obtain s where "s \<in> S"
+ by auto
+ with `Sup S \<notin> S` S have "s < Sup S"
+ unfolding less_le by (blast intro: cSup_upper)
+ show ?thesis
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "b < Sup S"
+ and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> f y < (INF s:S. f s)"
+ by (auto simp: not_le eventually_at_left[OF `s < Sup S`])
+ with `S \<noteq> {}` obtain c where "c \<in> S" "b < c"
+ using less_cSupD[of S b] by auto
+ with `Sup S \<notin> S` S have "c < Sup S"
+ unfolding less_le by (blast intro: cSup_upper)
+ from *[OF `b < c` `c < Sup S`] cINF_lower[OF bdd_below_image_antimono, of f S c] `c \<in> S`
+ show False
+ by (auto simp: assms)
+ qed
+ qed
+qed (intro cINF_greatest `antimono f`[THEN antimonoD] cSup_upper S)
+
+lemma continuous_at_Inf_mono:
+ fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+ assumes "mono f"
+ assumes cont: "continuous (at_right (Inf S)) f"
+ assumes S: "S \<noteq> {}" "bdd_below S"
+ shows "f (Inf S) = (INF s:S. f s)"
+proof (rule antisym)
+ have f: "(f ---> f (Inf S)) (at_right (Inf S))"
+ using cont unfolding continuous_within .
+
+ show "(INF s:S. f s) \<le> f (Inf S)"
+ proof cases
+ assume "Inf S \<in> S" then show ?thesis
+ by (rule cINF_lower[rotated]) (auto intro: bdd_below_image_mono S `mono f`)
+ next
+ assume "Inf S \<notin> S"
+ from `S \<noteq> {}` obtain s where "s \<in> S"
+ by auto
+ with `Inf S \<notin> S` S have "Inf S < s"
+ unfolding less_le by (blast intro: cInf_lower)
+ show ?thesis
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "Inf S < b"
+ and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> f y < (INF s:S. f s)"
+ by (auto simp: not_le eventually_at_right[OF `Inf S < s`])
+ with `S \<noteq> {}` obtain c where "c \<in> S" "c < b"
+ using cInf_lessD[of S b] by auto
+ with `Inf S \<notin> S` S have "Inf S < c"
+ unfolding less_le by (blast intro: cInf_lower)
+ from *[OF `Inf S < c` `c < b`] cINF_lower[OF bdd_below_image_mono[of f] `c \<in> S`]
+ show False
+ by (auto simp: assms)
+ qed
+ qed
+qed (intro cINF_greatest `mono f`[THEN monoD] cInf_lower `bdd_below S` `S \<noteq> {}`)
+
+lemma continuous_at_Inf_antimono:
+ fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+ assumes "antimono f"
+ assumes cont: "continuous (at_right (Inf S)) f"
+ assumes S: "S \<noteq> {}" "bdd_below S"
+ shows "f (Inf S) = (SUP s:S. f s)"
+proof (rule antisym)
+ have f: "(f ---> f (Inf S)) (at_right (Inf S))"
+ using cont unfolding continuous_within .
+
+ show "f (Inf S) \<le> (SUP s:S. f s)"
+ proof cases
+ assume "Inf S \<in> S" then show ?thesis
+ by (rule cSUP_upper) (auto intro: bdd_above_image_antimono S `antimono f`)
+ next
+ assume "Inf S \<notin> S"
+ from `S \<noteq> {}` obtain s where "s \<in> S"
+ by auto
+ with `Inf S \<notin> S` S have "Inf S < s"
+ unfolding less_le by (blast intro: cInf_lower)
+ show ?thesis
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "Inf S < b"
+ and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> (SUP s:S. f s) < f y"
+ by (auto simp: not_le eventually_at_right[OF `Inf S < s`])
+ with `S \<noteq> {}` obtain c where "c \<in> S" "c < b"
+ using cInf_lessD[of S b] by auto
+ with `Inf S \<notin> S` S have "Inf S < c"
+ unfolding less_le by (blast intro: cInf_lower)
+ from *[OF `Inf S < c` `c < b`] cSUP_upper[OF `c \<in> S` bdd_above_image_antimono[of f]]
+ show False
+ by (auto simp: assms)
+ qed
+ qed
+qed (intro cSUP_least `antimono f`[THEN antimonoD] cInf_lower S)
+
subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
context begin interpretation lifting_syntax .