# HG changeset patch # User hoelzl # Date 1360169841 -3600 # Node ID 78de6c7e8a583c65075f90a05086f5a62eff41c1 # Parent 1cf4faed8b220aa840ab56b825e68bbd5a5b2460 replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules diff -r 1cf4faed8b22 -r 78de6c7e8a58 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Wed Feb 06 17:18:01 2013 +0100 +++ b/src/HOL/Library/Extended_Real.thy Wed Feb 06 17:57:21 2013 +0100 @@ -11,6 +11,13 @@ imports "~~/src/HOL/Complex_Main" Extended_Nat begin +text {* + +For more lemmas about the extended real numbers go to + @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} + +*} + lemma LIMSEQ_SUP: fixes X :: "nat \ 'a :: {complete_linorder, linorder_topology}" assumes "incseq X" @@ -22,24 +29,37 @@ lemma eventually_const: "\ trivial_limit net \ eventually (\x. P) net \ P" by (cases P) (simp_all add: eventually_False) -lemma (in complete_lattice) Inf_le_Sup: - assumes "A \ {}" shows "Inf A \ Sup A" -proof - - from `A \ {}` obtain x where "x \ A" by auto - then show ?thesis - by (metis Sup_upper2 Inf_lower) -qed - -lemma (in complete_lattice) INF_le_SUP: - "A \ {} \ INFI A f \ SUPR A f" +lemma (in complete_lattice) Inf_le_Sup: "A \ {} \ Inf A \ Sup A" + by (metis Sup_upper2 Inf_lower ex_in_conv) + +lemma (in complete_lattice) INF_le_SUP: "A \ {} \ INFI A f \ 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 - @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} - -*} +lemma (in complete_linorder) le_Sup_iff: + "x \ Sup A \ (\ya\A. y < a)" +proof safe + fix y assume "x \ Sup A" "y < x" + then have "y < Sup A" by auto + then show "\a\A. y < a" + unfolding less_Sup_iff . +qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper) + +lemma (in complete_linorder) le_SUP_iff: + "x \ SUPR A f \ (\yi\A. y < f i)" + unfolding le_Sup_iff SUP_def by simp + +lemma (in complete_linorder) Inf_le_iff: + "Inf A \ x \ (\y>x. \a\A. y > a)" +proof safe + fix y assume "x \ Inf A" "y > x" + then have "y > Inf A" by auto + then show "\a\A. y > a" + unfolding Inf_less_iff . +qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower) + +lemma (in complete_linorder) le_INF_iff: + "INFI A f \ x \ (\y>x. \i\A. y > f i)" + unfolding Inf_le_iff INF_def by simp lemma (in complete_lattice) Sup_eqI: assumes "\y. y \ A \ y \ x" @@ -1429,8 +1449,7 @@ lemma ereal_le_Sup: fixes x :: ereal - shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" -(is "?lhs <-> ?rhs") + shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs") proof- { assume "?rhs" { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i) \) F \ (\r. eventually (\x. ereal r < f x) F)" - unfolding tendsto_def -proof safe - fix S :: "ereal set" assume "open S" "\ \ S" - from open_PInfty[OF this] guess B .. note B = this - moreover - assume "\r::real. eventually (\z. r < f z) F" - then have "eventually (\z. f z \ {B <..}) F" by auto - ultimately show "eventually (\z. f z \ S) F" by (auto elim!: eventually_elim1) -next - fix x assume "\S. open S \ \ \ S \ eventually (\x. f x \ S) F" - from this[rule_format, of "{ereal x <..}"] - show "eventually (\y. ereal x < f y) F" by auto +proof - + { fix l :: ereal assume "\r. eventually (\x. ereal r < f x) F" + from this[THEN spec, of "real l"] + have "l \ \ \ eventually (\x. l < f x) F" + by (cases l) (auto elim: eventually_elim1) } + then show ?thesis + by (auto simp: order_tendsto_iff) qed lemma tendsto_MInfty: "(f ---> -\) F \ (\r. eventually (\x. f x < ereal r) F)" @@ -2209,7 +2223,6 @@ "[| (a::ereal) <= x; c <= x |] ==> max a c <= x" by (metis sup_ereal_def sup_least) - lemma ereal_LimI_finite: fixes x :: ereal assumes "\x\ \ \" @@ -2403,25 +2416,142 @@ shows "Limsup F X \ C" using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp +lemma le_Liminf_iff: + fixes X :: "_ \ _ :: complete_linorder" + shows "C \ Liminf F X \ (\yx. y < X x) F)" +proof - + { fix y P assume "eventually P F" "y < INFI (Collect P) X" + then have "eventually (\x. y < X x) F" + by (auto elim!: eventually_elim1 dest: less_INF_D) } + moreover + { fix y P assume "y < C" and y: "\yx. y < X x) F" + have "\P. eventually P F \ y < INFI (Collect P) X" + proof cases + assume "\z. y < z \ z < C" + then guess z .. + moreover then have "z \ INFI {x. z < X x} X" + by (auto intro!: INF_greatest) + ultimately show ?thesis + using y by (intro exI[of _ "\x. z < X x"]) auto + next + assume "\ (\z. y < z \ z < C)" + then have "C \ INFI {x. y < X x} X" + by (intro INF_greatest) auto + with `y < C` show ?thesis + using y by (intro exI[of _ "\x. y < X x"]) auto + qed } + ultimately show ?thesis + unfolding Liminf_def le_SUP_iff by auto +qed + +lemma lim_imp_Liminf: + fixes f :: "'a \ _ :: {complete_linorder, linorder_topology}" + assumes ntriv: "\ trivial_limit F" + assumes lim: "(f ---> f0) F" + shows "Liminf F f = f0" +proof (intro Liminf_eqI) + fix P assume P: "eventually P F" + then have "eventually (\x. INFI (Collect P) f \ f x) F" + by eventually_elim (auto intro!: INF_lower) + then show "INFI (Collect P) f \ f0" + by (rule tendsto_le[OF ntriv lim tendsto_const]) +next + fix y assume upper: "\P. eventually P F \ INFI (Collect P) f \ y" + show "f0 \ y" + proof cases + assume "\z. y < z \ z < f0" + then guess z .. + moreover have "z \ INFI {x. z < f x} f" + by (rule INF_greatest) simp + ultimately show ?thesis + using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto + next + assume discrete: "\ (\z. y < z \ z < f0)" + show ?thesis + proof (rule classical) + assume "\ f0 \ y" + then have "eventually (\x. y < f x) F" + using lim[THEN topological_tendstoD, of "{y <..}"] by auto + then have "eventually (\x. f0 \ f x) F" + using discrete by (auto elim!: eventually_elim1) + then have "INFI {x. f0 \ f x} f \ y" + by (rule upper) + moreover have "f0 \ INFI {x. f0 \ f x} f" + by (intro INF_greatest) simp + ultimately show "f0 \ y" by simp + qed + qed +qed + +lemma lim_imp_Limsup: + fixes f :: "'a \ _ :: {complete_linorder, linorder_topology}" + assumes ntriv: "\ trivial_limit F" + assumes lim: "(f ---> f0) F" + shows "Limsup F f = f0" +proof (intro Limsup_eqI) + fix P assume P: "eventually P F" + then have "eventually (\x. f x \ SUPR (Collect P) f) F" + by eventually_elim (auto intro!: SUP_upper) + then show "f0 \ SUPR (Collect P) f" + by (rule tendsto_le[OF ntriv tendsto_const lim]) +next + fix y assume lower: "\P. eventually P F \ y \ SUPR (Collect P) f" + show "y \ f0" + proof cases + assume "\z. f0 < z \ z < y" + then guess z .. + moreover have "SUPR {x. f x < z} f \ z" + by (rule SUP_least) simp + ultimately show ?thesis + using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto + next + assume discrete: "\ (\z. f0 < z \ z < y)" + show ?thesis + proof (rule classical) + assume "\ y \ f0" + then have "eventually (\x. f x < y) F" + using lim[THEN topological_tendstoD, of "{..< y}"] by auto + then have "eventually (\x. f x \ f0) F" + using discrete by (auto elim!: eventually_elim1 simp: not_less) + then have "y \ SUPR {x. f x \ f0} f" + by (rule lower) + moreover have "SUPR {x. f x \ f0} f \ f0" + by (intro SUP_least) simp + ultimately show "y \ f0" by simp + qed + qed +qed + +lemma Liminf_eq_Limsup: + fixes f0 :: "'a :: {complete_linorder, linorder_topology}" + assumes ntriv: "\ trivial_limit F" + and lim: "Liminf F f = f0" "Limsup F f = f0" + shows "(f ---> f0) F" +proof (rule order_tendstoI) + fix a assume "f0 < a" + with assms have "Limsup F f < a" by simp + then obtain P where "eventually P F" "SUPR (Collect P) f < a" + unfolding Limsup_def INF_less_iff by auto + then show "eventually (\x. f x < a) F" + by (auto elim!: eventually_elim1 dest: SUP_lessD) +next + fix a assume "a < f0" + with assms have "a < Liminf F f" by simp + then obtain P where "eventually P F" "a < INFI (Collect P) f" + unfolding Liminf_def less_SUP_iff by auto + then show "eventually (\x. a < f x) F" + by (auto elim!: eventually_elim1 dest: less_INF_D) +qed + +lemma tendsto_iff_Liminf_eq_Limsup: + fixes f0 :: "'a :: {complete_linorder, linorder_topology}" + shows "\ trivial_limit F \ (f ---> f0) F \ (Liminf F f = f0 \ Limsup F f = f0)" + by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf) + lemma liminf_bounded_iff: fixes x :: "nat \ ereal" shows "C \ liminf x \ (\BN. \n\N. B < x n)" (is "?lhs <-> ?rhs") -proof safe - fix B assume "B < C" "C \ 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 "\N. \n\N. B < x n" by auto -next - assume *: "\BN. \n\N. B < x n" - { fix B assume "Bn\N. B < x n" using `?rhs` by auto - hence "B \ (INF m:{N..}. x m)" by (intro INF_greatest) auto - also have "... \ liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp - finally have "B \ liminf x" . - } then show "?lhs" - by (metis * leD Liminf_bounded[OF sequentially_bot] linorder_le_less_linear eventually_sequentially) -qed + unfolding le_Liminf_iff eventually_sequentially .. lemma liminf_subseq_mono: fixes X :: "nat \ 'a :: complete_linorder" @@ -2449,56 +2579,6 @@ then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def) qed -lemma lim_imp_Liminf: - fixes f :: "'a \ ereal" (* generalize to inner dense, complete_linorder, order_topology *) - assumes ntriv: "\ trivial_limit F" - assumes lim: "(f ---> f0) F" - shows "Liminf F f = f0" -proof (rule Liminf_eqI) - fix y assume *: "\P. eventually P F \ INFI (Collect P) f \ y" - show "f0 \ y" - proof (rule ereal_le_ereal) - fix B - assume "B < f0" - have "B \ INFI {x. B < f x} f" - by (rule INF_greatest) simp - also have "INFI {x. B < f x} f \ y" - using lim[THEN topological_tendstoD, of "{B <..}"] `B < f0` * by auto - finally show "B \ y" . - qed -next - fix P assume P: "eventually P F" - then have "eventually (\x. INFI (Collect P) f \ f x) F" - by eventually_elim (auto intro!: INF_lower) - then show "INFI (Collect P) f \ f0" - by (rule tendsto_le[OF ntriv lim tendsto_const]) -qed - -lemma lim_imp_Limsup: - fixes f :: "'a \ ereal" (* generalize to inner dense, complete_linorder, order_topology *) - assumes ntriv: "\ trivial_limit F" - assumes lim: "(f ---> f0) F" - shows "Limsup F f = f0" -proof (rule Limsup_eqI) - fix y assume *: "\P. eventually P F \ y \ SUPR (Collect P) f" - show "y \ f0" - proof (rule ereal_ge_ereal, safe) - fix B - assume "f0 < B" - have "y \ 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 \ B" - by (rule SUP_least) simp - finally show "y \ B" . - qed -next - fix P assume P: "eventually P F" - then have "eventually (\x. f x \ SUPR (Collect P) f) F" - by eventually_elim (auto intro!: SUP_upper) - then show "f0 \ SUPR (Collect P) f" - by (rule tendsto_le[OF ntriv tendsto_const lim]) -qed - definition (in order) mono_set: "mono_set S \ (\x y. x \ y \ x \ S \ y \ S)" diff -r 1cf4faed8b22 -r 78de6c7e8a58 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Wed Feb 06 17:18:01 2013 +0100 +++ b/src/HOL/Limits.thy Wed Feb 06 17:57:21 2013 +0100 @@ -469,12 +469,6 @@ apply (erule le_less_trans [OF dist_triangle]) done -lemma eventually_nhds_order: - "eventually P (nhds (a::'a::linorder_topology)) \ - (\S. open_interval S \ a \ S \ (\z\S. P z))" - (is "_ \ ?rhs") - unfolding eventually_nhds by (auto dest!: open_orderD dest: open_interval_imp_open) - lemma nhds_neq_bot [simp]: "nhds a \ bot" unfolding trivial_limit_def eventually_nhds by simp @@ -838,6 +832,35 @@ "(f ---> l) F \ (\e>0. eventually (\x. dist (f x) l < e) F)" using tendstoI tendstoD by fast +lemma order_tendstoI: + fixes y :: "_ :: order_topology" + assumes "\a. a < y \ eventually (\x. a < f x) F" + assumes "\a. y < a \ eventually (\x. f x < a) F" + shows "(f ---> y) F" +proof (rule topological_tendstoI) + fix S assume "open S" "y \ S" + then show "eventually (\x. f x \ S) F" + unfolding open_generated_order + proof induct + case (UN K) + then obtain k where "y \ k" "k \ K" by auto + with UN(2)[of k] show ?case + by (auto elim: eventually_elim1) + qed (insert assms, auto elim: eventually_elim2) +qed + +lemma order_tendstoD: + fixes y :: "_ :: order_topology" + assumes y: "(f ---> y) F" + shows "a < y \ eventually (\x. a < f x) F" + and "y < a \ eventually (\x. f x < a) F" + using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto + +lemma order_tendsto_iff: + fixes f :: "_ \ 'a :: order_topology" + shows "(f ---> x) F \(\lx. l < f x) F) \ (\u>x. eventually (\x. f x < u) F)" + by (metis order_tendstoI order_tendstoD) + lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\x. f x - a) F" by (simp only: tendsto_iff Zfun_def dist_norm) @@ -908,34 +931,18 @@ qed lemma increasing_tendsto: - fixes f :: "_ \ 'a::linorder_topology" + fixes f :: "_ \ 'a::order_topology" assumes bdd: "eventually (\n. f n \ l) F" and en: "\x. x < l \ eventually (\n. x < f n) F" shows "(f ---> l) F" -proof (rule topological_tendstoI) - fix S assume "open S" "l \ S" - then show "eventually (\x. f x \ S) F" - proof (induct rule: open_order_induct) - case (greaterThanLessThan a b) with en bdd show ?case - by (auto elim!: eventually_elim2) - qed (insert en bdd, auto elim!: eventually_elim1) -qed + using assms by (intro order_tendstoI) (auto elim!: eventually_elim1) lemma decreasing_tendsto: - fixes f :: "_ \ 'a::linorder_topology" + fixes f :: "_ \ 'a::order_topology" assumes bdd: "eventually (\n. l \ f n) F" and en: "\x. l < x \ eventually (\n. f n < x) F" shows "(f ---> l) F" -proof (rule topological_tendstoI) - fix S assume "open S" "l \ S" - then show "eventually (\x. f x \ S) F" - proof (induct rule: open_order_induct) - case (greaterThanLessThan a b) - with en have "eventually (\n. f n < b) F" by auto - with bdd show ?case - by eventually_elim (insert greaterThanLessThan, auto) - qed (insert en bdd, auto elim!: eventually_elim1) -qed + using assms by (intro order_tendstoI) (auto elim!: eventually_elim1) subsubsection {* Distance and norms *} @@ -1039,20 +1046,16 @@ qed lemma tendsto_sandwich: - fixes f g h :: "'a \ 'b::linorder_topology" + fixes f g h :: "'a \ 'b::order_topology" assumes ev: "eventually (\n. f n \ g n) net" "eventually (\n. g n \ h n) net" assumes lim: "(f ---> c) net" "(h ---> c) net" shows "(g ---> c) net" -proof (rule topological_tendstoI) - fix S assume "open S" "c \ S" - from open_orderD[OF this] obtain T where "open_interval T" "c \ T" "T \ S" by auto - with lim[THEN topological_tendstoD, of T] - have "eventually (\x. f x \ T) net" "eventually (\x. h x \ T) net" - by (auto dest: open_interval_imp_open) - with ev have "eventually (\x. g x \ T) net" - by eventually_elim (insert `open_interval T`, auto dest: open_intervalD) - with `T \ S` show "eventually (\x. g x \ S) net" - by (auto elim: eventually_elim1) +proof (rule order_tendstoI) + fix a show "a < c \ eventually (\x. a < g x) net" + using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2) +next + fix a show "c < a \ eventually (\x. g x < a) net" + using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2) qed lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real] @@ -1129,15 +1132,12 @@ shows "y \ x" proof (rule ccontr) assume "\ y \ x" - then have "x < y" by simp - from less_separate[OF this] obtain a b where xy: "x \ {.. {b <..}" "{.. {b<..} = {}" - by auto - then have less: "\x y. x < a \ b < y \ x < y" - by auto - from x[THEN topological_tendstoD, of "{..x. f x \ {..x. g x \ {b <..}) F" by auto + with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{.. {b<..} = {}" + by (auto simp: not_le) + then have "eventually (\x. f x < a) F" "eventually (\x. b < g x) F" + using x y by (auto intro: order_tendstoD) with ev have "eventually (\x. False) F" - by eventually_elim (auto dest!: less) + by eventually_elim (insert xy, fastforce) with F show False by (simp add: eventually_False) qed diff -r 1cf4faed8b22 -r 78de6c7e8a58 src/HOL/RealVector.thy --- a/src/HOL/RealVector.thy Wed Feb 06 17:18:01 2013 +0100 +++ b/src/HOL/RealVector.thy Wed Feb 06 17:57:21 2013 +0100 @@ -559,60 +559,6 @@ by (simp add: closed_Int) qed -inductive open_interval :: "'a::order set \ bool" where - empty[intro]: "open_interval {}" | - UNIV[intro]: "open_interval UNIV" | - greaterThan[intro]: "open_interval {a <..}" | - lessThan[intro]: "open_interval {..< b}" | - greaterThanLessThan[intro]: "open_interval {a <..< b}" -hide_fact (open) empty UNIV greaterThan lessThan greaterThanLessThan - -lemma open_intervalD: - "open_interval S \ x \ S \ y \ S \ x \ z \ z \ y \ z \ S" - by (cases rule: open_interval.cases) auto - -lemma open_interval_Int[intro]: - fixes S T :: "'a :: linorder set" - assumes S: "open_interval S" and T: "open_interval T" - shows "open_interval (S \ T)" -proof - - { fix a b :: 'a have "{.. {a<..} = { a <..} \ {..< b }" by auto } note this[simp] - { fix a b :: 'a and A have "{a <..} \ ({b <..} \ A) = {max a b <..} \ A" by auto } note this[simp] - { fix a b :: 'a and A have "{.. (A \ {.. {.. {..< b})" - unfolding greaterThanLessThan_eq[symmetric] by auto } note this[simp] - show ?thesis - by (cases rule: open_interval.cases[OF S, case_product open_interval.cases[OF T]]) - (auto simp: greaterThanLessThan_eq lessThan_Int_lessThan greaterThan_Int_greaterThan Int_assoc) -qed - -lemma open_interval_imp_open: "open_interval S \ open (S::'a::order_topology set)" - by (cases S rule: open_interval.cases) auto - -lemma open_orderD: - "open (S::'a::linorder_topology set) \ x \ S \ \T. open_interval T \ T \ S \ x \ T" - unfolding open_generated_order -proof (induct rule: generate_topology.induct) - case (UN K) then obtain k where "k \ K" "x \ k" by auto - with UN(2)[of k] show ?case by auto -qed auto - -lemma open_order_induct[consumes 2, case_names subset UNIV lessThan greaterThan greaterThanLessThan]: - fixes S :: "'a::linorder_topology set" - assumes S: "open S" "x \ S" - assumes subset: "\S T. P S \ S \ T \ P T" - assumes univ: "P UNIV" - assumes lt: "\a. x < a \ P {..< a}" - assumes gt: "\a. a < x \ P {a <..}" - assumes lgt: "\a b. a < x \ x < b \ P {a <..< b}" - shows "P S" -proof - - from open_orderD[OF S] obtain T where "open_interval T" "T \ S" "x \ T" - by auto - then show "P S" - by induct (auto intro: univ subset lt gt lgt) -qed - subsection {* Metric spaces *} class dist =