wenzelm@52265: (* Title: HOL/Limits.thy hoelzl@51526: Author: Brian Huffman hoelzl@51526: Author: Jacques D. Fleuriot, University of Cambridge hoelzl@51526: Author: Lawrence C Paulson hoelzl@51526: Author: Jeremy Avigad huffman@31349: *) huffman@31349: hoelzl@51526: header {* Limits on Real Vector Spaces *} huffman@31349: huffman@31349: theory Limits hoelzl@51524: imports Real_Vector_Spaces huffman@31349: begin huffman@31349: hoelzl@51526: subsection {* Filter going to infinity norm *} hoelzl@51526: hoelzl@50324: definition at_infinity :: "'a::real_normed_vector filter" where hoelzl@57276: "at_infinity = (INF r. principal {x. r \ norm x})" hoelzl@50324: hoelzl@57276: lemma eventually_at_infinity: "eventually P at_infinity \ (\b. \x. b \ norm x \ P x)" hoelzl@57276: unfolding at_infinity_def hoelzl@57276: by (subst eventually_INF_base) hoelzl@57276: (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b]) huffman@31392: hoelzl@50325: lemma at_infinity_eq_at_top_bot: hoelzl@50325: "(at_infinity \ real filter) = sup at_top at_bot" hoelzl@57276: apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity hoelzl@57276: eventually_at_top_linorder eventually_at_bot_linorder) hoelzl@57276: apply safe hoelzl@57276: apply (rule_tac x="b" in exI, simp) hoelzl@57276: apply (rule_tac x="- b" in exI, simp) hoelzl@57276: apply (rule_tac x="max (- Na) N" in exI, auto simp: abs_real_def) hoelzl@57276: done hoelzl@50325: hoelzl@57276: lemma at_top_le_at_infinity: "at_top \ (at_infinity :: real filter)" hoelzl@50325: unfolding at_infinity_eq_at_top_bot by simp hoelzl@50325: hoelzl@57276: lemma at_bot_le_at_infinity: "at_bot \ (at_infinity :: real filter)" hoelzl@50325: unfolding at_infinity_eq_at_top_bot by simp hoelzl@50325: hoelzl@57275: lemma filterlim_at_top_imp_at_infinity: hoelzl@57275: fixes f :: "_ \ real" hoelzl@57275: shows "filterlim f at_top F \ filterlim f at_infinity F" hoelzl@57275: by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl]) hoelzl@57275: hoelzl@51531: subsubsection {* Boundedness *} hoelzl@51531: hoelzl@51531: definition Bfun :: "('a \ 'b::metric_space) \ 'a filter \ bool" where hoelzl@51531: Bfun_metric_def: "Bfun f F = (\y. \K>0. eventually (\x. dist (f x) y \ K) F)" hoelzl@51531: hoelzl@51531: abbreviation Bseq :: "(nat \ 'a::metric_space) \ bool" where hoelzl@51531: "Bseq X \ Bfun X sequentially" hoelzl@51531: hoelzl@51531: lemma Bseq_conv_Bfun: "Bseq X \ Bfun X sequentially" .. hoelzl@51531: hoelzl@51531: lemma Bseq_ignore_initial_segment: "Bseq X \ Bseq (\n. X (n + k))" hoelzl@51531: unfolding Bfun_metric_def by (subst eventually_sequentially_seg) hoelzl@51531: hoelzl@51531: lemma Bseq_offset: "Bseq (\n. X (n + k)) \ Bseq X" hoelzl@51531: unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg) huffman@31355: hoelzl@51474: lemma Bfun_def: hoelzl@51474: "Bfun f F \ (\K>0. eventually (\x. norm (f x) \ K) F)" hoelzl@51474: unfolding Bfun_metric_def norm_conv_dist hoelzl@51474: proof safe hoelzl@51474: fix y K assume "0 < K" and *: "eventually (\x. dist (f x) y \ K) F" hoelzl@51474: moreover have "eventually (\x. dist (f x) 0 \ dist (f x) y + dist 0 y) F" hoelzl@51474: by (intro always_eventually) (metis dist_commute dist_triangle) hoelzl@51474: with * have "eventually (\x. dist (f x) 0 \ K + dist 0 y) F" hoelzl@51474: by eventually_elim auto hoelzl@51474: with `0 < K` show "\K>0. eventually (\x. dist (f x) 0 \ K) F" hoelzl@51474: by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto hoelzl@51474: qed auto huffman@31355: huffman@31487: lemma BfunI: huffman@44195: assumes K: "eventually (\x. norm (f x) \ K) F" shows "Bfun f F" huffman@31355: unfolding Bfun_def huffman@31355: proof (intro exI conjI allI) huffman@31355: show "0 < max K 1" by simp huffman@31355: next huffman@44195: show "eventually (\x. norm (f x) \ max K 1) F" huffman@31355: using K by (rule eventually_elim1, simp) huffman@31355: qed huffman@31355: huffman@31355: lemma BfunE: huffman@44195: assumes "Bfun f F" huffman@44195: obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) F" huffman@31355: using assms unfolding Bfun_def by fast huffman@31355: hoelzl@51531: lemma Cauchy_Bseq: "Cauchy X \ Bseq X" hoelzl@51531: unfolding Cauchy_def Bfun_metric_def eventually_sequentially hoelzl@51531: apply (erule_tac x=1 in allE) hoelzl@51531: apply simp hoelzl@51531: apply safe hoelzl@51531: apply (rule_tac x="X M" in exI) hoelzl@51531: apply (rule_tac x=1 in exI) hoelzl@51531: apply (erule_tac x=M in allE) hoelzl@51531: apply simp hoelzl@51531: apply (rule_tac x=M in exI) hoelzl@51531: apply (auto simp: dist_commute) hoelzl@51531: done hoelzl@51531: hoelzl@51531: hoelzl@51531: subsubsection {* Bounded Sequences *} hoelzl@51531: hoelzl@51531: lemma BseqI': "(\n. norm (X n) \ K) \ Bseq X" hoelzl@51531: by (intro BfunI) (auto simp: eventually_sequentially) hoelzl@51531: hoelzl@51531: lemma BseqI2': "\n\N. norm (X n) \ K \ Bseq X" hoelzl@51531: by (intro BfunI) (auto simp: eventually_sequentially) hoelzl@51531: hoelzl@51531: lemma Bseq_def: "Bseq X \ (\K>0. \n. norm (X n) \ K)" hoelzl@51531: unfolding Bfun_def eventually_sequentially hoelzl@51531: proof safe hoelzl@51531: fix N K assume "0 < K" "\n\N. norm (X n) \ K" hoelzl@51531: then show "\K>0. \n. norm (X n) \ K" haftmann@54863: by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2) hoelzl@51531: (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) hoelzl@51531: qed auto hoelzl@51531: hoelzl@51531: lemma BseqE: "\Bseq X; \K. \0 < K; \n. norm (X n) \ K\ \ Q\ \ Q" hoelzl@51531: unfolding Bseq_def by auto hoelzl@51531: hoelzl@51531: lemma BseqD: "Bseq X ==> \K. 0 < K & (\n. norm (X n) \ K)" hoelzl@51531: by (simp add: Bseq_def) hoelzl@51531: hoelzl@51531: lemma BseqI: "[| 0 < K; \n. norm (X n) \ K |] ==> Bseq X" hoelzl@51531: by (auto simp add: Bseq_def) hoelzl@51531: hoelzl@54263: lemma Bseq_bdd_above: "Bseq (X::nat \ real) \ bdd_above (range X)" hoelzl@54263: proof (elim BseqE, intro bdd_aboveI2) hoelzl@54263: fix K n assume "0 < K" "\n. norm (X n) \ K" then show "X n \ K" hoelzl@54263: by (auto elim!: allE[of _ n]) hoelzl@54263: qed hoelzl@54263: hoelzl@54263: lemma Bseq_bdd_below: "Bseq (X::nat \ real) \ bdd_below (range X)" hoelzl@54263: proof (elim BseqE, intro bdd_belowI2) hoelzl@54263: fix K n assume "0 < K" "\n. norm (X n) \ K" then show "- K \ X n" hoelzl@54263: by (auto elim!: allE[of _ n]) hoelzl@54263: qed hoelzl@54263: hoelzl@51531: lemma lemma_NBseq_def: hoelzl@51531: "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) \ real(Suc N))" hoelzl@51531: proof safe hoelzl@51531: fix K :: real hoelzl@51531: from reals_Archimedean2 obtain n :: nat where "K < real n" .. hoelzl@51531: then have "K \ real (Suc n)" by auto hoelzl@51531: moreover assume "\m. norm (X m) \ K" hoelzl@51531: ultimately have "\m. norm (X m) \ real (Suc n)" hoelzl@51531: by (blast intro: order_trans) hoelzl@51531: then show "\N. \n. norm (X n) \ real (Suc N)" .. hoelzl@51531: qed (force simp add: real_of_nat_Suc) hoelzl@51531: hoelzl@51531: text{* alternative definition for Bseq *} hoelzl@51531: lemma Bseq_iff: "Bseq X = (\N. \n. norm (X n) \ real(Suc N))" hoelzl@51531: apply (simp add: Bseq_def) hoelzl@51531: apply (simp (no_asm) add: lemma_NBseq_def) hoelzl@51531: done hoelzl@51531: hoelzl@51531: lemma lemma_NBseq_def2: hoelzl@51531: "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) < real(Suc N))" hoelzl@51531: apply (subst lemma_NBseq_def, auto) hoelzl@51531: apply (rule_tac x = "Suc N" in exI) hoelzl@51531: apply (rule_tac [2] x = N in exI) hoelzl@51531: apply (auto simp add: real_of_nat_Suc) hoelzl@51531: prefer 2 apply (blast intro: order_less_imp_le) hoelzl@51531: apply (drule_tac x = n in spec, simp) hoelzl@51531: done hoelzl@51531: hoelzl@51531: (* yet another definition for Bseq *) hoelzl@51531: lemma Bseq_iff1a: "Bseq X = (\N. \n. norm (X n) < real(Suc N))" hoelzl@51531: by (simp add: Bseq_def lemma_NBseq_def2) hoelzl@51531: hoelzl@51531: subsubsection{*A Few More Equivalence Theorems for Boundedness*} hoelzl@51531: hoelzl@51531: text{*alternative formulation for boundedness*} hoelzl@51531: lemma Bseq_iff2: "Bseq X = (\k > 0. \x. \n. norm (X(n) + -x) \ k)" hoelzl@51531: apply (unfold Bseq_def, safe) hoelzl@51531: apply (rule_tac [2] x = "k + norm x" in exI) hoelzl@51531: apply (rule_tac x = K in exI, simp) hoelzl@51531: apply (rule exI [where x = 0], auto) hoelzl@51531: apply (erule order_less_le_trans, simp) haftmann@54230: apply (drule_tac x=n in spec) hoelzl@51531: apply (drule order_trans [OF norm_triangle_ineq2]) hoelzl@51531: apply simp hoelzl@51531: done hoelzl@51531: hoelzl@51531: text{*alternative formulation for boundedness*} haftmann@53602: lemma Bseq_iff3: haftmann@53602: "Bseq X \ (\k>0. \N. \n. norm (X n + - X N) \ k)" (is "?P \ ?Q") haftmann@53602: proof haftmann@53602: assume ?P haftmann@53602: then obtain K haftmann@53602: where *: "0 < K" and **: "\n. norm (X n) \ K" by (auto simp add: Bseq_def) haftmann@53602: from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp haftmann@54230: from ** have "\n. norm (X n - X 0) \ K + norm (X 0)" haftmann@54230: by (auto intro: order_trans norm_triangle_ineq4) haftmann@54230: then have "\n. norm (X n + - X 0) \ K + norm (X 0)" haftmann@54230: by simp haftmann@54230: with `0 < K + norm (X 0)` show ?Q by blast haftmann@53602: next haftmann@53602: assume ?Q then show ?P by (auto simp add: Bseq_iff2) haftmann@53602: qed hoelzl@51531: hoelzl@51531: lemma BseqI2: "(\n. k \ f n & f n \ (K::real)) ==> Bseq f" hoelzl@51531: apply (simp add: Bseq_def) hoelzl@51531: apply (rule_tac x = " (\k\ + \K\) + 1" in exI, auto) hoelzl@51531: apply (drule_tac x = n in spec, arith) hoelzl@51531: done hoelzl@51531: haftmann@54230: hoelzl@51531: subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} hoelzl@51531: hoelzl@51531: lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X" hoelzl@51531: by (simp add: Bseq_def) hoelzl@51531: hoelzl@51531: lemma Bseq_eq_bounded: "range f \ {a .. b::real} \ Bseq f" hoelzl@51531: apply (simp add: subset_eq) hoelzl@51531: apply (rule BseqI'[where K="max (norm a) (norm b)"]) hoelzl@51531: apply (erule_tac x=n in allE) hoelzl@51531: apply auto hoelzl@51531: done hoelzl@51531: hoelzl@51531: lemma incseq_bounded: "incseq X \ \i. X i \ (B::real) \ Bseq X" hoelzl@51531: by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) hoelzl@51531: hoelzl@51531: lemma decseq_bounded: "decseq X \ \i. (B::real) \ X i \ Bseq X" hoelzl@51531: by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) hoelzl@51531: hoelzl@51531: subsection {* Bounded Monotonic Sequences *} hoelzl@51531: hoelzl@51531: subsubsection{*A Bounded and Monotonic Sequence Converges*} hoelzl@51531: hoelzl@51531: (* TODO: delete *) hoelzl@51531: (* FIXME: one use in NSA/HSEQ.thy *) hoelzl@51531: lemma Bmonoseq_LIMSEQ: "\n. m \ n --> X n = X m ==> \L. (X ----> L)" hoelzl@51531: apply (rule_tac x="X m" in exI) hoelzl@51531: apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const]) hoelzl@51531: unfolding eventually_sequentially hoelzl@51531: apply blast hoelzl@51531: done hoelzl@51531: huffman@31349: subsection {* Convergence to Zero *} huffman@31349: huffman@44081: definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" huffman@44195: where "Zfun f F = (\r>0. eventually (\x. norm (f x) < r) F)" huffman@31349: huffman@31349: lemma ZfunI: huffman@44195: "(\r. 0 < r \ eventually (\x. norm (f x) < r) F) \ Zfun f F" huffman@44081: unfolding Zfun_def by simp huffman@31349: huffman@31349: lemma ZfunD: huffman@44195: "\Zfun f F; 0 < r\ \ eventually (\x. norm (f x) < r) F" huffman@44081: unfolding Zfun_def by simp huffman@31349: huffman@31355: lemma Zfun_ssubst: huffman@44195: "eventually (\x. f x = g x) F \ Zfun g F \ Zfun f F" huffman@44081: unfolding Zfun_def by (auto elim!: eventually_rev_mp) huffman@31355: huffman@44195: lemma Zfun_zero: "Zfun (\x. 0) F" huffman@44081: unfolding Zfun_def by simp huffman@31349: huffman@44195: lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) F = Zfun (\x. f x) F" huffman@44081: unfolding Zfun_def by simp huffman@31349: huffman@31349: lemma Zfun_imp_Zfun: huffman@44195: assumes f: "Zfun f F" huffman@44195: assumes g: "eventually (\x. norm (g x) \ norm (f x) * K) F" huffman@44195: shows "Zfun (\x. g x) F" huffman@31349: proof (cases) huffman@31349: assume K: "0 < K" huffman@31349: show ?thesis huffman@31349: proof (rule ZfunI) huffman@31349: fix r::real assume "0 < r" nipkow@56541: hence "0 < r / K" using K by simp huffman@44195: then have "eventually (\x. norm (f x) < r / K) F" huffman@31487: using ZfunD [OF f] by fast huffman@44195: with g show "eventually (\x. norm (g x) < r) F" noschinl@46887: proof eventually_elim noschinl@46887: case (elim x) huffman@31487: hence "norm (f x) * K < r" huffman@31349: by (simp add: pos_less_divide_eq K) noschinl@46887: thus ?case noschinl@46887: by (simp add: order_le_less_trans [OF elim(1)]) huffman@31349: qed huffman@31349: qed huffman@31349: next huffman@31349: assume "\ 0 < K" huffman@31349: hence K: "K \ 0" by (simp only: not_less) huffman@31355: show ?thesis huffman@31355: proof (rule ZfunI) huffman@31355: fix r :: real huffman@31355: assume "0 < r" huffman@44195: from g show "eventually (\x. norm (g x) < r) F" noschinl@46887: proof eventually_elim noschinl@46887: case (elim x) noschinl@46887: also have "norm (f x) * K \ norm (f x) * 0" huffman@31355: using K norm_ge_zero by (rule mult_left_mono) noschinl@46887: finally show ?case huffman@31355: using `0 < r` by simp huffman@31355: qed huffman@31355: qed huffman@31349: qed huffman@31349: huffman@44195: lemma Zfun_le: "\Zfun g F; \x. norm (f x) \ norm (g x)\ \ Zfun f F" huffman@44081: by (erule_tac K="1" in Zfun_imp_Zfun, simp) huffman@31349: huffman@31349: lemma Zfun_add: huffman@44195: assumes f: "Zfun f F" and g: "Zfun g F" huffman@44195: shows "Zfun (\x. f x + g x) F" huffman@31349: proof (rule ZfunI) huffman@31349: fix r::real assume "0 < r" huffman@31349: hence r: "0 < r / 2" by simp huffman@44195: have "eventually (\x. norm (f x) < r/2) F" huffman@31487: using f r by (rule ZfunD) huffman@31349: moreover huffman@44195: have "eventually (\x. norm (g x) < r/2) F" huffman@31487: using g r by (rule ZfunD) huffman@31349: ultimately huffman@44195: show "eventually (\x. norm (f x + g x) < r) F" noschinl@46887: proof eventually_elim noschinl@46887: case (elim x) huffman@31487: have "norm (f x + g x) \ norm (f x) + norm (g x)" huffman@31349: by (rule norm_triangle_ineq) huffman@31349: also have "\ < r/2 + r/2" noschinl@46887: using elim by (rule add_strict_mono) noschinl@46887: finally show ?case huffman@31349: by simp huffman@31349: qed huffman@31349: qed huffman@31349: huffman@44195: lemma Zfun_minus: "Zfun f F \ Zfun (\x. - f x) F" huffman@44081: unfolding Zfun_def by simp huffman@31349: huffman@44195: lemma Zfun_diff: "\Zfun f F; Zfun g F\ \ Zfun (\x. f x - g x) F" haftmann@54230: using Zfun_add [of f F "\x. - g x"] by (simp add: Zfun_minus) huffman@31349: huffman@31349: lemma (in bounded_linear) Zfun: huffman@44195: assumes g: "Zfun g F" huffman@44195: shows "Zfun (\x. f (g x)) F" huffman@31349: proof - huffman@31349: obtain K where "\x. norm (f x) \ norm x * K" huffman@31349: using bounded by fast huffman@44195: then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) F" huffman@31355: by simp huffman@31487: with g show ?thesis huffman@31349: by (rule Zfun_imp_Zfun) huffman@31349: qed huffman@31349: huffman@31349: lemma (in bounded_bilinear) Zfun: huffman@44195: assumes f: "Zfun f F" huffman@44195: assumes g: "Zfun g F" huffman@44195: shows "Zfun (\x. f x ** g x) F" huffman@31349: proof (rule ZfunI) huffman@31349: fix r::real assume r: "0 < r" huffman@31349: obtain K where K: "0 < K" huffman@31349: and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" huffman@31349: using pos_bounded by fast huffman@31349: from K have K': "0 < inverse K" huffman@31349: by (rule positive_imp_inverse_positive) huffman@44195: have "eventually (\x. norm (f x) < r) F" huffman@31487: using f r by (rule ZfunD) huffman@31349: moreover huffman@44195: have "eventually (\x. norm (g x) < inverse K) F" huffman@31487: using g K' by (rule ZfunD) huffman@31349: ultimately huffman@44195: show "eventually (\x. norm (f x ** g x) < r) F" noschinl@46887: proof eventually_elim noschinl@46887: case (elim x) huffman@31487: have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" huffman@31349: by (rule norm_le) huffman@31487: also have "norm (f x) * norm (g x) * K < r * inverse K * K" noschinl@46887: by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) huffman@31349: also from K have "r * inverse K * K = r" huffman@31349: by simp noschinl@46887: finally show ?case . huffman@31349: qed huffman@31349: qed huffman@31349: huffman@31349: lemma (in bounded_bilinear) Zfun_left: huffman@44195: "Zfun f F \ Zfun (\x. f x ** a) F" huffman@44081: by (rule bounded_linear_left [THEN bounded_linear.Zfun]) huffman@31349: huffman@31349: lemma (in bounded_bilinear) Zfun_right: huffman@44195: "Zfun f F \ Zfun (\x. a ** f x) F" huffman@44081: by (rule bounded_linear_right [THEN bounded_linear.Zfun]) huffman@31349: huffman@44282: lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] huffman@44282: lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] huffman@44282: lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] huffman@31349: huffman@44195: lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\x. f x - a) F" huffman@44081: by (simp only: tendsto_iff Zfun_def dist_norm) huffman@31349: lp15@56366: lemma tendsto_0_le: "\(f ---> 0) F; eventually (\x. norm (g x) \ norm (f x) * K) F\ lp15@56366: \ (g ---> 0) F" lp15@56366: by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) lp15@56366: huffman@44205: subsubsection {* Distance and norms *} huffman@36662: hoelzl@51531: lemma tendsto_dist [tendsto_intros]: hoelzl@51531: fixes l m :: "'a :: metric_space" hoelzl@51531: assumes f: "(f ---> l) F" and g: "(g ---> m) F" hoelzl@51531: shows "((\x. dist (f x) (g x)) ---> dist l m) F" hoelzl@51531: proof (rule tendstoI) hoelzl@51531: fix e :: real assume "0 < e" hoelzl@51531: hence e2: "0 < e/2" by simp hoelzl@51531: from tendstoD [OF f e2] tendstoD [OF g e2] hoelzl@51531: show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) F" hoelzl@51531: proof (eventually_elim) hoelzl@51531: case (elim x) hoelzl@51531: then show "dist (dist (f x) (g x)) (dist l m) < e" hoelzl@51531: unfolding dist_real_def hoelzl@51531: using dist_triangle2 [of "f x" "g x" "l"] hoelzl@51531: using dist_triangle2 [of "g x" "l" "m"] hoelzl@51531: using dist_triangle3 [of "l" "m" "f x"] hoelzl@51531: using dist_triangle [of "f x" "m" "g x"] hoelzl@51531: by arith hoelzl@51531: qed hoelzl@51531: qed hoelzl@51531: hoelzl@51531: lemma continuous_dist[continuous_intros]: hoelzl@51531: fixes f g :: "_ \ 'a :: metric_space" hoelzl@51531: shows "continuous F f \ continuous F g \ continuous F (\x. dist (f x) (g x))" hoelzl@51531: unfolding continuous_def by (rule tendsto_dist) hoelzl@51531: hoelzl@56371: lemma continuous_on_dist[continuous_intros]: hoelzl@51531: fixes f g :: "_ \ 'a :: metric_space" hoelzl@51531: shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. dist (f x) (g x))" hoelzl@51531: unfolding continuous_on_def by (auto intro: tendsto_dist) hoelzl@51531: huffman@31565: lemma tendsto_norm [tendsto_intros]: huffman@44195: "(f ---> a) F \ ((\x. norm (f x)) ---> norm a) F" huffman@44081: unfolding norm_conv_dist by (intro tendsto_intros) huffman@36662: hoelzl@51478: lemma continuous_norm [continuous_intros]: hoelzl@51478: "continuous F f \ continuous F (\x. norm (f x))" hoelzl@51478: unfolding continuous_def by (rule tendsto_norm) hoelzl@51478: hoelzl@56371: lemma continuous_on_norm [continuous_intros]: hoelzl@51478: "continuous_on s f \ continuous_on s (\x. norm (f x))" hoelzl@51478: unfolding continuous_on_def by (auto intro: tendsto_norm) hoelzl@51478: huffman@36662: lemma tendsto_norm_zero: huffman@44195: "(f ---> 0) F \ ((\x. norm (f x)) ---> 0) F" huffman@44081: by (drule tendsto_norm, simp) huffman@36662: huffman@36662: lemma tendsto_norm_zero_cancel: huffman@44195: "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" huffman@44081: unfolding tendsto_iff dist_norm by simp huffman@36662: huffman@36662: lemma tendsto_norm_zero_iff: huffman@44195: "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" huffman@44081: unfolding tendsto_iff dist_norm by simp huffman@31349: huffman@44194: lemma tendsto_rabs [tendsto_intros]: huffman@44195: "(f ---> (l::real)) F \ ((\x. \f x\) ---> \l\) F" huffman@44194: by (fold real_norm_def, rule tendsto_norm) huffman@44194: hoelzl@51478: lemma continuous_rabs [continuous_intros]: hoelzl@51478: "continuous F f \ continuous F (\x. \f x :: real\)" hoelzl@51478: unfolding real_norm_def[symmetric] by (rule continuous_norm) hoelzl@51478: hoelzl@56371: lemma continuous_on_rabs [continuous_intros]: hoelzl@51478: "continuous_on s f \ continuous_on s (\x. \f x :: real\)" hoelzl@51478: unfolding real_norm_def[symmetric] by (rule continuous_on_norm) hoelzl@51478: huffman@44194: lemma tendsto_rabs_zero: huffman@44195: "(f ---> (0::real)) F \ ((\x. \f x\) ---> 0) F" huffman@44194: by (fold real_norm_def, rule tendsto_norm_zero) huffman@44194: huffman@44194: lemma tendsto_rabs_zero_cancel: huffman@44195: "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" huffman@44194: by (fold real_norm_def, rule tendsto_norm_zero_cancel) huffman@44194: huffman@44194: lemma tendsto_rabs_zero_iff: huffman@44195: "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" huffman@44194: by (fold real_norm_def, rule tendsto_norm_zero_iff) huffman@44194: huffman@44194: subsubsection {* Addition and subtraction *} huffman@44194: huffman@31565: lemma tendsto_add [tendsto_intros]: huffman@31349: fixes a b :: "'a::real_normed_vector" huffman@44195: shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x + g x) ---> a + b) F" huffman@44081: by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) huffman@31349: hoelzl@51478: lemma continuous_add [continuous_intros]: hoelzl@51478: fixes f g :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51478: shows "continuous F f \ continuous F g \ continuous F (\x. f x + g x)" hoelzl@51478: unfolding continuous_def by (rule tendsto_add) hoelzl@51478: hoelzl@56371: lemma continuous_on_add [continuous_intros]: hoelzl@51478: fixes f g :: "_ \ 'b::real_normed_vector" hoelzl@51478: shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x + g x)" hoelzl@51478: unfolding continuous_on_def by (auto intro: tendsto_add) hoelzl@51478: huffman@44194: lemma tendsto_add_zero: hoelzl@51478: fixes f g :: "_ \ 'b::real_normed_vector" huffman@44195: shows "\(f ---> 0) F; (g ---> 0) F\ \ ((\x. f x + g x) ---> 0) F" huffman@44194: by (drule (1) tendsto_add, simp) huffman@44194: huffman@31565: lemma tendsto_minus [tendsto_intros]: huffman@31349: fixes a :: "'a::real_normed_vector" huffman@44195: shows "(f ---> a) F \ ((\x. - f x) ---> - a) F" huffman@44081: by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) huffman@31349: hoelzl@51478: lemma continuous_minus [continuous_intros]: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51478: shows "continuous F f \ continuous F (\x. - f x)" hoelzl@51478: unfolding continuous_def by (rule tendsto_minus) hoelzl@51478: hoelzl@56371: lemma continuous_on_minus [continuous_intros]: hoelzl@51478: fixes f :: "_ \ 'b::real_normed_vector" hoelzl@51478: shows "continuous_on s f \ continuous_on s (\x. - f x)" hoelzl@51478: unfolding continuous_on_def by (auto intro: tendsto_minus) hoelzl@51478: huffman@31349: lemma tendsto_minus_cancel: huffman@31349: fixes a :: "'a::real_normed_vector" huffman@44195: shows "((\x. - f x) ---> - a) F \ (f ---> a) F" huffman@44081: by (drule tendsto_minus, simp) huffman@31349: hoelzl@50330: lemma tendsto_minus_cancel_left: hoelzl@50330: "(f ---> - (y::_::real_normed_vector)) F \ ((\x. - f x) ---> y) F" hoelzl@50330: using tendsto_minus_cancel[of f "- y" F] tendsto_minus[of f "- y" F] hoelzl@50330: by auto hoelzl@50330: huffman@31565: lemma tendsto_diff [tendsto_intros]: huffman@31349: fixes a b :: "'a::real_normed_vector" huffman@44195: shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x - g x) ---> a - b) F" haftmann@54230: using tendsto_add [of f a F "\x. - g x" "- b"] by (simp add: tendsto_minus) huffman@31349: hoelzl@51478: lemma continuous_diff [continuous_intros]: hoelzl@51478: fixes f g :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51478: shows "continuous F f \ continuous F g \ continuous F (\x. f x - g x)" hoelzl@51478: unfolding continuous_def by (rule tendsto_diff) hoelzl@51478: hoelzl@56371: lemma continuous_on_diff [continuous_intros]: hoelzl@51478: fixes f g :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51478: shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" hoelzl@51478: unfolding continuous_on_def by (auto intro: tendsto_diff) hoelzl@51478: huffman@31588: lemma tendsto_setsum [tendsto_intros]: huffman@31588: fixes f :: "'a \ 'b \ 'c::real_normed_vector" huffman@44195: assumes "\i. i \ S \ (f i ---> a i) F" huffman@44195: shows "((\x. \i\S. f i x) ---> (\i\S. a i)) F" huffman@31588: proof (cases "finite S") huffman@31588: assume "finite S" thus ?thesis using assms huffman@44194: by (induct, simp add: tendsto_const, simp add: tendsto_add) huffman@31588: next huffman@31588: assume "\ finite S" thus ?thesis huffman@31588: by (simp add: tendsto_const) huffman@31588: qed huffman@31588: hoelzl@51478: lemma continuous_setsum [continuous_intros]: hoelzl@51478: fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" hoelzl@51478: shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)" hoelzl@51478: unfolding continuous_def by (rule tendsto_setsum) hoelzl@51478: hoelzl@51478: lemma continuous_on_setsum [continuous_intros]: hoelzl@51478: fixes f :: "'a \ _ \ 'c::real_normed_vector" hoelzl@51478: shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)" hoelzl@51478: unfolding continuous_on_def by (auto intro: tendsto_setsum) hoelzl@51478: hoelzl@50999: lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real] hoelzl@50999: huffman@44194: subsubsection {* Linear operators and multiplication *} huffman@44194: huffman@44282: lemma (in bounded_linear) tendsto: huffman@44195: "(g ---> a) F \ ((\x. f (g x)) ---> f a) F" huffman@44081: by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) huffman@31349: hoelzl@51478: lemma (in bounded_linear) continuous: hoelzl@51478: "continuous F g \ continuous F (\x. f (g x))" hoelzl@51478: using tendsto[of g _ F] by (auto simp: continuous_def) hoelzl@51478: hoelzl@51478: lemma (in bounded_linear) continuous_on: hoelzl@51478: "continuous_on s g \ continuous_on s (\x. f (g x))" hoelzl@51478: using tendsto[of g] by (auto simp: continuous_on_def) hoelzl@51478: huffman@44194: lemma (in bounded_linear) tendsto_zero: huffman@44195: "(g ---> 0) F \ ((\x. f (g x)) ---> 0) F" huffman@44194: by (drule tendsto, simp only: zero) huffman@44194: huffman@44282: lemma (in bounded_bilinear) tendsto: huffman@44195: "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x ** g x) ---> a ** b) F" huffman@44081: by (simp only: tendsto_Zfun_iff prod_diff_prod huffman@44081: Zfun_add Zfun Zfun_left Zfun_right) huffman@31349: hoelzl@51478: lemma (in bounded_bilinear) continuous: hoelzl@51478: "continuous F f \ continuous F g \ continuous F (\x. f x ** g x)" hoelzl@51478: using tendsto[of f _ F g] by (auto simp: continuous_def) hoelzl@51478: hoelzl@51478: lemma (in bounded_bilinear) continuous_on: hoelzl@51478: "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x ** g x)" hoelzl@51478: using tendsto[of f _ _ g] by (auto simp: continuous_on_def) hoelzl@51478: huffman@44194: lemma (in bounded_bilinear) tendsto_zero: huffman@44195: assumes f: "(f ---> 0) F" huffman@44195: assumes g: "(g ---> 0) F" huffman@44195: shows "((\x. f x ** g x) ---> 0) F" huffman@44194: using tendsto [OF f g] by (simp add: zero_left) huffman@31355: huffman@44194: lemma (in bounded_bilinear) tendsto_left_zero: huffman@44195: "(f ---> 0) F \ ((\x. f x ** c) ---> 0) F" huffman@44194: by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) huffman@44194: huffman@44194: lemma (in bounded_bilinear) tendsto_right_zero: huffman@44195: "(f ---> 0) F \ ((\x. c ** f x) ---> 0) F" huffman@44194: by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) huffman@44194: huffman@44282: lemmas tendsto_of_real [tendsto_intros] = huffman@44282: bounded_linear.tendsto [OF bounded_linear_of_real] huffman@44282: huffman@44282: lemmas tendsto_scaleR [tendsto_intros] = huffman@44282: bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] huffman@44282: huffman@44282: lemmas tendsto_mult [tendsto_intros] = huffman@44282: bounded_bilinear.tendsto [OF bounded_bilinear_mult] huffman@44194: hoelzl@51478: lemmas continuous_of_real [continuous_intros] = hoelzl@51478: bounded_linear.continuous [OF bounded_linear_of_real] hoelzl@51478: hoelzl@51478: lemmas continuous_scaleR [continuous_intros] = hoelzl@51478: bounded_bilinear.continuous [OF bounded_bilinear_scaleR] hoelzl@51478: hoelzl@51478: lemmas continuous_mult [continuous_intros] = hoelzl@51478: bounded_bilinear.continuous [OF bounded_bilinear_mult] hoelzl@51478: hoelzl@56371: lemmas continuous_on_of_real [continuous_intros] = hoelzl@51478: bounded_linear.continuous_on [OF bounded_linear_of_real] hoelzl@51478: hoelzl@56371: lemmas continuous_on_scaleR [continuous_intros] = hoelzl@51478: bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR] hoelzl@51478: hoelzl@56371: lemmas continuous_on_mult [continuous_intros] = hoelzl@51478: bounded_bilinear.continuous_on [OF bounded_bilinear_mult] hoelzl@51478: huffman@44568: lemmas tendsto_mult_zero = huffman@44568: bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] huffman@44568: huffman@44568: lemmas tendsto_mult_left_zero = huffman@44568: bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] huffman@44568: huffman@44568: lemmas tendsto_mult_right_zero = huffman@44568: bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] huffman@44568: huffman@44194: lemma tendsto_power [tendsto_intros]: huffman@44194: fixes f :: "'a \ 'b::{power,real_normed_algebra}" huffman@44195: shows "(f ---> a) F \ ((\x. f x ^ n) ---> a ^ n) F" huffman@44194: by (induct n) (simp_all add: tendsto_const tendsto_mult) huffman@44194: hoelzl@51478: lemma continuous_power [continuous_intros]: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" hoelzl@51478: shows "continuous F f \ continuous F (\x. (f x)^n)" hoelzl@51478: unfolding continuous_def by (rule tendsto_power) hoelzl@51478: hoelzl@56371: lemma continuous_on_power [continuous_intros]: hoelzl@51478: fixes f :: "_ \ 'b::{power,real_normed_algebra}" hoelzl@51478: shows "continuous_on s f \ continuous_on s (\x. (f x)^n)" hoelzl@51478: unfolding continuous_on_def by (auto intro: tendsto_power) hoelzl@51478: huffman@44194: lemma tendsto_setprod [tendsto_intros]: huffman@44194: fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}" huffman@44195: assumes "\i. i \ S \ (f i ---> L i) F" huffman@44195: shows "((\x. \i\S. f i x) ---> (\i\S. L i)) F" huffman@44194: proof (cases "finite S") huffman@44194: assume "finite S" thus ?thesis using assms huffman@44194: by (induct, simp add: tendsto_const, simp add: tendsto_mult) huffman@44194: next huffman@44194: assume "\ finite S" thus ?thesis huffman@44194: by (simp add: tendsto_const) huffman@44194: qed huffman@44194: hoelzl@51478: lemma continuous_setprod [continuous_intros]: hoelzl@51478: fixes f :: "'a \ 'b::t2_space \ 'c::{real_normed_algebra,comm_ring_1}" hoelzl@51478: shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)" hoelzl@51478: unfolding continuous_def by (rule tendsto_setprod) hoelzl@51478: hoelzl@51478: lemma continuous_on_setprod [continuous_intros]: hoelzl@51478: fixes f :: "'a \ _ \ 'c::{real_normed_algebra,comm_ring_1}" hoelzl@51478: shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)" hoelzl@51478: unfolding continuous_on_def by (auto intro: tendsto_setprod) hoelzl@51478: huffman@44194: subsubsection {* Inverse and division *} huffman@31355: huffman@31355: lemma (in bounded_bilinear) Zfun_prod_Bfun: huffman@44195: assumes f: "Zfun f F" huffman@44195: assumes g: "Bfun g F" huffman@44195: shows "Zfun (\x. f x ** g x) F" huffman@31355: proof - huffman@31355: obtain K where K: "0 \ K" huffman@31355: and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" huffman@31355: using nonneg_bounded by fast huffman@31355: obtain B where B: "0 < B" huffman@44195: and norm_g: "eventually (\x. norm (g x) \ B) F" huffman@31487: using g by (rule BfunE) huffman@44195: have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) F" noschinl@46887: using norm_g proof eventually_elim noschinl@46887: case (elim x) huffman@31487: have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" huffman@31355: by (rule norm_le) huffman@31487: also have "\ \ norm (f x) * B * K" huffman@31487: by (intro mult_mono' order_refl norm_g norm_ge_zero noschinl@46887: mult_nonneg_nonneg K elim) huffman@31487: also have "\ = norm (f x) * (B * K)" haftmann@57512: by (rule mult.assoc) huffman@31487: finally show "norm (f x ** g x) \ norm (f x) * (B * K)" . huffman@31355: qed huffman@31487: with f show ?thesis huffman@31487: by (rule Zfun_imp_Zfun) huffman@31355: qed huffman@31355: huffman@31355: lemma (in bounded_bilinear) flip: huffman@31355: "bounded_bilinear (\x y. y ** x)" huffman@44081: apply default huffman@44081: apply (rule add_right) huffman@44081: apply (rule add_left) huffman@44081: apply (rule scaleR_right) huffman@44081: apply (rule scaleR_left) haftmann@57512: apply (subst mult.commute) huffman@44081: using bounded by fast huffman@31355: huffman@31355: lemma (in bounded_bilinear) Bfun_prod_Zfun: huffman@44195: assumes f: "Bfun f F" huffman@44195: assumes g: "Zfun g F" huffman@44195: shows "Zfun (\x. f x ** g x) F" huffman@44081: using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) huffman@31355: huffman@31355: lemma Bfun_inverse_lemma: huffman@31355: fixes x :: "'a::real_normed_div_algebra" huffman@31355: shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" huffman@44081: apply (subst nonzero_norm_inverse, clarsimp) huffman@44081: apply (erule (1) le_imp_inverse_le) huffman@44081: done huffman@31355: huffman@31355: lemma Bfun_inverse: huffman@31355: fixes a :: "'a::real_normed_div_algebra" huffman@44195: assumes f: "(f ---> a) F" huffman@31355: assumes a: "a \ 0" huffman@44195: shows "Bfun (\x. inverse (f x)) F" huffman@31355: proof - huffman@31355: from a have "0 < norm a" by simp huffman@31355: hence "\r>0. r < norm a" by (rule dense) huffman@31355: then obtain r where r1: "0 < r" and r2: "r < norm a" by fast huffman@44195: have "eventually (\x. dist (f x) a < r) F" huffman@31487: using tendstoD [OF f r1] by fast huffman@44195: hence "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) F" noschinl@46887: proof eventually_elim noschinl@46887: case (elim x) huffman@31487: hence 1: "norm (f x - a) < r" huffman@31355: by (simp add: dist_norm) huffman@31487: hence 2: "f x \ 0" using r2 by auto huffman@31487: hence "norm (inverse (f x)) = inverse (norm (f x))" huffman@31355: by (rule nonzero_norm_inverse) huffman@31355: also have "\ \ inverse (norm a - r)" huffman@31355: proof (rule le_imp_inverse_le) huffman@31355: show "0 < norm a - r" using r2 by simp huffman@31355: next huffman@31487: have "norm a - norm (f x) \ norm (a - f x)" huffman@31355: by (rule norm_triangle_ineq2) huffman@31487: also have "\ = norm (f x - a)" huffman@31355: by (rule norm_minus_commute) huffman@31355: also have "\ < r" using 1 . huffman@31487: finally show "norm a - r \ norm (f x)" by simp huffman@31355: qed huffman@31487: finally show "norm (inverse (f x)) \ inverse (norm a - r)" . huffman@31355: qed huffman@31355: thus ?thesis by (rule BfunI) huffman@31355: qed huffman@31355: huffman@31565: lemma tendsto_inverse [tendsto_intros]: huffman@31355: fixes a :: "'a::real_normed_div_algebra" huffman@44195: assumes f: "(f ---> a) F" huffman@31355: assumes a: "a \ 0" huffman@44195: shows "((\x. inverse (f x)) ---> inverse a) F" huffman@31355: proof - huffman@31355: from a have "0 < norm a" by simp huffman@44195: with f have "eventually (\x. dist (f x) a < norm a) F" huffman@31355: by (rule tendstoD) huffman@44195: then have "eventually (\x. f x \ 0) F" huffman@31355: unfolding dist_norm by (auto elim!: eventually_elim1) huffman@44627: with a have "eventually (\x. inverse (f x) - inverse a = huffman@44627: - (inverse (f x) * (f x - a) * inverse a)) F" huffman@44627: by (auto elim!: eventually_elim1 simp: inverse_diff_inverse) huffman@44627: moreover have "Zfun (\x. - (inverse (f x) * (f x - a) * inverse a)) F" huffman@44627: by (intro Zfun_minus Zfun_mult_left huffman@44627: bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] huffman@44627: Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff]) huffman@44627: ultimately show ?thesis huffman@44627: unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) huffman@31355: qed huffman@31355: hoelzl@51478: lemma continuous_inverse: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" hoelzl@51478: assumes "continuous F f" and "f (Lim F (\x. x)) \ 0" hoelzl@51478: shows "continuous F (\x. inverse (f x))" hoelzl@51478: using assms unfolding continuous_def by (rule tendsto_inverse) hoelzl@51478: hoelzl@51478: lemma continuous_at_within_inverse[continuous_intros]: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" hoelzl@51478: assumes "continuous (at a within s) f" and "f a \ 0" hoelzl@51478: shows "continuous (at a within s) (\x. inverse (f x))" hoelzl@51478: using assms unfolding continuous_within by (rule tendsto_inverse) hoelzl@51478: hoelzl@51478: lemma isCont_inverse[continuous_intros, simp]: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" hoelzl@51478: assumes "isCont f a" and "f a \ 0" hoelzl@51478: shows "isCont (\x. inverse (f x)) a" hoelzl@51478: using assms unfolding continuous_at by (rule tendsto_inverse) hoelzl@51478: hoelzl@56371: lemma continuous_on_inverse[continuous_intros]: hoelzl@51478: fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" hoelzl@51478: assumes "continuous_on s f" and "\x\s. f x \ 0" hoelzl@51478: shows "continuous_on s (\x. inverse (f x))" hoelzl@51478: using assms unfolding continuous_on_def by (fast intro: tendsto_inverse) hoelzl@51478: huffman@31565: lemma tendsto_divide [tendsto_intros]: huffman@31355: fixes a b :: "'a::real_normed_field" huffman@44195: shows "\(f ---> a) F; (g ---> b) F; b \ 0\ huffman@44195: \ ((\x. f x / g x) ---> a / b) F" huffman@44282: by (simp add: tendsto_mult tendsto_inverse divide_inverse) huffman@31355: hoelzl@51478: lemma continuous_divide: hoelzl@51478: fixes f g :: "'a::t2_space \ 'b::real_normed_field" hoelzl@51478: assumes "continuous F f" and "continuous F g" and "g (Lim F (\x. x)) \ 0" hoelzl@51478: shows "continuous F (\x. (f x) / (g x))" hoelzl@51478: using assms unfolding continuous_def by (rule tendsto_divide) hoelzl@51478: hoelzl@51478: lemma continuous_at_within_divide[continuous_intros]: hoelzl@51478: fixes f g :: "'a::t2_space \ 'b::real_normed_field" hoelzl@51478: assumes "continuous (at a within s) f" "continuous (at a within s) g" and "g a \ 0" hoelzl@51478: shows "continuous (at a within s) (\x. (f x) / (g x))" hoelzl@51478: using assms unfolding continuous_within by (rule tendsto_divide) hoelzl@51478: hoelzl@51478: lemma isCont_divide[continuous_intros, simp]: hoelzl@51478: fixes f g :: "'a::t2_space \ 'b::real_normed_field" hoelzl@51478: assumes "isCont f a" "isCont g a" "g a \ 0" hoelzl@51478: shows "isCont (\x. (f x) / g x) a" hoelzl@51478: using assms unfolding continuous_at by (rule tendsto_divide) hoelzl@51478: hoelzl@56371: lemma continuous_on_divide[continuous_intros]: hoelzl@51478: fixes f :: "'a::topological_space \ 'b::real_normed_field" hoelzl@51478: assumes "continuous_on s f" "continuous_on s g" and "\x\s. g x \ 0" hoelzl@51478: shows "continuous_on s (\x. (f x) / (g x))" hoelzl@51478: using assms unfolding continuous_on_def by (fast intro: tendsto_divide) hoelzl@51478: huffman@44194: lemma tendsto_sgn [tendsto_intros]: huffman@44194: fixes l :: "'a::real_normed_vector" huffman@44195: shows "\(f ---> l) F; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) F" huffman@44194: unfolding sgn_div_norm by (simp add: tendsto_intros) huffman@44194: hoelzl@51478: lemma continuous_sgn: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51478: assumes "continuous F f" and "f (Lim F (\x. x)) \ 0" hoelzl@51478: shows "continuous F (\x. sgn (f x))" hoelzl@51478: using assms unfolding continuous_def by (rule tendsto_sgn) hoelzl@51478: hoelzl@51478: lemma continuous_at_within_sgn[continuous_intros]: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51478: assumes "continuous (at a within s) f" and "f a \ 0" hoelzl@51478: shows "continuous (at a within s) (\x. sgn (f x))" hoelzl@51478: using assms unfolding continuous_within by (rule tendsto_sgn) hoelzl@51478: hoelzl@51478: lemma isCont_sgn[continuous_intros]: hoelzl@51478: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51478: assumes "isCont f a" and "f a \ 0" hoelzl@51478: shows "isCont (\x. sgn (f x)) a" hoelzl@51478: using assms unfolding continuous_at by (rule tendsto_sgn) hoelzl@51478: hoelzl@56371: lemma continuous_on_sgn[continuous_intros]: hoelzl@51478: fixes f :: "'a::topological_space \ 'b::real_normed_vector" hoelzl@51478: assumes "continuous_on s f" and "\x\s. f x \ 0" hoelzl@51478: shows "continuous_on s (\x. sgn (f x))" hoelzl@51478: using assms unfolding continuous_on_def by (fast intro: tendsto_sgn) hoelzl@51478: hoelzl@50325: lemma filterlim_at_infinity: hoelzl@50325: fixes f :: "_ \ 'a\real_normed_vector" hoelzl@50325: assumes "0 \ c" hoelzl@50325: shows "(LIM x F. f x :> at_infinity) \ (\r>c. eventually (\x. r \ norm (f x)) F)" hoelzl@50325: unfolding filterlim_iff eventually_at_infinity hoelzl@50325: proof safe hoelzl@50325: fix P :: "'a \ bool" and b hoelzl@50325: assume *: "\r>c. eventually (\x. r \ norm (f x)) F" hoelzl@50325: and P: "\x. b \ norm x \ P x" hoelzl@50325: have "max b (c + 1) > c" by auto hoelzl@50325: with * have "eventually (\x. max b (c + 1) \ norm (f x)) F" hoelzl@50325: by auto hoelzl@50325: then show "eventually (\x. P (f x)) F" hoelzl@50325: proof eventually_elim hoelzl@50325: fix x assume "max b (c + 1) \ norm (f x)" hoelzl@50325: with P show "P (f x)" by auto hoelzl@50325: qed hoelzl@50325: qed force hoelzl@50325: hoelzl@51529: hoelzl@50347: subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *} hoelzl@50347: hoelzl@50347: text {* hoelzl@50347: hoelzl@50347: This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and hoelzl@50347: @{term "at_right x"} and also @{term "at_right 0"}. hoelzl@50347: hoelzl@50347: *} hoelzl@50347: hoelzl@51471: lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real] hoelzl@50323: hoelzl@51641: lemma filtermap_homeomorph: hoelzl@51641: assumes f: "continuous (at a) f" hoelzl@51641: assumes g: "continuous (at (f a)) g" hoelzl@51641: assumes bij1: "\x. f (g x) = x" and bij2: "\x. g (f x) = x" hoelzl@51641: shows "filtermap f (nhds a) = nhds (f a)" hoelzl@51641: unfolding filter_eq_iff eventually_filtermap eventually_nhds hoelzl@51641: proof safe hoelzl@51641: fix P S assume S: "open S" "f a \ S" and P: "\x\S. P x" hoelzl@51641: from continuous_within_topological[THEN iffD1, rule_format, OF f S] P hoelzl@51641: show "\S. open S \ a \ S \ (\x\S. P (f x))" by auto hoelzl@51641: next hoelzl@51641: fix P S assume S: "open S" "a \ S" and P: "\x\S. P (f x)" hoelzl@51641: with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2 hoelzl@51641: obtain A where "open A" "f a \ A" "(\y\A. g y \ S)" hoelzl@51641: by (metis UNIV_I) hoelzl@51641: with P bij1 show "\S. open S \ f a \ S \ (\x\S. P x)" hoelzl@51641: by (force intro!: exI[of _ A]) hoelzl@51641: qed hoelzl@50347: hoelzl@51641: lemma filtermap_nhds_shift: "filtermap (\x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)" hoelzl@51641: by (rule filtermap_homeomorph[where g="\x. x + d"]) (auto intro: continuous_intros) hoelzl@50347: hoelzl@51641: lemma filtermap_nhds_minus: "filtermap (\x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)" hoelzl@51641: by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus) hoelzl@51641: hoelzl@51641: lemma filtermap_at_shift: "filtermap (\x. x - d) (at a) = at (a - d::'a::real_normed_vector)" hoelzl@51641: by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) hoelzl@50347: hoelzl@50347: lemma filtermap_at_right_shift: "filtermap (\x. x - d) (at_right a) = at_right (a - d::real)" hoelzl@51641: by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) hoelzl@50323: hoelzl@50347: lemma at_right_to_0: "at_right (a::real) = filtermap (\x. x + a) (at_right 0)" hoelzl@50347: using filtermap_at_right_shift[of "-a" 0] by simp hoelzl@50347: hoelzl@50347: lemma filterlim_at_right_to_0: hoelzl@50347: "filterlim f F (at_right (a::real)) \ filterlim (\x. f (x + a)) F (at_right 0)" hoelzl@50347: unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] .. hoelzl@50347: hoelzl@50347: lemma eventually_at_right_to_0: hoelzl@50347: "eventually P (at_right (a::real)) \ eventually (\x. P (x + a)) (at_right 0)" hoelzl@50347: unfolding at_right_to_0[of a] by (simp add: eventually_filtermap) hoelzl@50347: hoelzl@51641: lemma filtermap_at_minus: "filtermap (\x. - x) (at a) = at (- a::'a::real_normed_vector)" hoelzl@51641: by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) hoelzl@50347: hoelzl@50347: lemma at_left_minus: "at_left (a::real) = filtermap (\x. - x) (at_right (- a))" hoelzl@51641: by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) hoelzl@50323: hoelzl@50347: lemma at_right_minus: "at_right (a::real) = filtermap (\x. - x) (at_left (- a))" hoelzl@51641: by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) hoelzl@50347: hoelzl@50347: lemma filterlim_at_left_to_right: hoelzl@50347: "filterlim f F (at_left (a::real)) \ filterlim (\x. f (- x)) F (at_right (-a))" hoelzl@50347: unfolding filterlim_def filtermap_filtermap at_left_minus[of a] .. hoelzl@50347: hoelzl@50347: lemma eventually_at_left_to_right: hoelzl@50347: "eventually P (at_left (a::real)) \ eventually (\x. P (- x)) (at_right (-a))" hoelzl@50347: unfolding at_left_minus[of a] by (simp add: eventually_filtermap) hoelzl@50347: hoelzl@50346: lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)" hoelzl@50346: unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder hoelzl@50346: by (metis le_minus_iff minus_minus) hoelzl@50346: hoelzl@50346: lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)" hoelzl@50346: unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident) hoelzl@50346: hoelzl@50346: lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \ (LIM x at_bot. f (-x::real) :> F)" hoelzl@50346: unfolding filterlim_def at_top_mirror filtermap_filtermap .. hoelzl@50346: hoelzl@50346: lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \ (LIM x at_top. f (-x::real) :> F)" hoelzl@50346: unfolding filterlim_def at_bot_mirror filtermap_filtermap .. hoelzl@50346: hoelzl@50323: lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top" hoelzl@50323: unfolding filterlim_at_top eventually_at_bot_dense hoelzl@50346: by (metis leI minus_less_iff order_less_asym) hoelzl@50323: hoelzl@50323: lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot" hoelzl@50323: unfolding filterlim_at_bot eventually_at_top_dense hoelzl@50346: by (metis leI less_minus_iff order_less_asym) hoelzl@50323: hoelzl@50346: lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \ (LIM x F. - (f x) :: real :> at_bot)" hoelzl@50346: using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F] hoelzl@50346: using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\x. - f x" F] hoelzl@50346: by auto hoelzl@50346: hoelzl@50346: lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \ (LIM x F. - (f x) :: real :> at_top)" hoelzl@50346: unfolding filterlim_uminus_at_top by simp hoelzl@50323: hoelzl@50347: lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top" hoelzl@51641: unfolding filterlim_at_top_gt[where c=0] eventually_at_filter hoelzl@50347: proof safe hoelzl@50347: fix Z :: real assume [arith]: "0 < Z" hoelzl@50347: then have "eventually (\x. x < inverse Z) (nhds 0)" hoelzl@50347: by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\inverse Z\"]) hoelzl@51641: then show "eventually (\x. x \ 0 \ x \ {0<..} \ Z \ inverse x) (nhds 0)" hoelzl@50347: by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps) hoelzl@50347: qed hoelzl@50347: hoelzl@50347: lemma filterlim_inverse_at_top: hoelzl@50347: "(f ---> (0 :: real)) F \ eventually (\x. 0 < f x) F \ LIM x F. inverse (f x) :> at_top" hoelzl@50347: by (intro filterlim_compose[OF filterlim_inverse_at_top_right]) hoelzl@51641: (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal) hoelzl@50347: hoelzl@50347: lemma filterlim_inverse_at_bot_neg: hoelzl@50347: "LIM x (at_left (0::real)). inverse x :> at_bot" hoelzl@50347: by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right) hoelzl@50347: hoelzl@50347: lemma filterlim_inverse_at_bot: hoelzl@50347: "(f ---> (0 :: real)) F \ eventually (\x. f x < 0) F \ LIM x F. inverse (f x) :> at_bot" hoelzl@50347: unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric] hoelzl@50347: by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric]) hoelzl@50347: hoelzl@50325: lemma tendsto_inverse_0: hoelzl@50325: fixes x :: "_ \ 'a\real_normed_div_algebra" hoelzl@50325: shows "(inverse ---> (0::'a)) at_infinity" hoelzl@50325: unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity hoelzl@50325: proof safe hoelzl@50325: fix r :: real assume "0 < r" hoelzl@50325: show "\b. \x. b \ norm x \ norm (inverse x :: 'a) < r" hoelzl@50325: proof (intro exI[of _ "inverse (r / 2)"] allI impI) hoelzl@50325: fix x :: 'a hoelzl@50325: from `0 < r` have "0 < inverse (r / 2)" by simp hoelzl@50325: also assume *: "inverse (r / 2) \ norm x" hoelzl@50325: finally show "norm (inverse x) < r" hoelzl@50325: using * `0 < r` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps) hoelzl@50325: qed hoelzl@50325: qed hoelzl@50325: hoelzl@50347: lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top" hoelzl@50347: proof (rule antisym) hoelzl@50347: have "(inverse ---> (0::real)) at_top" hoelzl@50347: by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl) hoelzl@50347: then show "filtermap inverse at_top \ at_right (0::real)" hoelzl@51641: by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def) hoelzl@50347: next hoelzl@50347: have "filtermap inverse (filtermap inverse (at_right (0::real))) \ filtermap inverse at_top" hoelzl@50347: using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono) hoelzl@50347: then show "at_right (0::real) \ filtermap inverse at_top" hoelzl@50347: by (simp add: filtermap_ident filtermap_filtermap) hoelzl@50347: qed hoelzl@50347: hoelzl@50347: lemma eventually_at_right_to_top: hoelzl@50347: "eventually P (at_right (0::real)) \ eventually (\x. P (inverse x)) at_top" hoelzl@50347: unfolding at_right_to_top eventually_filtermap .. hoelzl@50347: hoelzl@50347: lemma filterlim_at_right_to_top: hoelzl@50347: "filterlim f F (at_right (0::real)) \ (LIM x at_top. f (inverse x) :> F)" hoelzl@50347: unfolding filterlim_def at_right_to_top filtermap_filtermap .. hoelzl@50347: hoelzl@50347: lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))" hoelzl@50347: unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident .. hoelzl@50347: hoelzl@50347: lemma eventually_at_top_to_right: hoelzl@50347: "eventually P at_top \ eventually (\x. P (inverse x)) (at_right (0::real))" hoelzl@50347: unfolding at_top_to_right eventually_filtermap .. hoelzl@50347: hoelzl@50347: lemma filterlim_at_top_to_right: hoelzl@50347: "filterlim f F at_top \ (LIM x (at_right (0::real)). f (inverse x) :> F)" hoelzl@50347: unfolding filterlim_def at_top_to_right filtermap_filtermap .. hoelzl@50347: hoelzl@50325: lemma filterlim_inverse_at_infinity: hoelzl@50325: fixes x :: "_ \ 'a\{real_normed_div_algebra, division_ring_inverse_zero}" hoelzl@50325: shows "filterlim inverse at_infinity (at (0::'a))" hoelzl@50325: unfolding filterlim_at_infinity[OF order_refl] hoelzl@50325: proof safe hoelzl@50325: fix r :: real assume "0 < r" hoelzl@50325: then show "eventually (\x::'a. r \ norm (inverse x)) (at 0)" hoelzl@50325: unfolding eventually_at norm_inverse hoelzl@50325: by (intro exI[of _ "inverse r"]) hoelzl@50325: (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide) hoelzl@50325: qed hoelzl@50325: hoelzl@50325: lemma filterlim_inverse_at_iff: hoelzl@50325: fixes g :: "'a \ 'b\{real_normed_div_algebra, division_ring_inverse_zero}" hoelzl@50325: shows "(LIM x F. inverse (g x) :> at 0) \ (LIM x F. g x :> at_infinity)" hoelzl@50325: unfolding filterlim_def filtermap_filtermap[symmetric] hoelzl@50325: proof hoelzl@50325: assume "filtermap g F \ at_infinity" hoelzl@50325: then have "filtermap inverse (filtermap g F) \ filtermap inverse at_infinity" hoelzl@50325: by (rule filtermap_mono) hoelzl@50325: also have "\ \ at 0" hoelzl@51641: using tendsto_inverse_0[where 'a='b] hoelzl@51641: by (auto intro!: exI[of _ 1] hoelzl@51641: simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity) hoelzl@50325: finally show "filtermap inverse (filtermap g F) \ at 0" . hoelzl@50325: next hoelzl@50325: assume "filtermap inverse (filtermap g F) \ at 0" hoelzl@50325: then have "filtermap inverse (filtermap inverse (filtermap g F)) \ filtermap inverse (at 0)" hoelzl@50325: by (rule filtermap_mono) hoelzl@50325: with filterlim_inverse_at_infinity show "filtermap g F \ at_infinity" hoelzl@50325: by (auto intro: order_trans simp: filterlim_def filtermap_filtermap) hoelzl@50325: qed hoelzl@50325: hoelzl@51641: lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \ ((\x. inverse (f x) :: real) ---> 0) F" hoelzl@51641: by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) hoelzl@50419: hoelzl@50324: text {* hoelzl@50324: hoelzl@50324: We only show rules for multiplication and addition when the functions are either against a real hoelzl@50324: value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}. hoelzl@50324: hoelzl@50324: *} hoelzl@50324: hoelzl@50324: lemma filterlim_tendsto_pos_mult_at_top: hoelzl@50324: assumes f: "(f ---> c) F" and c: "0 < c" hoelzl@50324: assumes g: "LIM x F. g x :> at_top" hoelzl@50324: shows "LIM x F. (f x * g x :: real) :> at_top" hoelzl@50324: unfolding filterlim_at_top_gt[where c=0] hoelzl@50324: proof safe hoelzl@50324: fix Z :: real assume "0 < Z" hoelzl@50324: from f `0 < c` have "eventually (\x. c / 2 < f x) F" hoelzl@50324: by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1 hoelzl@50324: simp: dist_real_def abs_real_def split: split_if_asm) hoelzl@50346: moreover from g have "eventually (\x. (Z / c * 2) \ g x) F" hoelzl@50324: unfolding filterlim_at_top by auto hoelzl@50346: ultimately show "eventually (\x. Z \ f x * g x) F" hoelzl@50324: proof eventually_elim hoelzl@50346: fix x assume "c / 2 < f x" "Z / c * 2 \ g x" hoelzl@50346: with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) \ f x * g x" hoelzl@50346: by (intro mult_mono) (auto simp: zero_le_divide_iff) hoelzl@50346: with `0 < c` show "Z \ f x * g x" hoelzl@50324: by simp hoelzl@50324: qed hoelzl@50324: qed hoelzl@50324: hoelzl@50324: lemma filterlim_at_top_mult_at_top: hoelzl@50324: assumes f: "LIM x F. f x :> at_top" hoelzl@50324: assumes g: "LIM x F. g x :> at_top" hoelzl@50324: shows "LIM x F. (f x * g x :: real) :> at_top" hoelzl@50324: unfolding filterlim_at_top_gt[where c=0] hoelzl@50324: proof safe hoelzl@50324: fix Z :: real assume "0 < Z" hoelzl@50346: from f have "eventually (\x. 1 \ f x) F" hoelzl@50324: unfolding filterlim_at_top by auto hoelzl@50346: moreover from g have "eventually (\x. Z \ g x) F" hoelzl@50324: unfolding filterlim_at_top by auto hoelzl@50346: ultimately show "eventually (\x. Z \ f x * g x) F" hoelzl@50324: proof eventually_elim hoelzl@50346: fix x assume "1 \ f x" "Z \ g x" hoelzl@50346: with `0 < Z` have "1 * Z \ f x * g x" hoelzl@50346: by (intro mult_mono) (auto simp: zero_le_divide_iff) hoelzl@50346: then show "Z \ f x * g x" hoelzl@50324: by simp hoelzl@50324: qed hoelzl@50324: qed hoelzl@50324: hoelzl@50419: lemma filterlim_tendsto_pos_mult_at_bot: hoelzl@50419: assumes "(f ---> c) F" "0 < (c::real)" "filterlim g at_bot F" hoelzl@50419: shows "LIM x F. f x * g x :> at_bot" hoelzl@50419: using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\x. - g x"] assms(3) hoelzl@50419: unfolding filterlim_uminus_at_bot by simp hoelzl@50419: hoelzl@56330: lemma filterlim_pow_at_top: hoelzl@56330: fixes f :: "real \ real" hoelzl@56330: assumes "0 < n" and f: "LIM x F. f x :> at_top" hoelzl@56330: shows "LIM x F. (f x)^n :: real :> at_top" hoelzl@56330: using `0 < n` proof (induct n) hoelzl@56330: case (Suc n) with f show ?case hoelzl@56330: by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top) hoelzl@56330: qed simp hoelzl@56330: hoelzl@56330: lemma filterlim_pow_at_bot_even: hoelzl@56330: fixes f :: "real \ real" hoelzl@56330: shows "0 < n \ LIM x F. f x :> at_bot \ even n \ LIM x F. (f x)^n :> at_top" hoelzl@56330: using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_top) hoelzl@56330: hoelzl@56330: lemma filterlim_pow_at_bot_odd: hoelzl@56330: fixes f :: "real \ real" hoelzl@56330: shows "0 < n \ LIM x F. f x :> at_bot \ odd n \ LIM x F. (f x)^n :> at_bot" hoelzl@56330: using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_bot) hoelzl@56330: hoelzl@50324: lemma filterlim_tendsto_add_at_top: hoelzl@50324: assumes f: "(f ---> c) F" hoelzl@50324: assumes g: "LIM x F. g x :> at_top" hoelzl@50324: shows "LIM x F. (f x + g x :: real) :> at_top" hoelzl@50324: unfolding filterlim_at_top_gt[where c=0] hoelzl@50324: proof safe hoelzl@50324: fix Z :: real assume "0 < Z" hoelzl@50324: from f have "eventually (\x. c - 1 < f x) F" hoelzl@50324: by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def) hoelzl@50346: moreover from g have "eventually (\x. Z - (c - 1) \ g x) F" hoelzl@50324: unfolding filterlim_at_top by auto hoelzl@50346: ultimately show "eventually (\x. Z \ f x + g x) F" hoelzl@50324: by eventually_elim simp hoelzl@50324: qed hoelzl@50324: hoelzl@50347: lemma LIM_at_top_divide: hoelzl@50347: fixes f g :: "'a \ real" hoelzl@50347: assumes f: "(f ---> a) F" "0 < a" hoelzl@50347: assumes g: "(g ---> 0) F" "eventually (\x. 0 < g x) F" hoelzl@50347: shows "LIM x F. f x / g x :> at_top" hoelzl@50347: unfolding divide_inverse hoelzl@50347: by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) hoelzl@50347: hoelzl@50324: lemma filterlim_at_top_add_at_top: hoelzl@50324: assumes f: "LIM x F. f x :> at_top" hoelzl@50324: assumes g: "LIM x F. g x :> at_top" hoelzl@50324: shows "LIM x F. (f x + g x :: real) :> at_top" hoelzl@50324: unfolding filterlim_at_top_gt[where c=0] hoelzl@50324: proof safe hoelzl@50324: fix Z :: real assume "0 < Z" hoelzl@50346: from f have "eventually (\x. 0 \ f x) F" hoelzl@50324: unfolding filterlim_at_top by auto hoelzl@50346: moreover from g have "eventually (\x. Z \ g x) F" hoelzl@50324: unfolding filterlim_at_top by auto hoelzl@50346: ultimately show "eventually (\x. Z \ f x + g x) F" hoelzl@50324: by eventually_elim simp hoelzl@50324: qed hoelzl@50324: hoelzl@50331: lemma tendsto_divide_0: hoelzl@50331: fixes f :: "_ \ 'a\{real_normed_div_algebra, division_ring_inverse_zero}" hoelzl@50331: assumes f: "(f ---> c) F" hoelzl@50331: assumes g: "LIM x F. g x :> at_infinity" hoelzl@50331: shows "((\x. f x / g x) ---> 0) F" hoelzl@50331: using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse) hoelzl@50331: hoelzl@50331: lemma linear_plus_1_le_power: hoelzl@50331: fixes x :: real hoelzl@50331: assumes x: "0 \ x" hoelzl@50331: shows "real n * x + 1 \ (x + 1) ^ n" hoelzl@50331: proof (induct n) hoelzl@50331: case (Suc n) hoelzl@50331: have "real (Suc n) * x + 1 \ (x + 1) * (real n * x + 1)" nipkow@56536: by (simp add: field_simps real_of_nat_Suc x) hoelzl@50331: also have "\ \ (x + 1)^Suc n" hoelzl@50331: using Suc x by (simp add: mult_left_mono) hoelzl@50331: finally show ?case . hoelzl@50331: qed simp hoelzl@50331: hoelzl@50331: lemma filterlim_realpow_sequentially_gt1: hoelzl@50331: fixes x :: "'a :: real_normed_div_algebra" hoelzl@50331: assumes x[arith]: "1 < norm x" hoelzl@50331: shows "LIM n sequentially. x ^ n :> at_infinity" hoelzl@50331: proof (intro filterlim_at_infinity[THEN iffD2] allI impI) hoelzl@50331: fix y :: real assume "0 < y" hoelzl@50331: have "0 < norm x - 1" by simp hoelzl@50331: then obtain N::nat where "y < real N * (norm x - 1)" by (blast dest: reals_Archimedean3) hoelzl@50331: also have "\ \ real N * (norm x - 1) + 1" by simp hoelzl@50331: also have "\ \ (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp hoelzl@50331: also have "\ = norm x ^ N" by simp hoelzl@50331: finally have "\n\N. y \ norm x ^ n" hoelzl@50331: by (metis order_less_le_trans power_increasing order_less_imp_le x) hoelzl@50331: then show "eventually (\n. y \ norm (x ^ n)) sequentially" hoelzl@50331: unfolding eventually_sequentially hoelzl@50331: by (auto simp: norm_power) hoelzl@50331: qed simp hoelzl@50331: hoelzl@51471: hoelzl@51526: subsection {* Limits of Sequences *} hoelzl@51526: hoelzl@51526: lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z" hoelzl@51526: by simp hoelzl@51526: hoelzl@51526: lemma LIMSEQ_iff: hoelzl@51526: fixes L :: "'a::real_normed_vector" hoelzl@51526: shows "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" hoelzl@51526: unfolding LIMSEQ_def dist_norm .. hoelzl@51526: hoelzl@51526: lemma LIMSEQ_I: hoelzl@51526: fixes L :: "'a::real_normed_vector" hoelzl@51526: shows "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X ----> L" hoelzl@51526: by (simp add: LIMSEQ_iff) hoelzl@51526: hoelzl@51526: lemma LIMSEQ_D: hoelzl@51526: fixes L :: "'a::real_normed_vector" hoelzl@51526: shows "\X ----> L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" hoelzl@51526: by (simp add: LIMSEQ_iff) hoelzl@51526: hoelzl@51526: lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ n. X (n * l)) ----> x" hoelzl@51526: unfolding tendsto_def eventually_sequentially haftmann@57512: by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute) hoelzl@51526: hoelzl@51526: lemma Bseq_inverse_lemma: hoelzl@51526: fixes x :: "'a::real_normed_div_algebra" hoelzl@51526: shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" hoelzl@51526: apply (subst nonzero_norm_inverse, clarsimp) hoelzl@51526: apply (erule (1) le_imp_inverse_le) hoelzl@51526: done hoelzl@51526: hoelzl@51526: lemma Bseq_inverse: hoelzl@51526: fixes a :: "'a::real_normed_div_algebra" hoelzl@51526: shows "\X ----> a; a \ 0\ \ Bseq (\n. inverse (X n))" hoelzl@51526: by (rule Bfun_inverse) hoelzl@51526: hoelzl@51526: lemma LIMSEQ_diff_approach_zero: hoelzl@51526: fixes L :: "'a::real_normed_vector" hoelzl@51526: shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L" hoelzl@51526: by (drule (1) tendsto_add, simp) hoelzl@51526: hoelzl@51526: lemma LIMSEQ_diff_approach_zero2: hoelzl@51526: fixes L :: "'a::real_normed_vector" hoelzl@51526: shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L" hoelzl@51526: by (drule (1) tendsto_diff, simp) hoelzl@51526: hoelzl@51526: text{*An unbounded sequence's inverse tends to 0*} hoelzl@51526: hoelzl@51526: lemma LIMSEQ_inverse_zero: hoelzl@51526: "\r::real. \N. \n\N. r < X n \ (\n. inverse (X n)) ----> 0" hoelzl@51526: apply (rule filterlim_compose[OF tendsto_inverse_0]) hoelzl@51526: apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially) hoelzl@51526: apply (metis abs_le_D1 linorder_le_cases linorder_not_le) hoelzl@51526: done hoelzl@51526: hoelzl@51526: text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} hoelzl@51526: hoelzl@51526: lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" hoelzl@51526: by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc hoelzl@51526: filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity) hoelzl@51526: hoelzl@51526: text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to hoelzl@51526: infinity is now easily proved*} hoelzl@51526: hoelzl@51526: lemma LIMSEQ_inverse_real_of_nat_add: hoelzl@51526: "(%n. r + inverse(real(Suc n))) ----> r" hoelzl@51526: using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto hoelzl@51526: hoelzl@51526: lemma LIMSEQ_inverse_real_of_nat_add_minus: hoelzl@51526: "(%n. r + -inverse(real(Suc n))) ----> r" hoelzl@51526: using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] hoelzl@51526: by auto hoelzl@51526: hoelzl@51526: lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: hoelzl@51526: "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" hoelzl@51526: using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]] hoelzl@51526: by auto hoelzl@51526: hoelzl@51526: subsection {* Convergence on sequences *} hoelzl@51526: hoelzl@51526: lemma convergent_add: hoelzl@51526: fixes X Y :: "nat \ 'a::real_normed_vector" hoelzl@51526: assumes "convergent (\n. X n)" hoelzl@51526: assumes "convergent (\n. Y n)" hoelzl@51526: shows "convergent (\n. X n + Y n)" hoelzl@51526: using assms unfolding convergent_def by (fast intro: tendsto_add) hoelzl@51526: hoelzl@51526: lemma convergent_setsum: hoelzl@51526: fixes X :: "'a \ nat \ 'b::real_normed_vector" hoelzl@51526: assumes "\i. i \ A \ convergent (\n. X i n)" hoelzl@51526: shows "convergent (\n. \i\A. X i n)" hoelzl@51526: proof (cases "finite A") hoelzl@51526: case True from this and assms show ?thesis hoelzl@51526: by (induct A set: finite) (simp_all add: convergent_const convergent_add) hoelzl@51526: qed (simp add: convergent_const) hoelzl@51526: hoelzl@51526: lemma (in bounded_linear) convergent: hoelzl@51526: assumes "convergent (\n. X n)" hoelzl@51526: shows "convergent (\n. f (X n))" hoelzl@51526: using assms unfolding convergent_def by (fast intro: tendsto) hoelzl@51526: hoelzl@51526: lemma (in bounded_bilinear) convergent: hoelzl@51526: assumes "convergent (\n. X n)" and "convergent (\n. Y n)" hoelzl@51526: shows "convergent (\n. X n ** Y n)" hoelzl@51526: using assms unfolding convergent_def by (fast intro: tendsto) hoelzl@51526: hoelzl@51526: lemma convergent_minus_iff: hoelzl@51526: fixes X :: "nat \ 'a::real_normed_vector" hoelzl@51526: shows "convergent X \ convergent (\n. - X n)" hoelzl@51526: apply (simp add: convergent_def) hoelzl@51526: apply (auto dest: tendsto_minus) hoelzl@51526: apply (drule tendsto_minus, auto) hoelzl@51526: done hoelzl@51526: hoelzl@51526: hoelzl@51526: text {* A monotone sequence converges to its least upper bound. *} hoelzl@51526: hoelzl@54263: lemma LIMSEQ_incseq_SUP: hoelzl@54263: fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" hoelzl@54263: assumes u: "bdd_above (range X)" hoelzl@54263: assumes X: "incseq X" hoelzl@54263: shows "X ----> (SUP i. X i)" hoelzl@54263: by (rule order_tendstoI) hoelzl@54263: (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u]) hoelzl@51526: hoelzl@54263: lemma LIMSEQ_decseq_INF: hoelzl@54263: fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" hoelzl@54263: assumes u: "bdd_below (range X)" hoelzl@54263: assumes X: "decseq X" hoelzl@54263: shows "X ----> (INF i. X i)" hoelzl@54263: by (rule order_tendstoI) hoelzl@54263: (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u]) hoelzl@51526: hoelzl@51526: text{*Main monotonicity theorem*} hoelzl@51526: hoelzl@51526: lemma Bseq_monoseq_convergent: "Bseq X \ monoseq X \ convergent (X::nat\real)" hoelzl@54263: by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below) hoelzl@54263: hoelzl@54263: lemma Bseq_mono_convergent: "Bseq X \ (\m n. m \ n \ X m \ X n) \ convergent (X::nat\real)" hoelzl@54263: by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def) hoelzl@51526: hoelzl@51526: lemma Cauchy_iff: hoelzl@51526: fixes X :: "nat \ 'a::real_normed_vector" hoelzl@51526: shows "Cauchy X \ (\e>0. \M. \m\M. \n\M. norm (X m - X n) < e)" hoelzl@51526: unfolding Cauchy_def dist_norm .. hoelzl@51526: hoelzl@51526: lemma CauchyI: hoelzl@51526: fixes X :: "nat \ 'a::real_normed_vector" hoelzl@51526: shows "(\e. 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e) \ Cauchy X" hoelzl@51526: by (simp add: Cauchy_iff) hoelzl@51526: hoelzl@51526: lemma CauchyD: hoelzl@51526: fixes X :: "nat \ 'a::real_normed_vector" hoelzl@51526: shows "\Cauchy X; 0 < e\ \ \M. \m\M. \n\M. norm (X m - X n) < e" hoelzl@51526: by (simp add: Cauchy_iff) hoelzl@51526: hoelzl@51526: lemma incseq_convergent: hoelzl@51526: fixes X :: "nat \ real" hoelzl@51526: assumes "incseq X" and "\i. X i \ B" hoelzl@51526: obtains L where "X ----> L" "\i. X i \ L" hoelzl@51526: proof atomize_elim hoelzl@51526: from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X] hoelzl@51526: obtain L where "X ----> L" hoelzl@51526: by (auto simp: convergent_def monoseq_def incseq_def) hoelzl@51526: with `incseq X` show "\L. X ----> L \ (\i. X i \ L)" hoelzl@51526: by (auto intro!: exI[of _ L] incseq_le) hoelzl@51526: qed hoelzl@51526: hoelzl@51526: lemma decseq_convergent: hoelzl@51526: fixes X :: "nat \ real" hoelzl@51526: assumes "decseq X" and "\i. B \ X i" hoelzl@51526: obtains L where "X ----> L" "\i. L \ X i" hoelzl@51526: proof atomize_elim hoelzl@51526: from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X] hoelzl@51526: obtain L where "X ----> L" hoelzl@51526: by (auto simp: convergent_def monoseq_def decseq_def) hoelzl@51526: with `decseq X` show "\L. X ----> L \ (\i. L \ X i)" hoelzl@51526: by (auto intro!: exI[of _ L] decseq_le) hoelzl@51526: qed hoelzl@51526: hoelzl@51526: subsubsection {* Cauchy Sequences are Bounded *} hoelzl@51526: hoelzl@51526: text{*A Cauchy sequence is bounded -- this is the standard hoelzl@51526: proof mechanization rather than the nonstandard proof*} hoelzl@51526: hoelzl@51526: lemma lemmaCauchy: "\n \ M. norm (X M - X n) < (1::real) hoelzl@51526: ==> \n \ M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" hoelzl@51526: apply (clarify, drule spec, drule (1) mp) hoelzl@51526: apply (simp only: norm_minus_commute) hoelzl@51526: apply (drule order_le_less_trans [OF norm_triangle_ineq2]) hoelzl@51526: apply simp hoelzl@51526: done hoelzl@51526: hoelzl@51526: subsection {* Power Sequences *} hoelzl@51526: hoelzl@51526: text{*The sequence @{term "x^n"} tends to 0 if @{term "0\x"} and @{term hoelzl@51526: "x<1"}. Proof will use (NS) Cauchy equivalence for convergence and hoelzl@51526: also fact that bounded and monotonic sequence converges.*} hoelzl@51526: hoelzl@51526: lemma Bseq_realpow: "[| 0 \ (x::real); x \ 1 |] ==> Bseq (%n. x ^ n)" hoelzl@51526: apply (simp add: Bseq_def) hoelzl@51526: apply (rule_tac x = 1 in exI) hoelzl@51526: apply (simp add: power_abs) hoelzl@51526: apply (auto dest: power_mono) hoelzl@51526: done hoelzl@51526: hoelzl@51526: lemma monoseq_realpow: fixes x :: real shows "[| 0 \ x; x \ 1 |] ==> monoseq (%n. x ^ n)" hoelzl@51526: apply (clarify intro!: mono_SucI2) hoelzl@51526: apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) hoelzl@51526: done hoelzl@51526: hoelzl@51526: lemma convergent_realpow: hoelzl@51526: "[| 0 \ (x::real); x \ 1 |] ==> convergent (%n. x ^ n)" hoelzl@51526: by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) hoelzl@51526: hoelzl@51526: lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" hoelzl@51526: by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp hoelzl@51526: hoelzl@51526: lemma LIMSEQ_realpow_zero: hoelzl@51526: "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" hoelzl@51526: proof cases hoelzl@51526: assume "0 \ x" and "x \ 0" hoelzl@51526: hence x0: "0 < x" by simp hoelzl@51526: assume x1: "x < 1" hoelzl@51526: from x0 x1 have "1 < inverse x" hoelzl@51526: by (rule one_less_inverse) hoelzl@51526: hence "(\n. inverse (inverse x ^ n)) ----> 0" hoelzl@51526: by (rule LIMSEQ_inverse_realpow_zero) hoelzl@51526: thus ?thesis by (simp add: power_inverse) hoelzl@51526: qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const) hoelzl@51526: hoelzl@51526: lemma LIMSEQ_power_zero: hoelzl@51526: fixes x :: "'a::{real_normed_algebra_1}" hoelzl@51526: shows "norm x < 1 \ (\n. x ^ n) ----> 0" hoelzl@51526: apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) hoelzl@51526: apply (simp only: tendsto_Zfun_iff, erule Zfun_le) hoelzl@51526: apply (simp add: power_abs norm_power_ineq) hoelzl@51526: done hoelzl@51526: hoelzl@51526: lemma LIMSEQ_divide_realpow_zero: "1 < x \ (\n. a / (x ^ n) :: real) ----> 0" hoelzl@51526: by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp hoelzl@51526: hoelzl@51526: text{*Limit of @{term "c^n"} for @{term"\c\ < 1"}*} hoelzl@51526: hoelzl@51526: lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) ----> 0" hoelzl@51526: by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) hoelzl@51526: hoelzl@51526: lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\n. c ^ n :: real) ----> 0" hoelzl@51526: by (rule LIMSEQ_power_zero) simp hoelzl@51526: hoelzl@51526: hoelzl@51526: subsection {* Limits of Functions *} hoelzl@51526: hoelzl@51526: lemma LIM_eq: hoelzl@51526: fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" hoelzl@51526: shows "f -- a --> L = hoelzl@51526: (\r>0.\s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r)" hoelzl@51526: by (simp add: LIM_def dist_norm) hoelzl@51526: hoelzl@51526: lemma LIM_I: hoelzl@51526: fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" hoelzl@51526: shows "(!!r. 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r) hoelzl@51526: ==> f -- a --> L" hoelzl@51526: by (simp add: LIM_eq) hoelzl@51526: hoelzl@51526: lemma LIM_D: hoelzl@51526: fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" hoelzl@51526: shows "[| f -- a --> L; 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r" hoelzl@51526: by (simp add: LIM_eq) hoelzl@51526: hoelzl@51526: lemma LIM_offset: hoelzl@51526: fixes a :: "'a::real_normed_vector" hoelzl@51526: shows "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" hoelzl@51641: unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp hoelzl@51526: hoelzl@51526: lemma LIM_offset_zero: hoelzl@51526: fixes a :: "'a::real_normed_vector" hoelzl@51526: shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" haftmann@57512: by (drule_tac k="a" in LIM_offset, simp add: add.commute) hoelzl@51526: hoelzl@51526: lemma LIM_offset_zero_cancel: hoelzl@51526: fixes a :: "'a::real_normed_vector" hoelzl@51526: shows "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" hoelzl@51526: by (drule_tac k="- a" in LIM_offset, simp) hoelzl@51526: hoelzl@51642: lemma LIM_offset_zero_iff: hoelzl@51642: fixes f :: "'a :: real_normed_vector \ _" hoelzl@51642: shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" hoelzl@51642: using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto hoelzl@51642: hoelzl@51526: lemma LIM_zero: hoelzl@51526: fixes f :: "'a::topological_space \ 'b::real_normed_vector" hoelzl@51526: shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" hoelzl@51526: unfolding tendsto_iff dist_norm by simp hoelzl@51526: hoelzl@51526: lemma LIM_zero_cancel: hoelzl@51526: fixes f :: "'a::topological_space \ 'b::real_normed_vector" hoelzl@51526: shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" hoelzl@51526: unfolding tendsto_iff dist_norm by simp hoelzl@51526: hoelzl@51526: lemma LIM_zero_iff: hoelzl@51526: fixes f :: "'a::metric_space \ 'b::real_normed_vector" hoelzl@51526: shows "((\x. f x - l) ---> 0) F = (f ---> l) F" hoelzl@51526: unfolding tendsto_iff dist_norm by simp hoelzl@51526: hoelzl@51526: lemma LIM_imp_LIM: hoelzl@51526: fixes f :: "'a::topological_space \ 'b::real_normed_vector" hoelzl@51526: fixes g :: "'a::topological_space \ 'c::real_normed_vector" hoelzl@51526: assumes f: "f -- a --> l" hoelzl@51526: assumes le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" hoelzl@51526: shows "g -- a --> m" hoelzl@51526: by (rule metric_LIM_imp_LIM [OF f], hoelzl@51526: simp add: dist_norm le) hoelzl@51526: hoelzl@51526: lemma LIM_equal2: hoelzl@51526: fixes f g :: "'a::real_normed_vector \ 'b::topological_space" hoelzl@51526: assumes 1: "0 < R" hoelzl@51526: assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" hoelzl@51526: shows "g -- a --> l \ f -- a --> l" hoelzl@51526: by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) hoelzl@51526: hoelzl@51526: lemma LIM_compose2: hoelzl@51526: fixes a :: "'a::real_normed_vector" hoelzl@51526: assumes f: "f -- a --> b" hoelzl@51526: assumes g: "g -- b --> c" hoelzl@51526: assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" hoelzl@51526: shows "(\x. g (f x)) -- a --> c" hoelzl@51526: by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) hoelzl@51526: hoelzl@51526: lemma real_LIM_sandwich_zero: hoelzl@51526: fixes f g :: "'a::topological_space \ real" hoelzl@51526: assumes f: "f -- a --> 0" hoelzl@51526: assumes 1: "\x. x \ a \ 0 \ g x" hoelzl@51526: assumes 2: "\x. x \ a \ g x \ f x" hoelzl@51526: shows "g -- a --> 0" hoelzl@51526: proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) hoelzl@51526: fix x assume x: "x \ a" hoelzl@51526: have "norm (g x - 0) = g x" by (simp add: 1 x) hoelzl@51526: also have "g x \ f x" by (rule 2 [OF x]) hoelzl@51526: also have "f x \ \f x\" by (rule abs_ge_self) hoelzl@51526: also have "\f x\ = norm (f x - 0)" by simp hoelzl@51526: finally show "norm (g x - 0) \ norm (f x - 0)" . hoelzl@51526: qed hoelzl@51526: hoelzl@51526: hoelzl@51526: subsection {* Continuity *} hoelzl@51526: hoelzl@51526: lemma LIM_isCont_iff: hoelzl@51526: fixes f :: "'a::real_normed_vector \ 'b::topological_space" hoelzl@51526: shows "(f -- a --> f a) = ((\h. f (a + h)) -- 0 --> f a)" hoelzl@51526: by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) hoelzl@51526: hoelzl@51526: lemma isCont_iff: hoelzl@51526: fixes f :: "'a::real_normed_vector \ 'b::topological_space" hoelzl@51526: shows "isCont f x = (\h. f (x + h)) -- 0 --> f x" hoelzl@51526: by (simp add: isCont_def LIM_isCont_iff) hoelzl@51526: hoelzl@51526: lemma isCont_LIM_compose2: hoelzl@51526: fixes a :: "'a::real_normed_vector" hoelzl@51526: assumes f [unfolded isCont_def]: "isCont f a" hoelzl@51526: assumes g: "g -- f a --> l" hoelzl@51526: assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" hoelzl@51526: shows "(\x. g (f x)) -- a --> l" hoelzl@51526: by (rule LIM_compose2 [OF f g inj]) hoelzl@51526: hoelzl@51526: hoelzl@51526: lemma isCont_norm [simp]: hoelzl@51526: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51526: shows "isCont f a \ isCont (\x. norm (f x)) a" hoelzl@51526: by (fact continuous_norm) hoelzl@51526: hoelzl@51526: lemma isCont_rabs [simp]: hoelzl@51526: fixes f :: "'a::t2_space \ real" hoelzl@51526: shows "isCont f a \ isCont (\x. \f x\) a" hoelzl@51526: by (fact continuous_rabs) hoelzl@51526: hoelzl@51526: lemma isCont_add [simp]: hoelzl@51526: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51526: shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" hoelzl@51526: by (fact continuous_add) hoelzl@51526: hoelzl@51526: lemma isCont_minus [simp]: hoelzl@51526: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51526: shows "isCont f a \ isCont (\x. - f x) a" hoelzl@51526: by (fact continuous_minus) hoelzl@51526: hoelzl@51526: lemma isCont_diff [simp]: hoelzl@51526: fixes f :: "'a::t2_space \ 'b::real_normed_vector" hoelzl@51526: shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" hoelzl@51526: by (fact continuous_diff) hoelzl@51526: hoelzl@51526: lemma isCont_mult [simp]: hoelzl@51526: fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" hoelzl@51526: shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" hoelzl@51526: by (fact continuous_mult) hoelzl@51526: hoelzl@51526: lemma (in bounded_linear) isCont: hoelzl@51526: "isCont g a \ isCont (\x. f (g x)) a" hoelzl@51526: by (fact continuous) hoelzl@51526: hoelzl@51526: lemma (in bounded_bilinear) isCont: hoelzl@51526: "\isCont f a; isCont g a\ \ isCont (\x. f x ** g x) a" hoelzl@51526: by (fact continuous) hoelzl@51526: hoelzl@51526: lemmas isCont_scaleR [simp] = hoelzl@51526: bounded_bilinear.isCont [OF bounded_bilinear_scaleR] hoelzl@51526: hoelzl@51526: lemmas isCont_of_real [simp] = hoelzl@51526: bounded_linear.isCont [OF bounded_linear_of_real] hoelzl@51526: hoelzl@51526: lemma isCont_power [simp]: hoelzl@51526: fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" hoelzl@51526: shows "isCont f a \ isCont (\x. f x ^ n) a" hoelzl@51526: by (fact continuous_power) hoelzl@51526: hoelzl@51526: lemma isCont_setsum [simp]: hoelzl@51526: fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" hoelzl@51526: shows "\i\A. isCont (f i) a \ isCont (\x. \i\A. f i x) a" hoelzl@51526: by (auto intro: continuous_setsum) hoelzl@51526: hoelzl@51526: subsection {* Uniform Continuity *} hoelzl@51526: hoelzl@51531: definition hoelzl@51531: isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" where hoelzl@51531: "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" hoelzl@51531: hoelzl@51531: lemma isUCont_isCont: "isUCont f ==> isCont f x" hoelzl@51531: by (simp add: isUCont_def isCont_def LIM_def, force) hoelzl@51531: hoelzl@51531: lemma isUCont_Cauchy: hoelzl@51531: "\isUCont f; Cauchy X\ \ Cauchy (\n. f (X n))" hoelzl@51531: unfolding isUCont_def hoelzl@51531: apply (rule metric_CauchyI) hoelzl@51531: apply (drule_tac x=e in spec, safe) hoelzl@51531: apply (drule_tac e=s in metric_CauchyD, safe) hoelzl@51531: apply (rule_tac x=M in exI, simp) hoelzl@51531: done hoelzl@51531: hoelzl@51526: lemma (in bounded_linear) isUCont: "isUCont f" hoelzl@51526: unfolding isUCont_def dist_norm hoelzl@51526: proof (intro allI impI) hoelzl@51526: fix r::real assume r: "0 < r" hoelzl@51526: obtain K where K: "0 < K" and norm_le: "\x. norm (f x) \ norm x * K" hoelzl@51526: using pos_bounded by fast hoelzl@51526: show "\s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r" hoelzl@51526: proof (rule exI, safe) nipkow@56541: from r K show "0 < r / K" by simp hoelzl@51526: next hoelzl@51526: fix x y :: 'a hoelzl@51526: assume xy: "norm (x - y) < r / K" hoelzl@51526: have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff) hoelzl@51526: also have "\ \ norm (x - y) * K" by (rule norm_le) hoelzl@51526: also from K xy have "\ < r" by (simp only: pos_less_divide_eq) hoelzl@51526: finally show "norm (f x - f y) < r" . hoelzl@51526: qed hoelzl@51526: qed hoelzl@51526: hoelzl@51526: lemma (in bounded_linear) Cauchy: "Cauchy X \ Cauchy (\n. f (X n))" hoelzl@51526: by (rule isUCont [THEN isUCont_Cauchy]) hoelzl@51526: hoelzl@51526: lemma LIM_less_bound: hoelzl@51526: fixes f :: "real \ real" hoelzl@51526: assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" hoelzl@51526: shows "0 \ f x" hoelzl@51526: proof (rule tendsto_le_const) hoelzl@51526: show "(f ---> f x) (at_left x)" hoelzl@51526: using `isCont f x` by (simp add: filterlim_at_split isCont_def) hoelzl@51526: show "eventually (\x. 0 \ f x) (at_left x)" hoelzl@51641: using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"]) hoelzl@51526: qed simp hoelzl@51471: hoelzl@51529: hoelzl@51529: subsection {* Nested Intervals and Bisection -- Needed for Compactness *} hoelzl@51529: hoelzl@51529: lemma nested_sequence_unique: hoelzl@51529: assumes "\n. f n \ f (Suc n)" "\n. g (Suc n) \ g n" "\n. f n \ g n" "(\n. f n - g n) ----> 0" hoelzl@51529: shows "\l::real. ((\n. f n \ l) \ f ----> l) \ ((\n. l \ g n) \ g ----> l)" hoelzl@51529: proof - hoelzl@51529: have "incseq f" unfolding incseq_Suc_iff by fact hoelzl@51529: have "decseq g" unfolding decseq_Suc_iff by fact hoelzl@51529: hoelzl@51529: { fix n hoelzl@51529: from `decseq g` have "g n \ g 0" by (rule decseqD) simp hoelzl@51529: with `\n. f n \ g n`[THEN spec, of n] have "f n \ g 0" by auto } hoelzl@51529: then obtain u where "f ----> u" "\i. f i \ u" hoelzl@51529: using incseq_convergent[OF `incseq f`] by auto hoelzl@51529: moreover hoelzl@51529: { fix n hoelzl@51529: from `incseq f` have "f 0 \ f n" by (rule incseqD) simp hoelzl@51529: with `\n. f n \ g n`[THEN spec, of n] have "f 0 \ g n" by simp } hoelzl@51529: then obtain l where "g ----> l" "\i. l \ g i" hoelzl@51529: using decseq_convergent[OF `decseq g`] by auto hoelzl@51529: moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]] hoelzl@51529: ultimately show ?thesis by auto hoelzl@51529: qed hoelzl@51529: hoelzl@51529: lemma Bolzano[consumes 1, case_names trans local]: hoelzl@51529: fixes P :: "real \ real \ bool" hoelzl@51529: assumes [arith]: "a \ b" hoelzl@51529: assumes trans: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c" hoelzl@51529: assumes local: "\x. a \ x \ x \ b \ \d>0. \a b. a \ x \ x \ b \ b - a < d \ P a b" hoelzl@51529: shows "P a b" hoelzl@51529: proof - blanchet@55415: def bisect \ "rec_nat (a, b) (\n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))" hoelzl@51529: def l \ "\n. fst (bisect n)" and u \ "\n. snd (bisect n)" hoelzl@51529: have l[simp]: "l 0 = a" "\n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)" hoelzl@51529: and u[simp]: "u 0 = b" "\n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)" hoelzl@51529: by (simp_all add: l_def u_def bisect_def split: prod.split) hoelzl@51529: hoelzl@51529: { fix n have "l n \ u n" by (induct n) auto } note this[simp] hoelzl@51529: hoelzl@51529: have "\x. ((\n. l n \ x) \ l ----> x) \ ((\n. x \ u n) \ u ----> x)" hoelzl@51529: proof (safe intro!: nested_sequence_unique) hoelzl@51529: fix n show "l n \ l (Suc n)" "u (Suc n) \ u n" by (induct n) auto hoelzl@51529: next hoelzl@51529: { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) } hoelzl@51529: then show "(\n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero) hoelzl@51529: qed fact hoelzl@51529: then obtain x where x: "\n. l n \ x" "\n. x \ u n" and "l ----> x" "u ----> x" by auto hoelzl@51529: obtain d where "0 < d" and d: "\a b. a \ x \ x \ b \ b - a < d \ P a b" hoelzl@51529: using `l 0 \ x` `x \ u 0` local[of x] by auto hoelzl@51529: hoelzl@51529: show "P a b" hoelzl@51529: proof (rule ccontr) hoelzl@51529: assume "\ P a b" hoelzl@51529: { fix n have "\ P (l n) (u n)" hoelzl@51529: proof (induct n) hoelzl@51529: case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto hoelzl@51529: qed (simp add: `\ P a b`) } hoelzl@51529: moreover hoelzl@51529: { have "eventually (\n. x - d / 2 < l n) sequentially" hoelzl@51529: using `0 < d` `l ----> x` by (intro order_tendstoD[of _ x]) auto hoelzl@51529: moreover have "eventually (\n. u n < x + d / 2) sequentially" hoelzl@51529: using `0 < d` `u ----> x` by (intro order_tendstoD[of _ x]) auto hoelzl@51529: ultimately have "eventually (\n. P (l n) (u n)) sequentially" hoelzl@51529: proof eventually_elim hoelzl@51529: fix n assume "x - d / 2 < l n" "u n < x + d / 2" hoelzl@51529: from add_strict_mono[OF this] have "u n - l n < d" by simp hoelzl@51529: with x show "P (l n) (u n)" by (rule d) hoelzl@51529: qed } hoelzl@51529: ultimately show False by simp hoelzl@51529: qed hoelzl@51529: qed hoelzl@51529: hoelzl@51529: lemma compact_Icc[simp, intro]: "compact {a .. b::real}" hoelzl@51529: proof (cases "a \ b", rule compactI) hoelzl@51529: fix C assume C: "a \ b" "\t\C. open t" "{a..b} \ \C" hoelzl@51529: def T == "{a .. b}" hoelzl@51529: from C(1,3) show "\C'\C. finite C' \ {a..b} \ \C'" hoelzl@51529: proof (induct rule: Bolzano) hoelzl@51529: case (trans a b c) hoelzl@51529: then have *: "{a .. c} = {a .. b} \ {b .. c}" by auto hoelzl@51529: from trans obtain C1 C2 where "C1\C \ finite C1 \ {a..b} \ \C1" "C2\C \ finite C2 \ {b..c} \ \C2" hoelzl@51529: by (auto simp: *) hoelzl@51529: with trans show ?case hoelzl@51529: unfolding * by (intro exI[of _ "C1 \ C2"]) auto hoelzl@51529: next hoelzl@51529: case (local x) hoelzl@51529: then have "x \ \C" using C by auto hoelzl@51529: with C(2) obtain c where "x \ c" "open c" "c \ C" by auto hoelzl@51529: then obtain e where "0 < e" "{x - e <..< x + e} \ c" hoelzl@51529: by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff) hoelzl@51529: with `c \ C` show ?case hoelzl@51529: by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto hoelzl@51529: qed hoelzl@51529: qed simp hoelzl@51529: hoelzl@51529: hoelzl@57447: lemma continuous_image_closed_interval: hoelzl@57447: fixes a b and f :: "real \ real" hoelzl@57447: defines "S \ {a..b}" hoelzl@57447: assumes "a \ b" and f: "continuous_on S f" hoelzl@57447: shows "\c d. f`S = {c..d} \ c \ d" hoelzl@57447: proof - hoelzl@57447: have S: "compact S" "S \ {}" hoelzl@57447: using `a \ b` by (auto simp: S_def) hoelzl@57447: obtain c where "c \ S" "\d\S. f d \ f c" hoelzl@57447: using continuous_attains_sup[OF S f] by auto hoelzl@57447: moreover obtain d where "d \ S" "\c\S. f d \ f c" hoelzl@57447: using continuous_attains_inf[OF S f] by auto hoelzl@57447: moreover have "connected (f`S)" hoelzl@57447: using connected_continuous_image[OF f] connected_Icc by (auto simp: S_def) hoelzl@57447: ultimately have "f ` S = {f d .. f c} \ f d \ f c" hoelzl@57447: by (auto simp: connected_iff_interval) hoelzl@57447: then show ?thesis hoelzl@57447: by auto hoelzl@57447: qed hoelzl@57447: hoelzl@51529: subsection {* Boundedness of continuous functions *} hoelzl@51529: hoelzl@51529: text{*By bisection, function continuous on closed interval is bounded above*} hoelzl@51529: hoelzl@51529: lemma isCont_eq_Ub: hoelzl@51529: fixes f :: "real \ 'a::linorder_topology" hoelzl@51529: shows "a \ b \ \x::real. a \ x \ x \ b \ isCont f x \ hoelzl@51529: \M. (\x. a \ x \ x \ b \ f x \ M) \ (\x. a \ x \ x \ b \ f x = M)" hoelzl@51529: using continuous_attains_sup[of "{a .. b}" f] hoelzl@51529: by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def) hoelzl@51529: hoelzl@51529: lemma isCont_eq_Lb: hoelzl@51529: fixes f :: "real \ 'a::linorder_topology" hoelzl@51529: shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ hoelzl@51529: \M. (\x. a \ x \ x \ b \ M \ f x) \ (\x. a \ x \ x \ b \ f x = M)" hoelzl@51529: using continuous_attains_inf[of "{a .. b}" f] hoelzl@51529: by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def) hoelzl@51529: hoelzl@51529: lemma isCont_bounded: hoelzl@51529: fixes f :: "real \ 'a::linorder_topology" hoelzl@51529: shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ \M. \x. a \ x \ x \ b \ f x \ M" hoelzl@51529: using isCont_eq_Ub[of a b f] by auto hoelzl@51529: hoelzl@51529: lemma isCont_has_Ub: hoelzl@51529: fixes f :: "real \ 'a::linorder_topology" hoelzl@51529: shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ hoelzl@51529: \M. (\x. a \ x \ x \ b \ f x \ M) \ (\N. N < M \ (\x. a \ x \ x \ b \ N < f x))" hoelzl@51529: using isCont_eq_Ub[of a b f] by auto hoelzl@51529: hoelzl@51529: (*HOL style here: object-level formulations*) hoelzl@51529: lemma IVT_objl: "(f(a::real) \ (y::real) & y \ f(b) & a \ b & hoelzl@51529: (\x. a \ x & x \ b --> isCont f x)) hoelzl@51529: --> (\x. a \ x & x \ b & f(x) = y)" hoelzl@51529: by (blast intro: IVT) hoelzl@51529: hoelzl@51529: lemma IVT2_objl: "(f(b::real) \ (y::real) & y \ f(a) & a \ b & hoelzl@51529: (\x. a \ x & x \ b --> isCont f x)) hoelzl@51529: --> (\x. a \ x & x \ b & f(x) = y)" hoelzl@51529: by (blast intro: IVT2) hoelzl@51529: hoelzl@51529: lemma isCont_Lb_Ub: hoelzl@51529: fixes f :: "real \ real" hoelzl@51529: assumes "a \ b" "\x. a \ x \ x \ b \ isCont f x" hoelzl@51529: shows "\L M. (\x. a \ x \ x \ b \ L \ f x \ f x \ M) \ hoelzl@51529: (\y. L \ y \ y \ M \ (\x. a \ x \ x \ b \ (f x = y)))" hoelzl@51529: proof - hoelzl@51529: obtain M where M: "a \ M" "M \ b" "\x. a \ x \ x \ b \ f x \ f M" hoelzl@51529: using isCont_eq_Ub[OF assms] by auto hoelzl@51529: obtain L where L: "a \ L" "L \ b" "\x. a \ x \ x \ b \ f L \ f x" hoelzl@51529: using isCont_eq_Lb[OF assms] by auto hoelzl@51529: show ?thesis hoelzl@51529: using IVT[of f L _ M] IVT2[of f L _ M] M L assms hoelzl@51529: apply (rule_tac x="f L" in exI) hoelzl@51529: apply (rule_tac x="f M" in exI) hoelzl@51529: apply (cases "L \ M") hoelzl@51529: apply (simp, metis order_trans) hoelzl@51529: apply (simp, metis order_trans) hoelzl@51529: done hoelzl@51529: qed hoelzl@51529: hoelzl@51529: hoelzl@51529: text{*Continuity of inverse function*} hoelzl@51529: hoelzl@51529: lemma isCont_inverse_function: hoelzl@51529: fixes f g :: "real \ real" hoelzl@51529: assumes d: "0 < d" hoelzl@51529: and inj: "\z. \z-x\ \ d \ g (f z) = z" hoelzl@51529: and cont: "\z. \z-x\ \ d \ isCont f z" hoelzl@51529: shows "isCont g (f x)" hoelzl@51529: proof - hoelzl@51529: let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}" hoelzl@51529: hoelzl@51529: have f: "continuous_on ?D f" hoelzl@51529: using cont by (intro continuous_at_imp_continuous_on ballI) auto hoelzl@51529: then have g: "continuous_on (f`?D) g" hoelzl@51529: using inj by (intro continuous_on_inv) auto hoelzl@51529: hoelzl@51529: from d f have "{min ?A ?B <..< max ?A ?B} \ f ` ?D" hoelzl@51529: by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max) hoelzl@51529: with g have "continuous_on {min ?A ?B <..< max ?A ?B} g" hoelzl@51529: by (rule continuous_on_subset) hoelzl@51529: moreover hoelzl@51529: have "(?A < f x \ f x < ?B) \ (?B < f x \ f x < ?A)" hoelzl@51529: using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto hoelzl@51529: then have "f x \ {min ?A ?B <..< max ?A ?B}" hoelzl@51529: by auto hoelzl@51529: ultimately hoelzl@51529: show ?thesis hoelzl@51529: by (simp add: continuous_on_eq_continuous_at) hoelzl@51529: qed hoelzl@51529: hoelzl@51529: lemma isCont_inverse_function2: hoelzl@51529: fixes f g :: "real \ real" shows hoelzl@51529: "\a < x; x < b; hoelzl@51529: \z. a \ z \ z \ b \ g (f z) = z; hoelzl@51529: \z. a \ z \ z \ b \ isCont f z\ hoelzl@51529: \ isCont g (f x)" hoelzl@51529: apply (rule isCont_inverse_function hoelzl@51529: [where f=f and d="min (x - a) (b - x)"]) hoelzl@51529: apply (simp_all add: abs_le_iff) hoelzl@51529: done hoelzl@51529: hoelzl@51529: (* need to rename second isCont_inverse *) hoelzl@51529: hoelzl@51529: lemma isCont_inv_fun: hoelzl@51529: fixes f g :: "real \ real" hoelzl@51529: shows "[| 0 < d; \z. \z - x\ \ d --> g(f(z)) = z; hoelzl@51529: \z. \z - x\ \ d --> isCont f z |] hoelzl@51529: ==> isCont g (f x)" hoelzl@51529: by (rule isCont_inverse_function) hoelzl@51529: hoelzl@51529: text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*} hoelzl@51529: lemma LIM_fun_gt_zero: hoelzl@51529: fixes f :: "real \ real" hoelzl@51529: shows "f -- c --> l \ 0 < l \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ 0 < f x)" hoelzl@51529: apply (drule (1) LIM_D, clarify) hoelzl@51529: apply (rule_tac x = s in exI) hoelzl@51529: apply (simp add: abs_less_iff) hoelzl@51529: done hoelzl@51529: hoelzl@51529: lemma LIM_fun_less_zero: hoelzl@51529: fixes f :: "real \ real" hoelzl@51529: shows "f -- c --> l \ l < 0 \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ f x < 0)" hoelzl@51529: apply (drule LIM_D [where r="-l"], simp, clarify) hoelzl@51529: apply (rule_tac x = s in exI) hoelzl@51529: apply (simp add: abs_less_iff) hoelzl@51529: done hoelzl@51529: hoelzl@51529: lemma LIM_fun_not_zero: hoelzl@51529: fixes f :: "real \ real" hoelzl@51529: shows "f -- c --> l \ l \ 0 \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ f x \ 0)" hoelzl@51529: using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff) hoelzl@51531: huffman@31349: end hoelzl@50324: