# HG changeset patch # User hoelzl # Date 1354555142 -3600 # Node ID 0a1242d5e7d48f351ed6b70dc1a1c94573fa0b50 # Parent 3764d4620fb3dd70ba0e99ae75e169d25f46625d add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image diff -r 3764d4620fb3 -r 0a1242d5e7d4 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Dec 03 18:19:01 2012 +0100 +++ b/src/HOL/Limits.thy Mon Dec 03 18:19:02 2012 +0100 @@ -285,8 +285,7 @@ definition at_top :: "('a::order) filter" where "at_top = Abs_filter (\P. \k. \n\k. P n)" -lemma eventually_at_top_linorder: - fixes P :: "'a::linorder \ bool" shows "eventually P at_top \ (\N. \n\N. P n)" +lemma eventually_at_top_linorder: "eventually P at_top \ (\N::'a::linorder. \n\N. P n)" unfolding at_top_def proof (rule eventually_Abs_filter, rule is_filter.intro) fix P Q :: "'a \ bool" @@ -296,13 +295,12 @@ then show "\k. \n\k. P n \ Q n" .. qed auto -lemma eventually_at_top_dense: - fixes P :: "'a::dense_linorder \ bool" shows "eventually P at_top \ (\N. \n>N. P n)" +lemma eventually_at_top_dense: "eventually P at_top \ (\N::'a::dense_linorder. \n>N. P n)" unfolding eventually_at_top_linorder proof safe fix N assume "\n\N. P n" then show "\N. \n>N. P n" by (auto intro!: exI[of _ N]) next - fix N assume "\n>N. P n" + fix N assume "\n>N. P n" moreover from gt_ex[of N] guess y .. ultimately show "\N. \n\N. P n" by (auto intro!: exI[of _ y]) qed @@ -375,6 +373,9 @@ definition (in topological_space) at :: "'a \ 'a filter" where "at a = nhds a within - {a}" +definition at_infinity :: "'a::real_normed_vector filter" where + "at_infinity = Abs_filter (\P. \r. \x. r \ norm x \ P x)" + lemma eventually_within: "eventually P (F within S) = eventually (\x. x \ S \ P x) F" unfolding within_def @@ -401,7 +402,7 @@ unfolding nhds_def proof (rule eventually_Abs_filter, rule is_filter.intro) have "open UNIV \ a \ UNIV \ (\x\UNIV. True)" by simp - thus "\S. open S \ a \ S \ (\x\S. True)" by - rule + thus "\S. open S \ a \ S \ (\x\S. True)" .. next fix P Q assume "\S. open S \ a \ S \ (\x\S. P x)" @@ -411,7 +412,7 @@ "open T \ a \ T \ (\x\T. Q x)" by auto hence "open (S \ T) \ a \ S \ T \ (\x\(S \ T). P x \ Q x)" by (simp add: open_Int) - thus "\S. open S \ a \ S \ (\x\S. P x \ Q x)" by - rule + thus "\S. open S \ a \ S \ (\x\S. P x \ Q x)" .. qed auto lemma eventually_nhds_metric: @@ -445,6 +446,17 @@ lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \ bot" by (simp add: at_eq_bot_iff not_open_singleton) +lemma eventually_at_infinity: + "eventually P at_infinity \ (\b. \x. norm x >= b \ P x)" +unfolding at_infinity_def +proof (rule eventually_Abs_filter, rule is_filter.intro) + fix P Q :: "'a \ bool" + assume "\r. \x. r \ norm x \ P x" and "\s. \x. s \ norm x \ Q x" + then obtain r s where + "\x. r \ norm x \ P x" and "\x. s \ norm x \ Q x" by auto + then have "\x. max r s \ norm x \ P x \ Q x" by simp + then show "\r. \x. r \ norm x \ P x \ Q x" .. +qed auto subsection {* Boundedness *} @@ -1164,4 +1176,85 @@ lemma filterlim_uminus_at_bot: "LIM x F. f x :> at_top \ LIM x F. - (f x) :: real :> at_bot" by (rule filterlim_compose[OF filterlim_uminus_at_bot_at_top]) +text {* + +We only show rules for multiplication and addition when the functions are either against a real +value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}. + +*} + +lemma filterlim_tendsto_pos_mult_at_top: + assumes f: "(f ---> c) F" and c: "0 < c" + assumes g: "LIM x F. g x :> at_top" + shows "LIM x F. (f x * g x :: real) :> at_top" + unfolding filterlim_at_top_gt[where c=0] +proof safe + fix Z :: real assume "0 < Z" + from f `0 < c` have "eventually (\x. c / 2 < f x) F" + by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1 + simp: dist_real_def abs_real_def split: split_if_asm) + moreover from g have "eventually (\x. (Z / c * 2) < g x) F" + unfolding filterlim_at_top by auto + ultimately show "eventually (\x. Z < f x * g x) F" + proof eventually_elim + fix x assume "c / 2 < f x" "Z / c * 2 < g x" + with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) < f x * g x" + by (intro mult_strict_mono) (auto simp: zero_le_divide_iff) + with `0 < c` show "Z < f x * g x" + by simp + qed +qed + +lemma filterlim_at_top_mult_at_top: + assumes f: "LIM x F. f x :> at_top" + assumes g: "LIM x F. g x :> at_top" + shows "LIM x F. (f x * g x :: real) :> at_top" + unfolding filterlim_at_top_gt[where c=0] +proof safe + fix Z :: real assume "0 < Z" + from f have "eventually (\x. 1 < f x) F" + unfolding filterlim_at_top by auto + moreover from g have "eventually (\x. Z < g x) F" + unfolding filterlim_at_top by auto + ultimately show "eventually (\x. Z < f x * g x) F" + proof eventually_elim + fix x assume "1 < f x" "Z < g x" + with `0 < Z` have "1 * Z < f x * g x" + by (intro mult_strict_mono) (auto simp: zero_le_divide_iff) + then show "Z < f x * g x" + by simp + qed +qed + +lemma filterlim_tendsto_add_at_top: + assumes f: "(f ---> c) F" + assumes g: "LIM x F. g x :> at_top" + shows "LIM x F. (f x + g x :: real) :> at_top" + unfolding filterlim_at_top_gt[where c=0] +proof safe + fix Z :: real assume "0 < Z" + from f have "eventually (\x. c - 1 < f x) F" + by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def) + moreover from g have "eventually (\x. Z - (c - 1) < g x) F" + unfolding filterlim_at_top by auto + ultimately show "eventually (\x. Z < f x + g x) F" + by eventually_elim simp +qed + +lemma filterlim_at_top_add_at_top: + assumes f: "LIM x F. f x :> at_top" + assumes g: "LIM x F. g x :> at_top" + shows "LIM x F. (f x + g x :: real) :> at_top" + unfolding filterlim_at_top_gt[where c=0] +proof safe + fix Z :: real assume "0 < Z" + from f have "eventually (\x. 0 < f x) F" + unfolding filterlim_at_top by auto + moreover from g have "eventually (\x. Z < g x) F" + unfolding filterlim_at_top by auto + ultimately show "eventually (\x. Z < f x + g x) F" + by eventually_elim simp +qed + end + diff -r 3764d4620fb3 -r 0a1242d5e7d4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 03 18:19:01 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 03 18:19:02 2012 +0100 @@ -1102,28 +1102,10 @@ subsection {* Filters and the ``eventually true'' quantifier *} definition - at_infinity :: "'a::real_normed_vector filter" where - "at_infinity = Abs_filter (\P. \r. \x. r \ norm x \ P x)" - -definition indirection :: "'a::real_normed_vector \ 'a \ 'a filter" (infixr "indirection" 70) where "a indirection v = (at a) within {b. \c\0. b - a = scaleR c v}" -text{* Prove That They are all filters. *} - -lemma eventually_at_infinity: - "eventually P at_infinity \ (\b. \x. norm x >= b \ P x)" -unfolding at_infinity_def -proof (rule eventually_Abs_filter, rule is_filter.intro) - fix P Q :: "'a \ bool" - assume "\r. \x. r \ norm x \ P x" and "\s. \x. s \ norm x \ Q x" - then obtain r s where - "\x. r \ norm x \ P x" and "\x. s \ norm x \ Q x" by auto - then have "\x. max r s \ norm x \ P x \ Q x" by simp - then show "\r. \x. r \ norm x \ P x \ Q x" .. -qed auto - text {* Identify Trivial limits, where we can't approach arbitrarily closely. *} lemma trivial_limit_within: