(* Title : Limits.thy Author : Brian Huffman *) header {* Filters and Limits *} theory Limits imports RealVector begin subsection {* Nets *} text {* A net is now defined simply as a filter on a set. The definition also allows non-proper filters. *} locale is_filter = fixes net :: "('a \ bool) \ bool" assumes True: "net (\x. True)" assumes conj: "net (\x. P x) \ net (\x. Q x) \ net (\x. P x \ Q x)" assumes mono: "\x. P x \ Q x \ net (\x. P x) \ net (\x. Q x)" typedef (open) 'a net = "{net :: ('a \ bool) \ bool. is_filter net}" proof show "(\x. True) \ ?net" by (auto intro: is_filter.intro) qed lemma is_filter_Rep_net: "is_filter (Rep_net net)" using Rep_net [of net] by simp lemma Abs_net_inverse': assumes "is_filter net" shows "Rep_net (Abs_net net) = net" using assms by (simp add: Abs_net_inverse) subsection {* Eventually *} definition eventually :: "('a \ bool) \ 'a net \ bool" where [code del]: "eventually P net \ Rep_net net P" lemma eventually_Abs_net: assumes "is_filter net" shows "eventually P (Abs_net net) = net P" unfolding eventually_def using assms by (simp add: Abs_net_inverse) lemma expand_net_eq: shows "net = net' \ (\P. eventually P net = eventually P net')" unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def .. lemma eventually_True [simp]: "eventually (\x. True) net" unfolding eventually_def by (rule is_filter.True [OF is_filter_Rep_net]) lemma always_eventually: "\x. P x \ eventually P net" proof - assume "\x. P x" hence "P = (\x. True)" by (simp add: ext) thus "eventually P net" by simp qed lemma eventually_mono: "(\x. P x \ Q x) \ eventually P net \ eventually Q net" unfolding eventually_def by (rule is_filter.mono [OF is_filter_Rep_net]) lemma eventually_conj: assumes P: "eventually (\x. P x) net" assumes Q: "eventually (\x. Q x) net" shows "eventually (\x. P x \ Q x) net" using assms unfolding eventually_def by (rule is_filter.conj [OF is_filter_Rep_net]) lemma eventually_mp: assumes "eventually (\x. P x \ Q x) net" assumes "eventually (\x. P x) net" shows "eventually (\x. Q x) net" proof (rule eventually_mono) show "\x. (P x \ Q x) \ P x \ Q x" by simp show "eventually (\x. (P x \ Q x) \ P x) net" using assms by (rule eventually_conj) qed lemma eventually_rev_mp: assumes "eventually (\x. P x) net" assumes "eventually (\x. P x \ Q x) net" shows "eventually (\x. Q x) net" using assms(2) assms(1) by (rule eventually_mp) lemma eventually_conj_iff: "eventually (\x. P x \ Q x) net \ eventually P net \ eventually Q net" by (auto intro: eventually_conj elim: eventually_rev_mp) lemma eventually_elim1: assumes "eventually (\i. P i) net" assumes "\i. P i \ Q i" shows "eventually (\i. Q i) net" using assms by (auto elim!: eventually_rev_mp) lemma eventually_elim2: assumes "eventually (\i. P i) net" assumes "eventually (\i. Q i) net" assumes "\i. P i \ Q i \ R i" shows "eventually (\i. R i) net" using assms by (auto elim!: eventually_rev_mp) subsection {* Finer-than relation *} text {* @{term "net \ net'"} means that @{term net} is finer than @{term net'}. *} instantiation net :: (type) complete_lattice begin definition le_net_def [code del]: "net \ net' \ (\P. eventually P net' \ eventually P net)" definition less_net_def [code del]: "(net :: 'a net) < net' \ net \ net' \ \ net' \ net" definition top_net_def [code del]: "top = Abs_net (\P. \x. P x)" definition bot_net_def [code del]: "bot = Abs_net (\P. True)" definition sup_net_def [code del]: "sup net net' = Abs_net (\P. eventually P net \ eventually P net')" definition inf_net_def [code del]: "inf a b = Abs_net (\P. \Q R. eventually Q a \ eventually R b \ (\x. Q x \ R x \ P x))" definition Sup_net_def [code del]: "Sup A = Abs_net (\P. \net\A. eventually P net)" definition Inf_net_def [code del]: "Inf A = Sup {x::'a net. \y\A. x \ y}" lemma eventually_top [simp]: "eventually P top \ (\x. P x)" unfolding top_net_def by (rule eventually_Abs_net, rule is_filter.intro, auto) lemma eventually_bot [simp]: "eventually P bot" unfolding bot_net_def by (subst eventually_Abs_net, rule is_filter.intro, auto) lemma eventually_sup: "eventually P (sup net net') \ eventually P net \ eventually P net'" unfolding sup_net_def by (rule eventually_Abs_net, rule is_filter.intro) (auto elim!: eventually_rev_mp) lemma eventually_inf: "eventually P (inf a b) \ (\Q R. eventually Q a \ eventually R b \ (\x. Q x \ R x \ P x))" unfolding inf_net_def apply (rule eventually_Abs_net, rule is_filter.intro) apply (fast intro: eventually_True) apply clarify apply (intro exI conjI) apply (erule (1) eventually_conj) apply (erule (1) eventually_conj) apply simp apply auto done lemma eventually_Sup: "eventually P (Sup A) \ (\net\A. eventually P net)" unfolding Sup_net_def apply (rule eventually_Abs_net, rule is_filter.intro) apply (auto intro: eventually_conj elim!: eventually_rev_mp) done instance proof fix x y :: "'a net" show "x < y \ x \ y \ \ y \ x" by (rule less_net_def) next fix x :: "'a net" show "x \ x" unfolding le_net_def by simp next fix x y z :: "'a net" assume "x \ y" and "y \ z" thus "x \ z" unfolding le_net_def by simp next fix x y :: "'a net" assume "x \ y" and "y \ x" thus "x = y" unfolding le_net_def expand_net_eq by fast next fix x :: "'a net" show "x \ top" unfolding le_net_def eventually_top by (simp add: always_eventually) next fix x :: "'a net" show "bot \ x" unfolding le_net_def by simp next fix x y :: "'a net" show "x \ sup x y" and "y \ sup x y" unfolding le_net_def eventually_sup by simp_all next fix x y z :: "'a net" assume "x \ z" and "y \ z" thus "sup x y \ z" unfolding le_net_def eventually_sup by simp next fix x y :: "'a net" show "inf x y \ x" and "inf x y \ y" unfolding le_net_def eventually_inf by (auto intro: eventually_True) next fix x y z :: "'a net" assume "x \ y" and "x \ z" thus "x \ inf y z" unfolding le_net_def eventually_inf by (auto elim!: eventually_mono intro: eventually_conj) next fix x :: "'a net" and A assume "x \ A" thus "x \ Sup A" unfolding le_net_def eventually_Sup by simp next fix A and y :: "'a net" assume "\x. x \ A \ x \ y" thus "Sup A \ y" unfolding le_net_def eventually_Sup by simp next fix z :: "'a net" and A assume "z \ A" thus "Inf A \ z" unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp next fix A and x :: "'a net" assume "\y. y \ A \ x \ y" thus "x \ Inf A" unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp qed end lemma net_leD: "net \ net' \ eventually P net' \ eventually P net" unfolding le_net_def by simp lemma net_leI: "(\P. eventually P net' \ eventually P net) \ net \ net'" unfolding le_net_def by simp lemma eventually_False: "eventually (\x. False) net \ net = bot" unfolding expand_net_eq by (auto elim: eventually_rev_mp) subsection {* Map function for nets *} definition netmap :: "('a \ 'b) \ 'a net \ 'b net" where [code del]: "netmap f net = Abs_net (\P. eventually (\x. P (f x)) net)" lemma eventually_netmap: "eventually P (netmap f net) = eventually (\x. P (f x)) net" unfolding netmap_def apply (rule eventually_Abs_net) apply (rule is_filter.intro) apply (auto elim!: eventually_rev_mp) done lemma netmap_ident: "netmap (\x. x) net = net" by (simp add: expand_net_eq eventually_netmap) lemma netmap_netmap: "netmap f (netmap g net) = netmap (\x. f (g x)) net" by (simp add: expand_net_eq eventually_netmap) lemma netmap_mono: "net \ net' \ netmap f net \ netmap f net'" unfolding le_net_def eventually_netmap by simp lemma netmap_bot [simp]: "netmap f bot = bot" by (simp add: expand_net_eq eventually_netmap) subsection {* Sequentially *} definition sequentially :: "nat net" where [code del]: "sequentially = Abs_net (\P. \k. \n\k. P n)" lemma eventually_sequentially: "eventually P sequentially \ (\N. \n\N. P n)" unfolding sequentially_def proof (rule eventually_Abs_net, rule is_filter.intro) fix P Q :: "nat \ bool" assume "\i. \n\i. P n" and "\j. \n\j. Q n" then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto then have "\n\max i j. P n \ Q n" by simp then show "\k. \n\k. P n \ Q n" .. qed auto lemma sequentially_bot [simp]: "sequentially \ bot" unfolding expand_net_eq eventually_sequentially by auto lemma eventually_False_sequentially [simp]: "\ eventually (\n. False) sequentially" by (simp add: eventually_False) lemma le_sequentially: "net \ sequentially \ (\N. eventually (\n. N \ n) net)" unfolding le_net_def eventually_sequentially by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) subsection {* Standard Nets *} definition within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) where [code del]: "net within S = Abs_net (\P. eventually (\x. x \ S \ P x) net)" definition nhds :: "'a::topological_space \ 'a net" where [code del]: "nhds a = Abs_net (\P. \S. open S \ a \ S \ (\x\S. P x))" definition at :: "'a::topological_space \ 'a net" where [code del]: "at a = nhds a within - {a}" lemma eventually_within: "eventually P (net within S) = eventually (\x. x \ S \ P x) net" unfolding within_def by (rule eventually_Abs_net, rule is_filter.intro) (auto elim!: eventually_rev_mp) lemma within_UNIV: "net within UNIV = net" unfolding expand_net_eq eventually_within by simp lemma eventually_nhds: "eventually P (nhds a) \ (\S. open S \ a \ S \ (\x\S. P x))" unfolding nhds_def proof (rule eventually_Abs_net, 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 next fix P Q assume "\S. open S \ a \ S \ (\x\S. P x)" and "\T. open T \ a \ T \ (\x\T. Q x)" then obtain S T where "open S \ a \ S \ (\x\S. P x)" "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 qed auto lemma eventually_nhds_metric: "eventually P (nhds a) \ (\d>0. \x. dist x a < d \ P x)" unfolding eventually_nhds open_dist apply safe apply fast apply (rule_tac x="{x. dist x a < d}" in exI, simp) apply clarsimp apply (rule_tac x="d - dist x a" in exI, clarsimp) apply (simp only: less_diff_eq) apply (erule le_less_trans [OF dist_triangle]) done lemma eventually_at_topological: "eventually P (at a) \ (\S. open S \ a \ S \ (\x\S. x \ a \ P x))" unfolding at_def eventually_within eventually_nhds by simp lemma eventually_at: fixes a :: "'a::metric_space" shows "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" unfolding at_def eventually_within eventually_nhds_metric by auto subsection {* Boundedness *} definition Bfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where [code del]: "Bfun f net = (\K>0. eventually (\x. norm (f x) \ K) net)" lemma BfunI: assumes K: "eventually (\x. norm (f x) \ K) net" shows "Bfun f net" unfolding Bfun_def proof (intro exI conjI allI) show "0 < max K 1" by simp next show "eventually (\x. norm (f x) \ max K 1) net" using K by (rule eventually_elim1, simp) qed lemma BfunE: assumes "Bfun f net" obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) net" using assms unfolding Bfun_def by fast subsection {* Convergence to Zero *} definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where [code del]: "Zfun f net = (\r>0. eventually (\x. norm (f x) < r) net)" lemma ZfunI: "(\r. 0 < r \ eventually (\x. norm (f x) < r) net) \ Zfun f net" unfolding Zfun_def by simp lemma ZfunD: "\Zfun f net; 0 < r\ \ eventually (\x. norm (f x) < r) net" unfolding Zfun_def by simp lemma Zfun_ssubst: "eventually (\x. f x = g x) net \ Zfun g net \ Zfun f net" unfolding Zfun_def by (auto elim!: eventually_rev_mp) lemma Zfun_zero: "Zfun (\x. 0) net" unfolding Zfun_def by simp lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) net = Zfun (\x. f x) net" unfolding Zfun_def by simp lemma Zfun_imp_Zfun: assumes f: "Zfun f net" assumes g: "eventually (\x. norm (g x) \ norm (f x) * K) net" shows "Zfun (\x. g x) net" proof (cases) assume K: "0 < K" show ?thesis proof (rule ZfunI) fix r::real assume "0 < r" hence "0 < r / K" using K by (rule divide_pos_pos) then have "eventually (\x. norm (f x) < r / K) net" using ZfunD [OF f] by fast with g show "eventually (\x. norm (g x) < r) net" proof (rule eventually_elim2) fix x assume *: "norm (g x) \ norm (f x) * K" assume "norm (f x) < r / K" hence "norm (f x) * K < r" by (simp add: pos_less_divide_eq K) thus "norm (g x) < r" by (simp add: order_le_less_trans [OF *]) qed qed next assume "\ 0 < K" hence K: "K \ 0" by (simp only: not_less) show ?thesis proof (rule ZfunI) fix r :: real assume "0 < r" from g show "eventually (\x. norm (g x) < r) net" proof (rule eventually_elim1) fix x assume "norm (g x) \ norm (f x) * K" also have "\ \ norm (f x) * 0" using K norm_ge_zero by (rule mult_left_mono) finally show "norm (g x) < r" using `0 < r` by simp qed qed qed lemma Zfun_le: "\Zfun g net; \x. norm (f x) \ norm (g x)\ \ Zfun f net" by (erule_tac K="1" in Zfun_imp_Zfun, simp) lemma Zfun_add: assumes f: "Zfun f net" and g: "Zfun g net" shows "Zfun (\x. f x + g x) net" proof (rule ZfunI) fix r::real assume "0 < r" hence r: "0 < r / 2" by simp have "eventually (\x. norm (f x) < r/2) net" using f r by (rule ZfunD) moreover have "eventually (\x. norm (g x) < r/2) net" using g r by (rule ZfunD) ultimately show "eventually (\x. norm (f x + g x) < r) net" proof (rule eventually_elim2) fix x assume *: "norm (f x) < r/2" "norm (g x) < r/2" have "norm (f x + g x) \ norm (f x) + norm (g x)" by (rule norm_triangle_ineq) also have "\ < r/2 + r/2" using * by (rule add_strict_mono) finally show "norm (f x + g x) < r" by simp qed qed lemma Zfun_minus: "Zfun f net \ Zfun (\x. - f x) net" unfolding Zfun_def by simp lemma Zfun_diff: "\Zfun f net; Zfun g net\ \ Zfun (\x. f x - g x) net" by (simp only: diff_minus Zfun_add Zfun_minus) lemma (in bounded_linear) Zfun: assumes g: "Zfun g net" shows "Zfun (\x. f (g x)) net" proof - obtain K where "\x. norm (f x) \ norm x * K" using bounded by fast then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) net" by simp with g show ?thesis by (rule Zfun_imp_Zfun) qed lemma (in bounded_bilinear) Zfun: assumes f: "Zfun f net" assumes g: "Zfun g net" shows "Zfun (\x. f x ** g x) net" proof (rule ZfunI) fix r::real assume r: "0 < r" obtain K where K: "0 < K" and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" using pos_bounded by fast from K have K': "0 < inverse K" by (rule positive_imp_inverse_positive) have "eventually (\x. norm (f x) < r) net" using f r by (rule ZfunD) moreover have "eventually (\x. norm (g x) < inverse K) net" using g K' by (rule ZfunD) ultimately show "eventually (\x. norm (f x ** g x) < r) net" proof (rule eventually_elim2) fix x assume *: "norm (f x) < r" "norm (g x) < inverse K" have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" by (rule norm_le) also have "norm (f x) * norm (g x) * K < r * inverse K * K" by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K) also from K have "r * inverse K * K = r" by simp finally show "norm (f x ** g x) < r" . qed qed lemma (in bounded_bilinear) Zfun_left: "Zfun f net \ Zfun (\x. f x ** a) net" by (rule bounded_linear_left [THEN bounded_linear.Zfun]) lemma (in bounded_bilinear) Zfun_right: "Zfun f net \ Zfun (\x. a ** f x) net" by (rule bounded_linear_right [THEN bounded_linear.Zfun]) lemmas Zfun_mult = mult.Zfun lemmas Zfun_mult_right = mult.Zfun_right lemmas Zfun_mult_left = mult.Zfun_left subsection {* Limits *} definition tendsto :: "('a \ 'b::topological_space) \ 'b \ 'a net \ bool" (infixr "--->" 55) where [code del]: "(f ---> l) net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" ML {* structure Tendsto_Intros = Named_Thms ( val name = "tendsto_intros" val description = "introduction rules for tendsto" ) *} setup Tendsto_Intros.setup lemma tendsto_mono: "net \ net' \ (f ---> l) net' \ (f ---> l) net" unfolding tendsto_def le_net_def by fast lemma topological_tendstoI: "(\S. open S \ l \ S \ eventually (\x. f x \ S) net) \ (f ---> l) net" unfolding tendsto_def by auto lemma topological_tendstoD: "(f ---> l) net \ open S \ l \ S \ eventually (\x. f x \ S) net" unfolding tendsto_def by auto lemma tendstoI: assumes "\e. 0 < e \ eventually (\x. dist (f x) l < e) net" shows "(f ---> l) net" apply (rule topological_tendstoI) apply (simp add: open_dist) apply (drule (1) bspec, clarify) apply (drule assms) apply (erule eventually_elim1, simp) done lemma tendstoD: "(f ---> l) net \ 0 < e \ eventually (\x. dist (f x) l < e) net" apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) apply (clarsimp simp add: open_dist) apply (rule_tac x="e - dist x l" in exI, clarsimp) apply (simp only: less_diff_eq) apply (erule le_less_trans [OF dist_triangle]) apply simp apply simp done lemma tendsto_iff: "(f ---> l) net \ (\e>0. eventually (\x. dist (f x) l < e) net)" using tendstoI tendstoD by fast lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\x. f x - a) net" by (simp only: tendsto_iff Zfun_def dist_norm) lemma tendsto_ident_at [tendsto_intros]: "((\x. x) ---> a) (at a)" unfolding tendsto_def eventually_at_topological by auto lemma tendsto_ident_at_within [tendsto_intros]: "((\x. x) ---> a) (at a within S)" unfolding tendsto_def eventually_within eventually_at_topological by auto lemma tendsto_const [tendsto_intros]: "((\x. k) ---> k) net" by (simp add: tendsto_def) lemma tendsto_const_iff: fixes k l :: "'a::metric_space" assumes "net \ bot" shows "((\n. k) ---> l) net \ k = l" apply (safe intro!: tendsto_const) apply (rule ccontr) apply (drule_tac e="dist k l" in tendstoD) apply (simp add: zero_less_dist_iff) apply (simp add: eventually_False assms) done lemma tendsto_dist [tendsto_intros]: assumes f: "(f ---> l) net" and g: "(g ---> m) net" shows "((\x. dist (f x) (g x)) ---> dist l m) net" proof (rule tendstoI) fix e :: real assume "0 < e" hence e2: "0 < e/2" by simp from tendstoD [OF f e2] tendstoD [OF g e2] show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) net" proof (rule eventually_elim2) fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2" then show "dist (dist (f x) (g x)) (dist l m) < e" unfolding dist_real_def using dist_triangle2 [of "f x" "g x" "l"] using dist_triangle2 [of "g x" "l" "m"] using dist_triangle3 [of "l" "m" "f x"] using dist_triangle [of "f x" "m" "g x"] by arith qed qed lemma norm_conv_dist: "norm x = dist x 0" unfolding dist_norm by simp lemma tendsto_norm [tendsto_intros]: "(f ---> a) net \ ((\x. norm (f x)) ---> norm a) net" unfolding norm_conv_dist by (intro tendsto_intros) lemma tendsto_norm_zero: "(f ---> 0) net \ ((\x. norm (f x)) ---> 0) net" by (drule tendsto_norm, simp) lemma tendsto_norm_zero_cancel: "((\x. norm (f x)) ---> 0) net \ (f ---> 0) net" unfolding tendsto_iff dist_norm by simp lemma tendsto_norm_zero_iff: "((\x. norm (f x)) ---> 0) net \ (f ---> 0) net" unfolding tendsto_iff dist_norm by simp lemma add_diff_add: fixes a b c d :: "'a::ab_group_add" shows "(a + c) - (b + d) = (a - b) + (c - d)" by simp lemma minus_diff_minus: fixes a b :: "'a::ab_group_add" shows "(- a) - (- b) = - (a - b)" by simp lemma tendsto_add [tendsto_intros]: fixes a b :: "'a::real_normed_vector" shows "\(f ---> a) net; (g ---> b) net\ \ ((\x. f x + g x) ---> a + b) net" by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) lemma tendsto_minus [tendsto_intros]: fixes a :: "'a::real_normed_vector" shows "(f ---> a) net \ ((\x. - f x) ---> - a) net" by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) lemma tendsto_minus_cancel: fixes a :: "'a::real_normed_vector" shows "((\x. - f x) ---> - a) net \ (f ---> a) net" by (drule tendsto_minus, simp) lemma tendsto_diff [tendsto_intros]: fixes a b :: "'a::real_normed_vector" shows "\(f ---> a) net; (g ---> b) net\ \ ((\x. f x - g x) ---> a - b) net" by (simp add: diff_minus tendsto_add tendsto_minus) lemma tendsto_setsum [tendsto_intros]: fixes f :: "'a \ 'b \ 'c::real_normed_vector" assumes "\i. i \ S \ (f i ---> a i) net" shows "((\x. \i\S. f i x) ---> (\i\S. a i)) net" proof (cases "finite S") assume "finite S" thus ?thesis using assms proof (induct set: finite) case empty show ?case by (simp add: tendsto_const) next case (insert i F) thus ?case by (simp add: tendsto_add) qed next assume "\ finite S" thus ?thesis by (simp add: tendsto_const) qed lemma (in bounded_linear) tendsto [tendsto_intros]: "(g ---> a) net \ ((\x. f (g x)) ---> f a) net" by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) lemma (in bounded_bilinear) tendsto [tendsto_intros]: "\(f ---> a) net; (g ---> b) net\ \ ((\x. f x ** g x) ---> a ** b) net" by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) subsection {* Continuity of Inverse *} lemma (in bounded_bilinear) Zfun_prod_Bfun: assumes f: "Zfun f net" assumes g: "Bfun g net" shows "Zfun (\x. f x ** g x) net" proof - obtain K where K: "0 \ K" and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" using nonneg_bounded by fast obtain B where B: "0 < B" and norm_g: "eventually (\x. norm (g x) \ B) net" using g by (rule BfunE) have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) net" using norm_g proof (rule eventually_elim1) fix x assume *: "norm (g x) \ B" have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" by (rule norm_le) also have "\ \ norm (f x) * B * K" by (intro mult_mono' order_refl norm_g norm_ge_zero mult_nonneg_nonneg K *) also have "\ = norm (f x) * (B * K)" by (rule mult_assoc) finally show "norm (f x ** g x) \ norm (f x) * (B * K)" . qed with f show ?thesis by (rule Zfun_imp_Zfun) qed lemma (in bounded_bilinear) flip: "bounded_bilinear (\x y. y ** x)" apply default apply (rule add_right) apply (rule add_left) apply (rule scaleR_right) apply (rule scaleR_left) apply (subst mult_commute) using bounded by fast lemma (in bounded_bilinear) Bfun_prod_Zfun: assumes f: "Bfun f net" assumes g: "Zfun g net" shows "Zfun (\x. f x ** g x) net" using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) lemma inverse_diff_inverse: "\(a::'a::division_ring) \ 0; b \ 0\ \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" by (simp add: algebra_simps) lemma Bfun_inverse_lemma: fixes x :: "'a::real_normed_div_algebra" shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" apply (subst nonzero_norm_inverse, clarsimp) apply (erule (1) le_imp_inverse_le) done lemma Bfun_inverse: fixes a :: "'a::real_normed_div_algebra" assumes f: "(f ---> a) net" assumes a: "a \ 0" shows "Bfun (\x. inverse (f x)) net" proof - from a have "0 < norm a" by simp hence "\r>0. r < norm a" by (rule dense) then obtain r where r1: "0 < r" and r2: "r < norm a" by fast have "eventually (\x. dist (f x) a < r) net" using tendstoD [OF f r1] by fast hence "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) net" proof (rule eventually_elim1) fix x assume "dist (f x) a < r" hence 1: "norm (f x - a) < r" by (simp add: dist_norm) hence 2: "f x \ 0" using r2 by auto hence "norm (inverse (f x)) = inverse (norm (f x))" by (rule nonzero_norm_inverse) also have "\ \ inverse (norm a - r)" proof (rule le_imp_inverse_le) show "0 < norm a - r" using r2 by simp next have "norm a - norm (f x) \ norm (a - f x)" by (rule norm_triangle_ineq2) also have "\ = norm (f x - a)" by (rule norm_minus_commute) also have "\ < r" using 1 . finally show "norm a - r \ norm (f x)" by simp qed finally show "norm (inverse (f x)) \ inverse (norm a - r)" . qed thus ?thesis by (rule BfunI) qed lemma tendsto_inverse_lemma: fixes a :: "'a::real_normed_div_algebra" shows "\(f ---> a) net; a \ 0; eventually (\x. f x \ 0) net\ \ ((\x. inverse (f x)) ---> inverse a) net" apply (subst tendsto_Zfun_iff) apply (rule Zfun_ssubst) apply (erule eventually_elim1) apply (erule (1) inverse_diff_inverse) apply (rule Zfun_minus) apply (rule Zfun_mult_left) apply (rule mult.Bfun_prod_Zfun) apply (erule (1) Bfun_inverse) apply (simp add: tendsto_Zfun_iff) done lemma tendsto_inverse [tendsto_intros]: fixes a :: "'a::real_normed_div_algebra" assumes f: "(f ---> a) net" assumes a: "a \ 0" shows "((\x. inverse (f x)) ---> inverse a) net" proof - from a have "0 < norm a" by simp with f have "eventually (\x. dist (f x) a < norm a) net" by (rule tendstoD) then have "eventually (\x. f x \ 0) net" unfolding dist_norm by (auto elim!: eventually_elim1) with f a show ?thesis by (rule tendsto_inverse_lemma) qed lemma tendsto_divide [tendsto_intros]: fixes a b :: "'a::real_normed_field" shows "\(f ---> a) net; (g ---> b) net; b \ 0\ \ ((\x. f x / g x) ---> a / b) net" by (simp add: mult.tendsto tendsto_inverse divide_inverse) end