# HG changeset patch # User hoelzl # Date 1354555144 -3600 # Node ID 5e40ad9f212a3231837cd8b27ddedfaa7cc2d306 # Parent 0a1242d5e7d48f351ed6b70dc1a1c94573fa0b50 add filterlim rules for inverse and at_infinity diff -r 0a1242d5e7d4 -r 5e40ad9f212a src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Dec 03 18:19:02 2012 +0100 +++ b/src/HOL/Limits.thy Mon Dec 03 18:19:04 2012 +0100 @@ -447,7 +447,7 @@ 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)" + "eventually P at_infinity \ (\b. \x. b \ norm x \ P x)" unfolding at_infinity_def proof (rule eventually_Abs_filter, rule is_filter.intro) fix P Q :: "'a \ bool" @@ -458,6 +458,30 @@ then show "\r. \x. r \ norm x \ P x \ Q x" .. qed auto +lemma at_infinity_eq_at_top_bot: + "(at_infinity \ real filter) = sup at_top at_bot" + unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder +proof (intro arg_cong[where f=Abs_filter] ext iffI) + fix P :: "real \ bool" assume "\r. \x. r \ norm x \ P x" + then guess r .. + then have "(\x\r. P x) \ (\x\-r. P x)" by auto + then show "(\r. \x\r. P x) \ (\r. \x\r. P x)" by auto +next + fix P :: "real \ bool" assume "(\r. \x\r. P x) \ (\r. \x\r. P x)" + then obtain p q where "\x\p. P x" "\x\q. P x" by auto + then show "\r. \x. r \ norm x \ P x" + by (intro exI[of _ "max p (-q)"]) + (auto simp: abs_real_def) +qed + +lemma at_top_le_at_infinity: + "at_top \ (at_infinity :: real filter)" + unfolding at_infinity_eq_at_top_bot by simp + +lemma at_bot_le_at_infinity: + "at_bot \ (at_infinity :: real filter)" + unfolding at_infinity_eq_at_top_bot by simp + subsection {* Boundedness *} definition Bfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" @@ -641,11 +665,9 @@ translations "LIM x F1. f :> F2" == "CONST filterlim (%x. f) F2 F1" -lemma filterlimE: "(LIM x F1. f x :> F2) \ eventually P F2 \ eventually (\x. P (f x)) F1" - by (auto simp: filterlim_def eventually_filtermap le_filter_def) - -lemma filterlimI: "(\P. eventually P F2 \ eventually (\x. P (f x)) F1) \ (LIM x F1. f x :> F2)" - by (auto simp: filterlim_def eventually_filtermap le_filter_def) +lemma filterlim_iff: + "(LIM x F1. f x :> F2) \ (\P. eventually P F2 \ eventually (\x. P (f x)) F1)" + unfolding filterlim_def le_filter_def eventually_filtermap .. lemma filterlim_compose: "filterlim g F3 F2 \ filterlim f F2 F1 \ filterlim (\x. g (f x)) F3 F1" @@ -655,6 +677,14 @@ "filterlim f F2 F1 \ F2 \ F2' \ F1' \ F1 \ filterlim f F2' F1'" unfolding filterlim_def by (metis filtermap_mono order_trans) +lemma filterlim_within: + "(LIM x F1. f x :> F2 within S) \ (eventually (\x. f x \ S) F1 \ (LIM x F1. f x :> F2))" + unfolding filterlim_def +proof safe + assume "filtermap f F1 \ F2 within S" then show "eventually (\x. f x \ S) F1" + by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\x. x \ S"]) +qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap) + abbreviation (in topological_space) tendsto :: "('b \ 'a) \ 'a \ 'b filter \ bool" (infixr "--->" 55) where "(f ---> l) F \ filterlim f (nhds l) F" @@ -678,6 +708,10 @@ by (auto elim!: allE[of _ "\x. x \ S"] eventually_rev_mp) qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def) +lemma filterlim_at: + "(LIM x F. f x :> at b) \ (eventually (\x. f x \ b) F \ (f ---> b) F)" + by (simp add: at_def filterlim_within) + lemma tendsto_mono: "F \ F' \ (f ---> l) F' \ (f ---> l) F" unfolding tendsto_def le_filter_def by fast @@ -770,15 +804,8 @@ unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g]) lemma tendsto_compose_eventually: - assumes g: "(g ---> m) (at l)" - assumes f: "(f ---> l) F" - assumes inj: "eventually (\x. f x \ l) F" - shows "((\x. g (f x)) ---> m) F" -proof - - from f inj have "LIM x F. f x :> at l" - unfolding filterlim_def at_def by (simp add: le_within_iff eventually_filtermap) - from filterlim_compose[OF g this] show ?thesis . -qed + "(g ---> m) (at l) \ (f ---> l) F \ eventually (\x. f x \ l) F \ ((\x. g (f x)) ---> m) F" + by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at) lemma metric_tendsto_imp_tendsto: assumes f: "(f ---> a) F" @@ -1092,8 +1119,7 @@ lemma filterlim_at_top: fixes f :: "'a \ ('b::dense_linorder)" shows "(LIM x F. f x :> at_top) \ (\Z. eventually (\x. Z < f x) F)" - by (safe elim!: filterlimE intro!: filterlimI) - (auto simp: eventually_at_top_dense elim!: eventually_elim1) + by (auto simp: filterlim_iff eventually_at_top_dense elim!: eventually_elim1) lemma filterlim_at_top_gt: fixes f :: "'a \ ('b::dense_linorder)" and c :: "'b" @@ -1109,8 +1135,7 @@ lemma filterlim_at_bot: fixes f :: "'a \ ('b::dense_linorder)" shows "(LIM x F. f x :> at_bot) \ (\Z. eventually (\x. f x < Z) F)" - by (safe elim!: filterlimE intro!: filterlimI) - (auto simp: eventually_at_bot_dense elim!: eventually_elim1) + by (auto simp: filterlim_iff eventually_at_bot_dense elim!: eventually_elim1) lemma filterlim_at_bot_lt: fixes f :: "'a \ ('b::dense_linorder)" and c :: "'b" @@ -1123,6 +1148,25 @@ by (auto elim!: eventually_elim1) qed simp +lemma filterlim_at_infinity: + fixes f :: "_ \ 'a\real_normed_vector" + assumes "0 \ c" + shows "(LIM x F. f x :> at_infinity) \ (\r>c. eventually (\x. r \ norm (f x)) F)" + unfolding filterlim_iff eventually_at_infinity +proof safe + fix P :: "'a \ bool" and b + assume *: "\r>c. eventually (\x. r \ norm (f x)) F" + and P: "\x. b \ norm x \ P x" + have "max b (c + 1) > c" by auto + with * have "eventually (\x. max b (c + 1) \ norm (f x)) F" + by auto + then show "eventually (\x. P (f x)) F" + proof eventually_elim + fix x assume "max b (c + 1) \ norm (f x)" + with P show "P (f x)" by auto + qed +qed force + lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top" unfolding filterlim_at_top apply (intro allI) @@ -1176,6 +1220,55 @@ 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]) +lemma tendsto_inverse_0: + fixes x :: "_ \ 'a\real_normed_div_algebra" + shows "(inverse ---> (0::'a)) at_infinity" + unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity +proof safe + fix r :: real assume "0 < r" + show "\b. \x. b \ norm x \ norm (inverse x :: 'a) < r" + proof (intro exI[of _ "inverse (r / 2)"] allI impI) + fix x :: 'a + from `0 < r` have "0 < inverse (r / 2)" by simp + also assume *: "inverse (r / 2) \ norm x" + finally show "norm (inverse x) < r" + using * `0 < r` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps) + qed +qed + +lemma filterlim_inverse_at_infinity: + fixes x :: "_ \ 'a\{real_normed_div_algebra, division_ring_inverse_zero}" + shows "filterlim inverse at_infinity (at (0::'a))" + unfolding filterlim_at_infinity[OF order_refl] +proof safe + fix r :: real assume "0 < r" + then show "eventually (\x::'a. r \ norm (inverse x)) (at 0)" + unfolding eventually_at norm_inverse + by (intro exI[of _ "inverse r"]) + (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide) +qed + +lemma filterlim_inverse_at_iff: + fixes g :: "'a \ 'b\{real_normed_div_algebra, division_ring_inverse_zero}" + shows "(LIM x F. inverse (g x) :> at 0) \ (LIM x F. g x :> at_infinity)" + unfolding filterlim_def filtermap_filtermap[symmetric] +proof + assume "filtermap g F \ at_infinity" + then have "filtermap inverse (filtermap g F) \ filtermap inverse at_infinity" + by (rule filtermap_mono) + also have "\ \ at 0" + using tendsto_inverse_0 + by (auto intro!: le_withinI exI[of _ 1] + simp: eventually_filtermap eventually_at_infinity filterlim_def at_def) + finally show "filtermap inverse (filtermap g F) \ at 0" . +next + assume "filtermap inverse (filtermap g F) \ at 0" + then have "filtermap inverse (filtermap inverse (filtermap g F)) \ filtermap inverse (at 0)" + by (rule filtermap_mono) + with filterlim_inverse_at_infinity show "filtermap g F \ at_infinity" + by (auto intro: order_trans simp: filterlim_def filtermap_filtermap) +qed + text {* We only show rules for multiplication and addition when the functions are either against a real