# HG changeset patch # User hoelzl # Date 1363945303 -3600 # Node ID 270b21f3ae0ab22b3a8c8bfabf783bc494e9dcf4 # Parent 2990382dc066359c85edd0976c6bba264f199ebf move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space) diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Library/Product_Vector.thy Fri Mar 22 10:41:43 2013 +0100 @@ -117,15 +117,6 @@ by (simp add: closed_vimage_fst closed_vimage_snd closed_Int) qed -lemma openI: (* TODO: move *) - assumes "\x. x \ S \ \T. open T \ x \ T \ T \ S" - shows "open S" -proof - - have "open (\{T. open T \ T \ S})" by auto - moreover have "\{T. open T \ T \ S} = S" by (auto dest!: assms) - ultimately show "open S" by simp -qed - lemma subset_fst_imageI: "A \ B \ S \ y \ B \ A \ fst ` S" unfolding image_def subset_eq by force @@ -202,15 +193,23 @@ (simp add: subsetD [OF `A \ B \ S`]) qed +lemma continuous_fst[continuous_intros]: "continuous F f \ continuous F (\x. fst (f x))" + unfolding continuous_def by (rule tendsto_fst) + +lemma continuous_snd[continuous_intros]: "continuous F f \ continuous F (\x. snd (f x))" + unfolding continuous_def by (rule tendsto_snd) + +lemma continuous_Pair[continuous_intros]: "continuous F f \ continuous F g \ continuous F (\x. (f x, g x))" + unfolding continuous_def by (rule tendsto_Pair) + lemma isCont_fst [simp]: "isCont f a \ isCont (\x. fst (f x)) a" - unfolding isCont_def by (rule tendsto_fst) + by (fact continuous_fst) lemma isCont_snd [simp]: "isCont f a \ isCont (\x. snd (f x)) a" - unfolding isCont_def by (rule tendsto_snd) + by (fact continuous_snd) -lemma isCont_Pair [simp]: - "\isCont f a; isCont g a\ \ isCont (\x. (f x, g x)) a" - unfolding isCont_def by (rule tendsto_Pair) +lemma isCont_Pair [simp]: "\isCont f a; isCont g a\ \ isCont (\x. (f x, g x)) a" + by (fact continuous_Pair) subsubsection {* Separation axioms *} diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Lim.thy --- a/src/HOL/Lim.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Lim.thy Fri Mar 22 10:41:43 2013 +0100 @@ -118,46 +118,6 @@ shows "isCont f x = (\h. f (x + h)) -- 0 --> f x" by (simp add: isCont_def LIM_isCont_iff) -lemma isCont_norm [simp]: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "isCont f a \ isCont (\x. norm (f x)) a" - unfolding isCont_def by (rule tendsto_norm) - -lemma isCont_rabs [simp]: - fixes f :: "'a::topological_space \ real" - shows "isCont f a \ isCont (\x. \f x\) a" - unfolding isCont_def by (rule tendsto_rabs) - -lemma isCont_add [simp]: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" - unfolding isCont_def by (rule tendsto_add) - -lemma isCont_minus [simp]: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "isCont f a \ isCont (\x. - f x) a" - unfolding isCont_def by (rule tendsto_minus) - -lemma isCont_diff [simp]: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" - unfolding isCont_def by (rule tendsto_diff) - -lemma isCont_mult [simp]: - fixes f g :: "'a::topological_space \ 'b::real_normed_algebra" - shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" - unfolding isCont_def by (rule tendsto_mult) - -lemma isCont_inverse [simp]: - fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" - shows "\isCont f a; f a \ 0\ \ isCont (\x. inverse (f x)) a" - unfolding isCont_def by (rule tendsto_inverse) - -lemma isCont_divide [simp]: - fixes f g :: "'a::topological_space \ 'b::real_normed_field" - shows "\isCont f a; isCont g a; g a \ 0\ \ isCont (\x. f x / g x) a" - unfolding isCont_def by (rule tendsto_divide) - lemma isCont_LIM_compose2: fixes a :: "'a::real_normed_vector" assumes f [unfolded isCont_def]: "isCont f a" @@ -166,35 +126,60 @@ shows "(\x. g (f x)) -- a --> l" by (rule LIM_compose2 [OF f g inj]) + +lemma isCont_norm [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "isCont f a \ isCont (\x. norm (f x)) a" + by (fact continuous_norm) + +lemma isCont_rabs [simp]: + fixes f :: "'a::t2_space \ real" + shows "isCont f a \ isCont (\x. \f x\) a" + by (fact continuous_rabs) + +lemma isCont_add [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" + by (fact continuous_add) + +lemma isCont_minus [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "isCont f a \ isCont (\x. - f x) a" + by (fact continuous_minus) + +lemma isCont_diff [simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" + by (fact continuous_diff) + +lemma isCont_mult [simp]: + fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" + shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" + by (fact continuous_mult) + lemma (in bounded_linear) isCont: "isCont g a \ isCont (\x. f (g x)) a" - unfolding isCont_def by (rule tendsto) + by (fact continuous) lemma (in bounded_bilinear) isCont: "\isCont f a; isCont g a\ \ isCont (\x. f x ** g x) a" - unfolding isCont_def by (rule tendsto) + by (fact continuous) -lemmas isCont_scaleR [simp] = +lemmas isCont_scaleR [simp] = bounded_bilinear.isCont [OF bounded_bilinear_scaleR] lemmas isCont_of_real [simp] = bounded_linear.isCont [OF bounded_linear_of_real] lemma isCont_power [simp]: - fixes f :: "'a::topological_space \ 'b::{power,real_normed_algebra}" + fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" shows "isCont f a \ isCont (\x. f x ^ n) a" - unfolding isCont_def by (rule tendsto_power) - -lemma isCont_sgn [simp]: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "\isCont f a; f a \ 0\ \ isCont (\x. sgn (f x)) a" - unfolding isCont_def by (rule tendsto_sgn) + by (fact continuous_power) lemma isCont_setsum [simp]: - fixes f :: "'a \ 'b::topological_space \ 'c::real_normed_vector" - fixes A :: "'a set" + fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" shows "\i\A. isCont (f i) a \ isCont (\x. \i\A. f i x) a" - unfolding isCont_def by (simp add: tendsto_setsum) + by (auto intro: continuous_setsum) lemmas isCont_intros = isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Limits.thy --- a/src/HOL/Limits.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Limits.thy Fri Mar 22 10:41:43 2013 +0100 @@ -236,6 +236,14 @@ "(f ---> a) F \ ((\x. norm (f x)) ---> norm a) F" unfolding norm_conv_dist by (intro tendsto_intros) +lemma continuous_norm [continuous_intros]: + "continuous F f \ continuous F (\x. norm (f x))" + unfolding continuous_def by (rule tendsto_norm) + +lemma continuous_on_norm [continuous_on_intros]: + "continuous_on s f \ continuous_on s (\x. norm (f x))" + unfolding continuous_on_def by (auto intro: tendsto_norm) + lemma tendsto_norm_zero: "(f ---> 0) F \ ((\x. norm (f x)) ---> 0) F" by (drule tendsto_norm, simp) @@ -252,6 +260,14 @@ "(f ---> (l::real)) F \ ((\x. \f x\) ---> \l\) F" by (fold real_norm_def, rule tendsto_norm) +lemma continuous_rabs [continuous_intros]: + "continuous F f \ continuous F (\x. \f x :: real\)" + unfolding real_norm_def[symmetric] by (rule continuous_norm) + +lemma continuous_on_rabs [continuous_on_intros]: + "continuous_on s f \ continuous_on s (\x. \f x :: real\)" + unfolding real_norm_def[symmetric] by (rule continuous_on_norm) + lemma tendsto_rabs_zero: "(f ---> (0::real)) F \ ((\x. \f x\) ---> 0) F" by (fold real_norm_def, rule tendsto_norm_zero) @@ -271,8 +287,18 @@ shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x + g x) ---> a + b) F" by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) +lemma continuous_add [continuous_intros]: + fixes f g :: "'a::t2_space \ 'b::real_normed_vector" + shows "continuous F f \ continuous F g \ continuous F (\x. f x + g x)" + unfolding continuous_def by (rule tendsto_add) + +lemma continuous_on_add [continuous_on_intros]: + fixes f g :: "_ \ 'b::real_normed_vector" + shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x + g x)" + unfolding continuous_on_def by (auto intro: tendsto_add) + lemma tendsto_add_zero: - fixes f g :: "'a::type \ 'b::real_normed_vector" + fixes f g :: "_ \ 'b::real_normed_vector" shows "\(f ---> 0) F; (g ---> 0) F\ \ ((\x. f x + g x) ---> 0) F" by (drule (1) tendsto_add, simp) @@ -281,6 +307,16 @@ shows "(f ---> a) F \ ((\x. - f x) ---> - a) F" by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) +lemma continuous_minus [continuous_intros]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + shows "continuous F f \ continuous F (\x. - f x)" + unfolding continuous_def by (rule tendsto_minus) + +lemma continuous_on_minus [continuous_on_intros]: + fixes f :: "_ \ 'b::real_normed_vector" + shows "continuous_on s f \ continuous_on s (\x. - f x)" + unfolding continuous_on_def by (auto intro: tendsto_minus) + lemma tendsto_minus_cancel: fixes a :: "'a::real_normed_vector" shows "((\x. - f x) ---> - a) F \ (f ---> a) F" @@ -296,6 +332,16 @@ shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x - g x) ---> a - b) F" by (simp add: diff_minus tendsto_add tendsto_minus) +lemma continuous_diff [continuous_intros]: + fixes f g :: "'a::t2_space \ 'b::real_normed_vector" + shows "continuous F f \ continuous F g \ continuous F (\x. f x - g x)" + unfolding continuous_def by (rule tendsto_diff) + +lemma continuous_on_diff [continuous_on_intros]: + fixes f g :: "'a::t2_space \ 'b::real_normed_vector" + shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" + unfolding continuous_on_def by (auto intro: tendsto_diff) + lemma tendsto_setsum [tendsto_intros]: fixes f :: "'a \ 'b \ 'c::real_normed_vector" assumes "\i. i \ S \ (f i ---> a i) F" @@ -308,6 +354,16 @@ by (simp add: tendsto_const) qed +lemma continuous_setsum [continuous_intros]: + fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" + shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)" + unfolding continuous_def by (rule tendsto_setsum) + +lemma continuous_on_setsum [continuous_intros]: + fixes f :: "'a \ _ \ 'c::real_normed_vector" + shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)" + unfolding continuous_on_def by (auto intro: tendsto_setsum) + lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real] subsubsection {* Linear operators and multiplication *} @@ -316,6 +372,14 @@ "(g ---> a) F \ ((\x. f (g x)) ---> f a) F" by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) +lemma (in bounded_linear) continuous: + "continuous F g \ continuous F (\x. f (g x))" + using tendsto[of g _ F] by (auto simp: continuous_def) + +lemma (in bounded_linear) continuous_on: + "continuous_on s g \ continuous_on s (\x. f (g x))" + using tendsto[of g] by (auto simp: continuous_on_def) + lemma (in bounded_linear) tendsto_zero: "(g ---> 0) F \ ((\x. f (g x)) ---> 0) F" by (drule tendsto, simp only: zero) @@ -325,6 +389,14 @@ by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) +lemma (in bounded_bilinear) continuous: + "continuous F f \ continuous F g \ continuous F (\x. f x ** g x)" + using tendsto[of f _ F g] by (auto simp: continuous_def) + +lemma (in bounded_bilinear) continuous_on: + "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x ** g x)" + using tendsto[of f _ _ g] by (auto simp: continuous_on_def) + lemma (in bounded_bilinear) tendsto_zero: assumes f: "(f ---> 0) F" assumes g: "(g ---> 0) F" @@ -348,6 +420,24 @@ lemmas tendsto_mult [tendsto_intros] = bounded_bilinear.tendsto [OF bounded_bilinear_mult] +lemmas continuous_of_real [continuous_intros] = + bounded_linear.continuous [OF bounded_linear_of_real] + +lemmas continuous_scaleR [continuous_intros] = + bounded_bilinear.continuous [OF bounded_bilinear_scaleR] + +lemmas continuous_mult [continuous_intros] = + bounded_bilinear.continuous [OF bounded_bilinear_mult] + +lemmas continuous_on_of_real [continuous_on_intros] = + bounded_linear.continuous_on [OF bounded_linear_of_real] + +lemmas continuous_on_scaleR [continuous_on_intros] = + bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR] + +lemmas continuous_on_mult [continuous_on_intros] = + bounded_bilinear.continuous_on [OF bounded_bilinear_mult] + lemmas tendsto_mult_zero = bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] @@ -362,6 +452,16 @@ shows "(f ---> a) F \ ((\x. f x ^ n) ---> a ^ n) F" by (induct n) (simp_all add: tendsto_const tendsto_mult) +lemma continuous_power [continuous_intros]: + fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" + shows "continuous F f \ continuous F (\x. (f x)^n)" + unfolding continuous_def by (rule tendsto_power) + +lemma continuous_on_power [continuous_on_intros]: + fixes f :: "_ \ 'b::{power,real_normed_algebra}" + shows "continuous_on s f \ continuous_on s (\x. (f x)^n)" + unfolding continuous_on_def by (auto intro: tendsto_power) + lemma tendsto_setprod [tendsto_intros]: fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}" assumes "\i. i \ S \ (f i ---> L i) F" @@ -374,6 +474,16 @@ by (simp add: tendsto_const) qed +lemma continuous_setprod [continuous_intros]: + fixes f :: "'a \ 'b::t2_space \ 'c::{real_normed_algebra,comm_ring_1}" + shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)" + unfolding continuous_def by (rule tendsto_setprod) + +lemma continuous_on_setprod [continuous_intros]: + fixes f :: "'a \ _ \ 'c::{real_normed_algebra,comm_ring_1}" + shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)" + unfolding continuous_on_def by (auto intro: tendsto_setprod) + subsubsection {* Inverse and division *} lemma (in bounded_bilinear) Zfun_prod_Bfun: @@ -483,17 +593,89 @@ unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) qed +lemma continuous_inverse: + fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" + assumes "continuous F f" and "f (Lim F (\x. x)) \ 0" + shows "continuous F (\x. inverse (f x))" + using assms unfolding continuous_def by (rule tendsto_inverse) + +lemma continuous_at_within_inverse[continuous_intros]: + fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" + assumes "continuous (at a within s) f" and "f a \ 0" + shows "continuous (at a within s) (\x. inverse (f x))" + using assms unfolding continuous_within by (rule tendsto_inverse) + +lemma isCont_inverse[continuous_intros, simp]: + fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" + assumes "isCont f a" and "f a \ 0" + shows "isCont (\x. inverse (f x)) a" + using assms unfolding continuous_at by (rule tendsto_inverse) + +lemma continuous_on_inverse[continuous_on_intros]: + fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" + assumes "continuous_on s f" and "\x\s. f x \ 0" + shows "continuous_on s (\x. inverse (f x))" + using assms unfolding continuous_on_def by (fast intro: tendsto_inverse) + lemma tendsto_divide [tendsto_intros]: fixes a b :: "'a::real_normed_field" shows "\(f ---> a) F; (g ---> b) F; b \ 0\ \ ((\x. f x / g x) ---> a / b) F" by (simp add: tendsto_mult tendsto_inverse divide_inverse) +lemma continuous_divide: + fixes f g :: "'a::t2_space \ 'b::real_normed_field" + assumes "continuous F f" and "continuous F g" and "g (Lim F (\x. x)) \ 0" + shows "continuous F (\x. (f x) / (g x))" + using assms unfolding continuous_def by (rule tendsto_divide) + +lemma continuous_at_within_divide[continuous_intros]: + fixes f g :: "'a::t2_space \ 'b::real_normed_field" + assumes "continuous (at a within s) f" "continuous (at a within s) g" and "g a \ 0" + shows "continuous (at a within s) (\x. (f x) / (g x))" + using assms unfolding continuous_within by (rule tendsto_divide) + +lemma isCont_divide[continuous_intros, simp]: + fixes f g :: "'a::t2_space \ 'b::real_normed_field" + assumes "isCont f a" "isCont g a" "g a \ 0" + shows "isCont (\x. (f x) / g x) a" + using assms unfolding continuous_at by (rule tendsto_divide) + +lemma continuous_on_divide[continuous_on_intros]: + fixes f :: "'a::topological_space \ 'b::real_normed_field" + assumes "continuous_on s f" "continuous_on s g" and "\x\s. g x \ 0" + shows "continuous_on s (\x. (f x) / (g x))" + using assms unfolding continuous_on_def by (fast intro: tendsto_divide) + lemma tendsto_sgn [tendsto_intros]: fixes l :: "'a::real_normed_vector" shows "\(f ---> l) F; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) F" unfolding sgn_div_norm by (simp add: tendsto_intros) +lemma continuous_sgn: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + assumes "continuous F f" and "f (Lim F (\x. x)) \ 0" + shows "continuous F (\x. sgn (f x))" + using assms unfolding continuous_def by (rule tendsto_sgn) + +lemma continuous_at_within_sgn[continuous_intros]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + assumes "continuous (at a within s) f" and "f a \ 0" + shows "continuous (at a within s) (\x. sgn (f x))" + using assms unfolding continuous_within by (rule tendsto_sgn) + +lemma isCont_sgn[continuous_intros]: + fixes f :: "'a::t2_space \ 'b::real_normed_vector" + assumes "isCont f a" and "f a \ 0" + shows "isCont (\x. sgn (f x)) a" + using assms unfolding continuous_at by (rule tendsto_sgn) + +lemma continuous_on_sgn[continuous_on_intros]: + fixes f :: "'a::topological_space \ 'b::real_normed_vector" + assumes "continuous_on s f" and "\x\s. f x \ 0" + shows "continuous_on s (\x. sgn (f x))" + using assms unfolding continuous_on_def by (fast intro: tendsto_sgn) + lemma filterlim_at_infinity: fixes f :: "_ \ 'a\real_normed_vector" assumes "0 \ c" diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Log.thy --- a/src/HOL/Log.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Log.thy Fri Mar 22 10:41:43 2013 +0100 @@ -21,6 +21,29 @@ "log a x = ln x / ln a" +lemma tendsto_log [tendsto_intros]: + "\(f ---> a) F; (g ---> b) F; 0 < a; a \ 1; 0 < b\ \ ((\x. log (f x) (g x)) ---> log a b) F" + unfolding log_def by (intro tendsto_intros) auto + +lemma continuous_log: + assumes "continuous F f" and "continuous F g" and "0 < f (Lim F (\x. x))" and "f (Lim F (\x. x)) \ 1" and "0 < g (Lim F (\x. x))" + shows "continuous F (\x. log (f x) (g x))" + using assms unfolding continuous_def by (rule tendsto_log) + +lemma continuous_at_within_log[continuous_intros]: + assumes "continuous (at a within s) f" "continuous (at a within s) g" and "0 < f a" and "f a \ 1" and "0 < g a" + shows "continuous (at a within s) (\x. log (f x) (g x))" + using assms unfolding continuous_within by (rule tendsto_log) + +lemma isCont_log[continuous_intros, simp]: + assumes "isCont f a" "isCont g a" "0 < f a" "f a \ 1" "0 < g a" + shows "isCont (\x. log (f x) (g x)) a" + using assms unfolding continuous_at by (rule tendsto_log) + +lemma continuous_on_log[continuous_on_intros]: + assumes "continuous_on s f" "continuous_on s g" and "\x\s. 0 < f x" "\x\s. f x \ 1" "\x\s. 0 < g x" + shows "continuous_on s (\x. log (f x) (g x))" + using assms unfolding continuous_on_def by (fast intro: tendsto_log) lemma powr_one_eq_one [simp]: "1 powr a = 1" by (simp add: powr_def) @@ -338,6 +361,26 @@ "\(f ---> a) F; (g ---> b) F; 0 < a\ \ ((\x. f x powr g x) ---> a powr b) F" unfolding powr_def by (intro tendsto_intros) +lemma continuous_powr: + assumes "continuous F f" and "continuous F g" and "0 < f (Lim F (\x. x))" + shows "continuous F (\x. (f x) powr (g x))" + using assms unfolding continuous_def by (rule tendsto_powr) + +lemma continuous_at_within_powr[continuous_intros]: + assumes "continuous (at a within s) f" "continuous (at a within s) g" and "0 < f a" + shows "continuous (at a within s) (\x. (f x) powr (g x))" + using assms unfolding continuous_within by (rule tendsto_powr) + +lemma isCont_powr[continuous_intros, simp]: + assumes "isCont f a" "isCont g a" "0 < f a" + shows "isCont (\x. (f x) powr g x) a" + using assms unfolding continuous_at by (rule tendsto_powr) + +lemma continuous_on_powr[continuous_on_intros]: + assumes "continuous_on s f" "continuous_on s g" and "\x\s. 0 < f x" + shows "continuous_on s (\x. (f x) powr (g x))" + using assms unfolding continuous_on_def by (fast intro: tendsto_powr) + (* FIXME: generalize by replacing d by with g x and g ---> d? *) lemma tendsto_zero_powrI: assumes "eventually (\x. 0 < f x ) F" and "(f ---> 0) F" diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Metric_Spaces.thy --- a/src/HOL/Metric_Spaces.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Metric_Spaces.thy Fri Mar 22 10:41:43 2013 +0100 @@ -582,6 +582,16 @@ qed qed +lemma continuous_dist[continuous_intros]: + fixes f g :: "_ \ 'a :: metric_space" + shows "continuous F f \ continuous F g \ continuous F (\x. dist (f x) (g x))" + unfolding continuous_def by (rule tendsto_dist) + +lemma continuous_on_dist[continuous_on_intros]: + fixes f g :: "_ \ 'a :: metric_space" + shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. dist (f x) (g x))" + unfolding continuous_on_def by (auto intro: tendsto_dist) + lemma tendsto_at_topI_sequentially: fixes f :: "real \ real" assumes mono: "mono f" diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Mar 22 10:41:43 2013 +0100 @@ -26,14 +26,6 @@ lemma divide_nonneg_nonneg:assumes "a \ 0" "b \ 0" shows "0 \ a / (b::real)" apply(cases "b=0") defer apply(rule divide_nonneg_pos) using assms by auto -lemma continuous_setsum: - fixes f :: "'i \ 'a::t2_space \ 'b::real_normed_vector" - assumes f: "\i. i \ I \ continuous F (f i)" shows "continuous F (\x. \i\I. f i x)" -proof cases - assume "finite I" from this f show ?thesis - by (induct I) (auto intro!: continuous_intros) -qed (auto intro!: continuous_intros) - lemma brouwer_compactness_lemma: fixes f :: "'a::metric_space \ 'b::euclidean_space" assumes "compact s" "continuous_on s f" "\ (\x\s. (f x = 0))" diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Mar 22 10:41:43 2013 +0100 @@ -576,10 +576,6 @@ unfolding FDERIV_conv_has_derivative [symmetric] by (rule FDERIV_unique) -lemma continuous_isCont: "isCont f x = continuous (at x) f" - unfolding isCont_def LIM_def - unfolding continuous_at Lim_at unfolding dist_nz by auto - lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \ 'b::real_normed_vector" assumes "\i\Basis. a\i < b\i" "x \ {a..b}" (is "x\?I") @@ -783,15 +779,12 @@ shows "\x\{a<..x\{a<..xa. f' x xa - (f b - f a) / (b - a) * xa) = (\v. 0)" - apply(rule rolle[OF assms(1), of "\x. f x - (f b - f a) / (b - a) * x"]) - defer - apply(rule continuous_on_intros assms(2))+ - proof + proof (intro rolle[OF assms(1), of "\x. f x - (f b - f a) / (b - a) * x"] ballI) fix x assume x:"x \ {a<..x. f x - (f b - f a) / (b - a) * x) has_derivative (\xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)" by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative) - qed(insert assms(1), auto simp add:field_simps) + qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps) then guess x .. thus ?thesis apply(rule_tac x=x in bexI) apply(drule fun_cong[of _ _ "b - a"]) by auto diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Mar 22 10:41:43 2013 +0100 @@ -22,7 +22,7 @@ qed lemma square_continuous: "0 < (e::real) ==> \d. 0 < d \ (\y. abs(y - x) < d \ abs(y * y - x * x) < e)" - using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] + using isCont_power[OF isCont_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2] apply (auto simp add: power2_eq_square) apply (rule_tac x="s" in exI) apply auto diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Mar 22 10:41:43 2013 +0100 @@ -8,6 +8,14 @@ imports Convex_Euclidean_Space begin +lemma continuous_on_cong: (* MOVE to Topological_Spaces *) + "s = t \ (\x. x \ t \ f x = g x) \ continuous_on s f \ continuous_on t g" + unfolding continuous_on_def by (intro ball_cong Lim_cong_within) auto + +lemma continuous_on_compose2: + shows "continuous_on t g \ continuous_on s f \ t = f ` s \ continuous_on s (\x. g (f x))" + using continuous_on_compose[of s f g] by (simp add: comp_def) + subsection {* Paths. *} definition path :: "(real \ 'a::topological_space) \ bool" @@ -111,106 +119,32 @@ assumes "pathfinish g1 = pathstart g2" shows "path (g1 +++ g2) \ path g1 \ path g2" unfolding path_def pathfinish_def pathstart_def - apply rule defer - apply(erule conjE) -proof - - assume as: "continuous_on {0..1} (g1 +++ g2)" - have *: "g1 = (\x. g1 (2 *\<^sub>R x)) \ (\x. (1/2) *\<^sub>R x)" - "g2 = (\x. g2 (2 *\<^sub>R x - 1)) \ (\x. (1/2) *\<^sub>R (x + 1))" - unfolding o_def by (auto simp add: add_divide_distrib) - have "op *\<^sub>R (1 / 2) ` {0::real..1} \ {0..1}" - "(\x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \ {0..1}" +proof safe + assume cont: "continuous_on {0..1} (g1 +++ g2)" + have g1: "continuous_on {0..1} g1 \ continuous_on {0..1} ((g1 +++ g2) \ (\x. x / 2))" + by (intro continuous_on_cong refl) (auto simp: joinpaths_def) + have g2: "continuous_on {0..1} g2 \ continuous_on {0..1} ((g1 +++ g2) \ (\x. x / 2 + 1/2))" + using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def) + show "continuous_on {0..1} g1" "continuous_on {0..1} g2" + unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont]) +next + assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2" + have 01: "{0 .. 1} = {0..1/2} \ {1/2 .. 1::real}" by auto - then show "continuous_on {0..1} g1 \ continuous_on {0..1} g2" - apply - - apply rule - apply (subst *) defer - apply (subst *) - apply (rule_tac[!] continuous_on_compose) - apply (intro continuous_on_intros) defer - apply (intro continuous_on_intros) - apply (rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3 - apply (rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) - apply (rule as, assumption, rule as, assumption) - apply rule defer - apply rule - proof - - fix x - assume "x \ op *\<^sub>R (1 / 2) ` {0::real..1}" - then have "x \ 1 / 2" unfolding image_iff by auto - then show "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto - next - fix x - assume "x \ (\x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}" - then have "x \ 1 / 2" unfolding image_iff by auto - then show "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)" - proof (cases "x = 1 / 2") - case True - then have "x = (1/2) *\<^sub>R 1" by auto - then show ?thesis - unfolding joinpaths_def - using assms[unfolded pathstart_def pathfinish_def] - by (auto simp add: mult_ac) - qed (auto simp add:le_less joinpaths_def) - qed -next - assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2" - have *: "{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \ {(1/2) *\<^sub>R 1 .. 1}" by auto - have **: "op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" - apply (rule set_eqI, rule) - unfolding image_iff - defer - apply (rule_tac x="(1/2)*\<^sub>R x" in bexI) - apply auto - done - have ***: "(\x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}" - apply (auto simp add: image_def) - apply (rule_tac x="(x + 1) / 2" in bexI) - apply (auto simp add: add_divide_distrib) - done + { fix x :: real assume "0 \ x" "x \ 1" then have "x \ (\x. x * 2) ` {0..1 / 2}" + by (intro image_eqI[where x="x/2"]) auto } + note 1 = this + { fix x :: real assume "0 \ x" "x \ 1" then have "x \ (\x. x * 2 - 1) ` {1 / 2..1}" + by (intro image_eqI[where x="x/2 + 1/2"]) auto } + note 2 = this show "continuous_on {0..1} (g1 +++ g2)" - unfolding * - apply (rule continuous_on_union) - apply (rule closed_real_atLeastAtMost)+ - proof - - show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" - apply (rule continuous_on_eq[of _ "\x. g1 (2 *\<^sub>R x)"]) defer - unfolding o_def[THEN sym] - apply (rule continuous_on_compose) - apply (intro continuous_on_intros) - unfolding ** - apply (rule as(1)) - unfolding joinpaths_def - apply auto - done - next - show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" - apply (rule continuous_on_eq[of _ "g2 \ (\x. 2 *\<^sub>R x - 1)"]) defer - apply (rule continuous_on_compose) - apply (intro continuous_on_intros) - unfolding *** o_def joinpaths_def - apply (rule as(2)) - using assms[unfolded pathstart_def pathfinish_def] - apply (auto simp add: mult_ac) - done - qed + using assms unfolding joinpaths_def 01 + by (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros) + (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) qed lemma path_image_join_subset: "path_image(g1 +++ g2) \ (path_image g1 \ path_image g2)" -proof - fix x - assume "x \ path_image (g1 +++ g2)" - then obtain y where y:"y\{0..1}" "x = (if y \ 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))" - unfolding path_image_def image_iff joinpaths_def by auto - then show "x \ path_image g1 \ path_image g2" - apply (cases "y \ 1/2") - apply (rule_tac UnI1) defer - apply (rule_tac UnI2) - unfolding y(2) path_image_def - using y(1) - apply (auto intro!: imageI) - done -qed + unfolding path_image_def joinpaths_def by auto lemma subset_path_image_join: assumes "path_image g1 \ s" "path_image g2 \ s" @@ -218,7 +152,7 @@ using path_image_join_subset[of g1 g2] and assms by auto lemma path_image_join: - assumes "path g1" "path g2" "pathfinish g1 = pathstart g2" + assumes "pathfinish g1 = pathstart g2" shows "path_image(g1 +++ g2) = (path_image g1) \ (path_image g2)" apply (rule, rule path_image_join_subset, rule) unfolding Un_iff @@ -240,7 +174,7 @@ then show "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) - using assms(3)[unfolded pathfinish_def pathstart_def] + using assms(1)[unfolded pathfinish_def pathstart_def] apply (auto simp add: add_divide_distrib) done qed diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100 @@ -1273,18 +1273,6 @@ subsection {* Limits *} -text{* Notation Lim to avoid collition with lim defined in analysis *} - -definition Lim :: "'a filter \ ('a \ 'b::t2_space) \ 'b" - where "Lim A f = (THE l. (f ---> l) A)" - -text{* Uniqueness of the limit, when nontrivial. *} - -lemma tendsto_Lim: - fixes f :: "'a \ 'b::t2_space" - shows "~(trivial_limit net) \ (f ---> l) net ==> Lim net f = l" - unfolding Lim_def using tendsto_unique[of net f] by auto - lemma Lim: "(f ---> l) net \ trivial_limit net \ @@ -3769,35 +3757,6 @@ subsection {* Continuity *} -text {* Define continuity over a net to take in restrictions of the set. *} - -definition - continuous :: "'a::t2_space filter \ ('a \ 'b::topological_space) \ bool" - where "continuous net f \ (f ---> f(netlimit net)) net" - -lemma continuous_trivial_limit: - "trivial_limit net ==> continuous net f" - unfolding continuous_def tendsto_def trivial_limit_eq by auto - -lemma continuous_within: "continuous (at x within s) f \ (f ---> f(x)) (at x within s)" - unfolding continuous_def - unfolding tendsto_def - using netlimit_within[of x s] - by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually) - -lemma continuous_at: "continuous (at x) f \ (f ---> f(x)) (at x)" - using continuous_within [of x UNIV f] by simp - -lemma continuous_isCont: "isCont f x = continuous (at x) f" - unfolding isCont_def LIM_def - unfolding continuous_at Lim_at unfolding dist_nz by auto - -lemma continuous_at_within: - assumes "continuous (at x) f" shows "continuous (at x within s) f" - using assms unfolding continuous_at continuous_within - by (rule Lim_at_within) - - text{* Derive the epsilon-delta forms, which we often use as "definitions" *} lemma continuous_within_eps_delta: @@ -3843,20 +3802,6 @@ text{* Define setwise continuity in terms of limits within the set. *} -definition - continuous_on :: - "'a set \ ('a::topological_space \ 'b::topological_space) \ bool" -where - "continuous_on s f \ (\x\s. (f ---> f x) (at x within s))" - -lemma continuous_on_topological: - "continuous_on s f \ - (\x\s. \B. open B \ f x \ B \ - (\A. open A \ x \ A \ (\y\s. y \ A \ f y \ B)))" -unfolding continuous_on_def tendsto_def -unfolding Limits.eventually_within eventually_at_topological -by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto - lemma continuous_on_iff: "continuous_on s f \ (\x\s. \e>0. \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) < e)" @@ -3884,38 +3829,7 @@ unfolding continuous_within continuous_at using Lim_at_within by auto lemma Lim_trivial_limit: "trivial_limit net \ (f ---> l) net" -unfolding tendsto_def by (simp add: trivial_limit_eq) - -lemma continuous_at_imp_continuous_on: - assumes "\x\s. continuous (at x) f" - shows "continuous_on s f" -unfolding continuous_on_def -proof - fix x assume "x \ s" - with assms have *: "(f ---> f (netlimit (at x))) (at x)" - unfolding continuous_def by simp - have "(f ---> f x) (at x)" - proof (cases "trivial_limit (at x)") - case True thus ?thesis - by (rule Lim_trivial_limit) - next - case False - hence 1: "netlimit (at x) = x" - using netlimit_within [of x UNIV] by simp - with * show ?thesis by simp - qed - thus "(f ---> f x) (at x within s)" - by (rule Lim_at_within) -qed - -lemma continuous_on_eq_continuous_within: - "continuous_on s f \ (\x \ s. continuous (at x within s) f)" -unfolding continuous_on_def continuous_def -apply (rule ball_cong [OF refl]) -apply (case_tac "trivial_limit (at x within s)") -apply (simp add: Lim_trivial_limit) -apply (simp add: netlimit_within) -done + by simp lemmas continuous_on = continuous_on_def -- "legacy theorem name" @@ -4056,169 +3970,32 @@ subsubsection {* Structural rules for pointwise continuity *} -ML {* - -structure Continuous_Intros = Named_Thms -( - val name = @{binding continuous_intros} - val description = "Structural introduction rules for pointwise continuity" -) - -*} - -setup Continuous_Intros.setup - -lemma continuous_within_id[continuous_intros]: "continuous (at a within s) (\x. x)" - unfolding continuous_within by (rule tendsto_ident_at_within) - -lemma continuous_at_id[continuous_intros]: "continuous (at a) (\x. x)" - unfolding continuous_at by (rule tendsto_ident_at) - -lemma continuous_const[continuous_intros]: "continuous F (\x. c)" - unfolding continuous_def by (rule tendsto_const) - -lemma continuous_fst[continuous_intros]: "continuous F f \ continuous F (\x. fst (f x))" - unfolding continuous_def by (rule tendsto_fst) - -lemma continuous_snd[continuous_intros]: "continuous F f \ continuous F (\x. snd (f x))" - unfolding continuous_def by (rule tendsto_snd) - -lemma continuous_Pair[continuous_intros]: "continuous F f \ continuous F g \ continuous F (\x. (f x, g x))" - unfolding continuous_def by (rule tendsto_Pair) - -lemma continuous_dist[continuous_intros]: - assumes "continuous F f" and "continuous F g" - shows "continuous F (\x. dist (f x) (g x))" - using assms unfolding continuous_def by (rule tendsto_dist) +lemmas continuous_within_id = continuous_ident + +lemmas continuous_at_id = isCont_ident lemma continuous_infdist[continuous_intros]: assumes "continuous F f" shows "continuous F (\x. infdist (f x) A)" using assms unfolding continuous_def by (rule tendsto_infdist) -lemma continuous_norm[continuous_intros]: - shows "continuous F f \ continuous F (\x. norm (f x))" - unfolding continuous_def by (rule tendsto_norm) - lemma continuous_infnorm[continuous_intros]: shows "continuous F f \ continuous F (\x. infnorm (f x))" unfolding continuous_def by (rule tendsto_infnorm) -lemma continuous_add[continuous_intros]: - fixes f g :: "'a::t2_space \ 'b::real_normed_vector" - shows "\continuous F f; continuous F g\ \ continuous F (\x. f x + g x)" - unfolding continuous_def by (rule tendsto_add) - -lemma continuous_minus[continuous_intros]: - fixes f :: "'a::t2_space \ 'b::real_normed_vector" - shows "continuous F f \ continuous F (\x. - f x)" - unfolding continuous_def by (rule tendsto_minus) - -lemma continuous_diff[continuous_intros]: - fixes f g :: "'a::t2_space \ 'b::real_normed_vector" - shows "\continuous F f; continuous F g\ \ continuous F (\x. f x - g x)" - unfolding continuous_def by (rule tendsto_diff) - -lemma continuous_scaleR[continuous_intros]: - fixes g :: "'a::t2_space \ 'b::real_normed_vector" - shows "\continuous F f; continuous F g\ \ continuous F (\x. f x *\<^sub>R g x)" - unfolding continuous_def by (rule tendsto_scaleR) - -lemma continuous_mult[continuous_intros]: - fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" - shows "\continuous F f; continuous F g\ \ continuous F (\x. f x * g x)" - unfolding continuous_def by (rule tendsto_mult) - lemma continuous_inner[continuous_intros]: assumes "continuous F f" and "continuous F g" shows "continuous F (\x. inner (f x) (g x))" using assms unfolding continuous_def by (rule tendsto_inner) -lemma continuous_inverse[continuous_intros]: - fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" - assumes "continuous F f" and "f (netlimit F) \ 0" - shows "continuous F (\x. inverse (f x))" - using assms unfolding continuous_def by (rule tendsto_inverse) - -lemma continuous_at_within_inverse[continuous_intros]: - fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" - assumes "continuous (at a within s) f" and "f a \ 0" - shows "continuous (at a within s) (\x. inverse (f x))" - using assms unfolding continuous_within by (rule tendsto_inverse) - -lemma continuous_at_inverse[continuous_intros]: - fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" - assumes "continuous (at a) f" and "f a \ 0" - shows "continuous (at a) (\x. inverse (f x))" - using assms unfolding continuous_at by (rule tendsto_inverse) +lemmas continuous_at_inverse = isCont_inverse subsubsection {* Structural rules for setwise continuity *} -ML {* - -structure Continuous_On_Intros = Named_Thms -( - val name = @{binding continuous_on_intros} - val description = "Structural introduction rules for setwise continuity" -) - -*} - -setup Continuous_On_Intros.setup - -lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\x. x)" - unfolding continuous_on_def by (fast intro: tendsto_ident_at_within) - -lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\x. c)" - unfolding continuous_on_def by (auto intro: tendsto_intros) - -lemma continuous_on_norm[continuous_on_intros]: - shows "continuous_on s f \ continuous_on s (\x. norm (f x))" - unfolding continuous_on_def by (fast intro: tendsto_norm) - lemma continuous_on_infnorm[continuous_on_intros]: shows "continuous_on s f \ continuous_on s (\x. infnorm (f x))" unfolding continuous_on by (fast intro: tendsto_infnorm) -lemma continuous_on_minus[continuous_on_intros]: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "continuous_on s f \ continuous_on s (\x. - f x)" - unfolding continuous_on_def by (auto intro: tendsto_intros) - -lemma continuous_on_add[continuous_on_intros]: - fixes f g :: "'a::topological_space \ 'b::real_normed_vector" - shows "continuous_on s f \ continuous_on s g - \ continuous_on s (\x. f x + g x)" - unfolding continuous_on_def by (auto intro: tendsto_intros) - -lemma continuous_on_diff[continuous_on_intros]: - fixes f g :: "'a::topological_space \ 'b::real_normed_vector" - shows "continuous_on s f \ continuous_on s g - \ continuous_on s (\x. f x - g x)" - unfolding continuous_on_def by (auto intro: tendsto_intros) - -lemma (in bounded_linear) continuous_on[continuous_on_intros]: - "continuous_on s g \ continuous_on s (\x. f (g x))" - unfolding continuous_on_def by (fast intro: tendsto) - -lemma (in bounded_bilinear) continuous_on[continuous_on_intros]: - "\continuous_on s f; continuous_on s g\ \ continuous_on s (\x. f x ** g x)" - unfolding continuous_on_def by (fast intro: tendsto) - -lemma continuous_on_scaleR[continuous_on_intros]: - fixes g :: "'a::topological_space \ 'b::real_normed_vector" - assumes "continuous_on s f" and "continuous_on s g" - shows "continuous_on s (\x. f x *\<^sub>R g x)" - using bounded_bilinear_scaleR assms - by (rule bounded_bilinear.continuous_on) - -lemma continuous_on_mult[continuous_on_intros]: - fixes g :: "'a::topological_space \ 'b::real_normed_algebra" - assumes "continuous_on s f" and "continuous_on s g" - shows "continuous_on s (\x. f x * g x)" - using bounded_bilinear_mult assms - by (rule bounded_bilinear.continuous_on) - lemma continuous_on_inner[continuous_on_intros]: fixes g :: "'a::topological_space \ 'b::real_inner" assumes "continuous_on s f" and "continuous_on s g" @@ -4226,12 +4003,6 @@ using bounded_bilinear_inner assms by (rule bounded_bilinear.continuous_on) -lemma continuous_on_inverse[continuous_on_intros]: - fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" - assumes "continuous_on s f" and "\x\s. f x \ 0" - shows "continuous_on s (\x. inverse (f x))" - using assms unfolding continuous_on by (fast intro: tendsto_inverse) - subsubsection {* Structural rules for uniform continuity *} lemma uniformly_continuous_on_id[continuous_on_intros]: @@ -4312,33 +4083,7 @@ text{* Continuity of all kinds is preserved under composition. *} -lemma continuous_within_topological: - "continuous (at x within s) f \ - (\B. open B \ f x \ B \ - (\A. open A \ x \ A \ (\y\s. y \ A \ f y \ B)))" -unfolding continuous_within -unfolding tendsto_def Limits.eventually_within eventually_at_topological -by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto - -lemma continuous_within_compose[continuous_intros]: - assumes "continuous (at x within s) f" - assumes "continuous (at (f x) within f ` s) g" - shows "continuous (at x within s) (g o f)" -using assms unfolding continuous_within_topological by simp metis - -lemma continuous_at_compose[continuous_intros]: - assumes "continuous (at x) f" and "continuous (at (f x)) g" - shows "continuous (at x) (g o f)" -proof- - have "continuous (at (f x) within range f) g" using assms(2) - using continuous_within_subset[of "f x" UNIV g "range f"] by simp - thus ?thesis using assms(1) - using continuous_within_compose[of x UNIV f g] by simp -qed - -lemma continuous_on_compose[continuous_on_intros]: - "continuous_on s f \ continuous_on (f ` s) g \ continuous_on s (g o f)" - unfolding continuous_on_topological by simp metis +lemmas continuous_at_compose = isCont_o lemma uniformly_continuous_on_compose[continuous_on_intros]: assumes "uniformly_continuous_on s f" "uniformly_continuous_on (f ` s) g" @@ -5182,8 +4927,7 @@ have "compact (s \ s)" using `compact s` by (intro compact_Times) moreover have "s \ s \ {}" using `s \ {}` by auto moreover have "continuous_on (s \ s) (\x. dist (fst x) (snd x))" - by (intro continuous_at_imp_continuous_on ballI continuous_dist - continuous_isCont[THEN iffD1] isCont_fst isCont_snd isCont_ident) + by (intro continuous_at_imp_continuous_on ballI continuous_intros) ultimately show ?thesis using continuous_attains_sup[of "s \ s" "\x. dist (fst x) (snd x)"] by auto qed @@ -5873,7 +5617,7 @@ by (rule isCont_open_vimage) lemma open_Collect_less: - fixes f g :: "'a::topological_space \ real" + fixes f g :: "'a::t2_space \ real" assumes f: "\x. isCont f x" assumes g: "\x. isCont g x" shows "open {x. f x < g x}" @@ -5887,7 +5631,7 @@ qed lemma closed_Collect_le: - fixes f g :: "'a::topological_space \ real" + fixes f g :: "'a::t2_space \ real" assumes f: "\x. isCont f x" assumes g: "\x. isCont g x" shows "closed {x. f x \ g x}" @@ -5901,7 +5645,7 @@ qed lemma closed_Collect_eq: - fixes f g :: "'a::topological_space \ 'b::t2_space" + fixes f g :: "'a::t2_space \ 'b::t2_space" assumes f: "\x. isCont f x" assumes g: "\x. isCont g x" shows "closed {x. f x = g x}" diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/NthRoot.thy Fri Mar 22 10:41:43 2013 +0100 @@ -338,6 +338,18 @@ apply (simp_all add: isCont_root_pos isCont_root_neg isCont_root_zero) done +lemma tendsto_real_root[tendsto_intros]: + "(f ---> x) F \ 0 < n \ ((\x. root n (f x)) ---> root n x) F" + using isCont_tendsto_compose[OF isCont_real_root, of n f x F] . + +lemma continuous_real_root[continuous_intros]: + "continuous F f \ 0 < n \ continuous F (\x. root n (f x))" + unfolding continuous_def by (rule tendsto_real_root) + +lemma continuous_on_real_root[continuous_on_intros]: + "continuous_on s f \ 0 < n \ continuous_on s (\x. root n (f x))" + unfolding continuous_on_def by (auto intro: tendsto_real_root) + lemma DERIV_real_root: assumes n: "0 < n" assumes x: "0 < x" @@ -491,6 +503,18 @@ lemma isCont_real_sqrt: "isCont sqrt x" unfolding sqrt_def by (rule isCont_real_root [OF pos2]) +lemma tendsto_real_sqrt[tendsto_intros]: + "(f ---> x) F \ ((\x. sqrt (f x)) ---> sqrt x) F" + unfolding sqrt_def by (rule tendsto_real_root [OF _ pos2]) + +lemma continuous_real_sqrt[continuous_intros]: + "continuous F f \ continuous F (\x. sqrt (f x))" + unfolding sqrt_def by (rule continuous_real_root [OF _ pos2]) + +lemma continuous_on_real_sqrt[continuous_on_intros]: + "continuous_on s f \ 0 < n \ continuous_on s (\x. sqrt (f x))" + unfolding sqrt_def by (rule continuous_on_real_root [OF _ pos2]) + lemma DERIV_real_sqrt_generic: assumes "x \ 0" assumes "x > 0 \ D = inverse (sqrt x) / 2" diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Probability/Borel_Space.thy Fri Mar 22 10:41:43 2013 +0100 @@ -675,11 +675,6 @@ by (rule borel_measurable_continuous_Pair) (auto intro: continuous_on_fst continuous_on_snd continuous_on_mult) -lemma continuous_on_dist: - fixes f :: "'a :: t2_space \ 'b :: metric_space" - shows "continuous_on A f \ continuous_on A g \ continuous_on A (\x. dist (f x) (g x))" - unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist) - lemma borel_measurable_dist[measurable (raw)]: fixes g f :: "'a \ 'b::ordered_euclidean_space" assumes f: "f \ borel_measurable M" @@ -794,8 +789,7 @@ have "(\x. if f x \ {0<..} then ln (f x) else ln 0) \ borel_measurable M" proof (rule borel_measurable_continuous_on_open[OF _ _ f]) show "continuous_on {0<..} ln" - by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont - simp: continuous_isCont[symmetric]) + by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont) show "open ({0<..}::real set)" by auto qed also have "(\x. if x \ {0<..} then ln x else ln 0) = ln" @@ -808,8 +802,7 @@ unfolding log_def by auto lemma borel_measurable_exp[measurable]: "exp \ borel_measurable borel" - by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI - continuous_isCont[THEN iffD1] isCont_exp) + by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) lemma measurable_count_space_eq2_countable: fixes f :: "'a => 'c::countable" diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Mar 22 10:41:43 2013 +0100 @@ -1049,7 +1049,7 @@ let ?g = "\x. if x = a then f a else if x = b then f b else if x \ {a <..< b} then f x else 0" from f have "continuous_on {a <..< b} f" - by (subst continuous_on_eq_continuous_at) (auto simp add: continuous_isCont) + by (subst continuous_on_eq_continuous_at) auto then have "?g \ borel_measurable borel" using borel_measurable_continuous_on_open[of "{a <..< b }" f "\x. x" borel 0] by (auto intro!: measurable_If[where P="\x. x = a"] measurable_If[where P="\x. x = b"]) diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100 @@ -39,6 +39,15 @@ lemma open_INT [intro]: "finite A \ \x\A. open (B x) \ open (\x\A. B x)" unfolding INF_def by (rule open_Inter) auto +lemma openI: + assumes "\x. x \ S \ \T. open T \ x \ T \ T \ S" + shows "open S" +proof - + have "open (\{T. open T \ T \ S})" by auto + moreover have "\{T. open T \ T \ S} = S" by (auto dest!: assms) + ultimately show "open S" by simp +qed + lemma closed_empty [intro, simp]: "closed {}" unfolding closed_def by simp @@ -835,6 +844,9 @@ tendsto :: "('b \ 'a) \ 'a \ 'b filter \ bool" (infixr "--->" 55) where "(f ---> l) F \ filterlim f (nhds l) F" +definition (in t2_space) Lim :: "'f filter \ ('f \ 'a) \ 'a" where + "Lim A f = (THE l. (f ---> l) A)" + lemma tendsto_eq_rhs: "(f ---> x) F \ x = y \ (f ---> y) F" by simp @@ -919,11 +931,10 @@ "((\x. x) ---> a) (at a within S)" unfolding tendsto_def eventually_within eventually_at_topological by auto -lemma tendsto_const [tendsto_intros]: "((\x. k) ---> k) F" +lemma (in topological_space) tendsto_const [tendsto_intros]: "((\x. k) ---> k) F" by (simp add: tendsto_def) -lemma tendsto_unique: - fixes f :: "'a \ 'b::t2_space" +lemma (in t2_space) tendsto_unique: assumes "\ trivial_limit F" and "(f ---> a) F" and "(f ---> b) F" shows "a = b" proof (rule ccontr) @@ -946,9 +957,8 @@ by (simp add: trivial_limit_def) qed -lemma tendsto_const_iff: - fixes a b :: "'a::t2_space" - assumes "\ trivial_limit F" shows "((\x. a) ---> b) F \ a = b" +lemma (in t2_space) tendsto_const_iff: + assumes "\ trivial_limit F" shows "((\x. a :: 'a) ---> b) F \ a = b" by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) lemma increasing_tendsto: @@ -1003,6 +1013,18 @@ shows "a \ x" using F x tendsto_const a by (rule tendsto_le) +subsubsection {* Rules about @{const Lim} *} + +lemma (in t2_space) tendsto_Lim: + "\(trivial_limit net) \ (f ---> l) net \ Lim net f = l" + unfolding Lim_def using tendsto_unique[of net f] by auto + +lemma Lim_ident_at: "\ trivial_limit (at x) \ Lim (at x) (\x. x) = x" + by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto + +lemma Lim_ident_at_within: "\ trivial_limit (at x within s) \ Lim (at x within s) (\x. x) = x" + by (rule tendsto_Lim[OF _ tendsto_ident_at_within]) auto + subsection {* Limits to @{const at_top} and @{const at_bot} *} lemma filterlim_at_top: @@ -1132,14 +1154,15 @@ ("((_)/ ----> (_))" [60, 60] 60) where "X ----> L \ (X ---> L) sequentially" -definition - lim :: "(nat \ 'a::t2_space) \ 'a" where - --{*Standard definition of limit using choice operator*} - "lim X = (THE L. X ----> L)" +abbreviation (in t2_space) lim :: "(nat \ 'a) \ 'a" where + "lim X \ Lim sequentially X" definition (in topological_space) convergent :: "(nat \ 'a) \ bool" where "convergent X = (\L. X ----> L)" +lemma lim_def: "lim X = (THE L. X ----> L)" + unfolding Lim_def .. + subsubsection {* Monotone sequences and subsequences *} definition @@ -1608,23 +1631,154 @@ subsection {* Continuity *} -definition isCont :: "('a::topological_space \ 'b::topological_space) \ 'a \ bool" where - "isCont f a \ f -- a --> f a" +subsubsection {* Continuity on a set *} + +definition continuous_on :: "'a set \ ('a :: topological_space \ 'b :: topological_space) \ bool" where + "continuous_on s f \ (\x\s. (f ---> f x) (at x within s))" + +lemma continuous_on_topological: + "continuous_on s f \ + (\x\s. \B. open B \ f x \ B \ (\A. open A \ x \ A \ (\y\s. y \ A \ f y \ B)))" + unfolding continuous_on_def tendsto_def eventually_within eventually_at_topological by metis + +lemma continuous_on_open_invariant: + "continuous_on s f \ (\B. open B \ (\A. open A \ A \ s = f -` B \ s))" +proof safe + fix B :: "'b set" assume "continuous_on s f" "open B" + then have "\x\f -` B \ s. (\A. open A \ x \ A \ s \ A \ f -` B)" + by (auto simp: continuous_on_topological subset_eq Ball_def imp_conjL) + then guess A unfolding bchoice_iff .. + then show "\A. open A \ A \ s = f -` B \ s" + by (intro exI[of _ "\x\f -` B \ s. A x"]) auto +next + assume B: "\B. open B \ (\A. open A \ A \ s = f -` B \ s)" + show "continuous_on s f" + unfolding continuous_on_topological + proof safe + fix x B assume "x \ s" "open B" "f x \ B" + with B obtain A where A: "open A" "A \ s = f -` B \ s" by auto + with `x \ s` `f x \ B` show "\A. open A \ x \ A \ (\y\s. y \ A \ f y \ B)" + by (intro exI[of _ A]) auto + qed +qed + +lemma continuous_on_closed_invariant: + "continuous_on s f \ (\B. closed B \ (\A. closed A \ A \ s = f -` B \ s))" +proof - + have *: "\P Q::'b set\bool. (\A. P A \ Q (- A)) \ (\A. P A) \ (\A. Q A)" + by (metis double_compl) + show ?thesis + unfolding continuous_on_open_invariant by (intro *) (auto simp: open_closed[symmetric]) +qed + +ML {* + +structure Continuous_On_Intros = Named_Thms +( + val name = @{binding continuous_on_intros} + val description = "Structural introduction rules for setwise continuity" +) + +*} + +setup Continuous_On_Intros.setup + +lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\x. x)" + unfolding continuous_on_def by (fast intro: tendsto_ident_at_within) + +lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\x. c)" + unfolding continuous_on_def by (auto intro: tendsto_const) + +lemma continuous_on_compose[continuous_on_intros]: + "continuous_on s f \ continuous_on (f ` s) g \ continuous_on s (g o f)" + unfolding continuous_on_topological by simp metis + +subsubsection {* Continuity at a point *} + +definition continuous :: "'a::t2_space filter \ ('a \ 'b::topological_space) \ bool" where + "continuous F f \ (f ---> f (Lim F (\x. x))) F" + +ML {* -lemma isCont_ident [simp]: "isCont (\x. x) a" - unfolding isCont_def by (rule tendsto_ident_at) +structure Continuous_Intros = Named_Thms +( + val name = @{binding continuous_intros} + val description = "Structural introduction rules for pointwise continuity" +) + +*} + +setup Continuous_Intros.setup + +lemma continuous_bot[continuous_intros, simp]: "continuous bot f" + unfolding continuous_def by auto + +lemma continuous_trivial_limit: "trivial_limit net \ continuous net f" + by simp + +lemma continuous_within: "continuous (at x within s) f \ (f ---> f x) (at x within s)" + by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at_within continuous_def) + +lemma continuous_within_topological: + "continuous (at x within s) f \ + (\B. open B \ f x \ B \ (\A. open A \ x \ A \ (\y\s. y \ A \ f y \ B)))" + unfolding continuous_within tendsto_def eventually_within eventually_at_topological by metis + +lemma continuous_within_compose[continuous_intros]: + "continuous (at x within s) f \ continuous (at (f x) within f ` s) g \ + continuous (at x within s) (g o f)" + by (simp add: continuous_within_topological) metis + +lemma continuous_within_compose2: + "continuous (at x within s) f \ continuous (at (f x) within f ` s) g \ + continuous (at x within s) (\x. g (f x))" + using continuous_within_compose[of x s f g] by (simp add: comp_def) -lemma isCont_const [simp]: "isCont (\x. k) a" - unfolding isCont_def by (rule tendsto_const) +lemma continuous_at: "continuous (at x) f \ f -- x --> f x" + using continuous_within[of x UNIV f] by simp + +lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\x. x)" + unfolding continuous_within by (rule tendsto_ident_at_within) + +lemma continuous_const[continuous_intros, simp]: "continuous F (\x. c)" + unfolding continuous_def by (rule tendsto_const) + +lemma continuous_on_eq_continuous_within: + "continuous_on s f \ (\x\s. continuous (at x within s) f)" + unfolding continuous_on_def continuous_within .. + +abbreviation isCont :: "('a::t2_space \ 'b::topological_space) \ 'a \ bool" where + "isCont f a \ continuous (at a) f" + +lemma isCont_def: "isCont f a \ f -- a --> f a" + by (rule continuous_at) + +lemma continuous_at_within: "isCont f x \ continuous (at x within s) f" + by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within) + +lemma continuous_at_imp_continuous_on: "\x\s. isCont f x \ continuous_on s f" + by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within) + +lemma isContI_continuous: "continuous (at x within UNIV) f \ isCont f x" + by simp + +lemma isCont_ident[continuous_intros, simp]: "isCont (\x. x) a" + using continuous_ident by (rule isContI_continuous) + +lemmas isCont_const = continuous_const + +lemma isCont_o2: "isCont f a \ isCont g (f a) \ isCont (\x. g (f x)) a" + unfolding isCont_def by (rule tendsto_compose) + +lemma isCont_o[continuous_intros]: "isCont f a \ isCont g (f a) \ isCont (g \ f) a" + unfolding o_def by (rule isCont_o2) lemma isCont_tendsto_compose: "isCont g l \ (f ---> l) F \ ((\x. g (f x)) ---> g l) F" unfolding isCont_def by (rule tendsto_compose) -lemma isCont_o2: "isCont f a \ isCont g (f a) \ isCont (\x. g (f x)) a" - unfolding isCont_def by (rule tendsto_compose) - -lemma isCont_o: "isCont f a \ isCont g (f a) \ isCont (g o f) a" - unfolding o_def by (rule isCont_o2) +lemma continuous_within_compose3: + "isCont g (f x) \ continuous (at x within s) f \ continuous (at x within s) (\x. g (f x))" + using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within) end diff -r 2990382dc066 -r 270b21f3ae0a src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Fri Mar 22 10:41:43 2013 +0100 +++ b/src/HOL/Transcendental.thy Fri Mar 22 10:41:43 2013 +0100 @@ -881,6 +881,12 @@ "(f ---> a) F \ ((\x. exp (f x)) ---> exp a) F" by (rule isCont_tendsto_compose [OF isCont_exp]) +lemma continuous_exp [continuous_intros]: "continuous F f \ continuous F (\x. exp (f x))" + unfolding continuous_def by (rule tendsto_exp) + +lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \ continuous_on s (\x. exp (f x))" + unfolding continuous_on_def by (auto intro: tendsto_exp) + subsubsection {* Properties of the Exponential Function *} lemma powser_zero: @@ -1169,6 +1175,22 @@ "\(f ---> a) F; 0 < a\ \ ((\x. ln (f x)) ---> ln a) F" by (rule isCont_tendsto_compose [OF isCont_ln]) +lemma continuous_ln: + "continuous F f \ 0 < f (Lim F (\x. x)) \ continuous F (\x. ln (f x))" + unfolding continuous_def by (rule tendsto_ln) + +lemma isCont_ln' [continuous_intros]: + "continuous (at x) f \ 0 < f x \ continuous (at x) (\x. ln (f x))" + unfolding continuous_at by (rule tendsto_ln) + +lemma continuous_within_ln [continuous_intros]: + "continuous (at x within s) f \ 0 < f x \ continuous (at x within s) (\x. ln (f x))" + unfolding continuous_within by (rule tendsto_ln) + +lemma continuous_on_ln [continuous_on_intros]: + "continuous_on s f \ (\x\s. 0 < f x) \ continuous_on s (\x. ln (f x))" + unfolding continuous_on_def by (auto intro: tendsto_ln) + lemma DERIV_ln: "0 < x \ DERIV ln x :> inverse x" apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"]) apply (erule DERIV_cong [OF DERIV_exp exp_ln]) @@ -1449,6 +1471,22 @@ "(f ---> a) F \ ((\x. cos (f x)) ---> cos a) F" by (rule isCont_tendsto_compose [OF isCont_cos]) +lemma continuous_sin [continuous_intros]: + "continuous F f \ continuous F (\x. sin (f x))" + unfolding continuous_def by (rule tendsto_sin) + +lemma continuous_on_sin [continuous_on_intros]: + "continuous_on s f \ continuous_on s (\x. sin (f x))" + unfolding continuous_on_def by (auto intro: tendsto_sin) + +lemma continuous_cos [continuous_intros]: + "continuous F f \ continuous F (\x. cos (f x))" + unfolding continuous_def by (rule tendsto_cos) + +lemma continuous_on_cos [continuous_on_intros]: + "continuous_on s f \ continuous_on s (\x. cos (f x))" + unfolding continuous_on_def by (auto intro: tendsto_cos) + declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] @@ -2076,6 +2114,22 @@ "\(f ---> a) F; cos a \ 0\ \ ((\x. tan (f x)) ---> tan a) F" by (rule isCont_tendsto_compose [OF isCont_tan]) +lemma continuous_tan: + "continuous F f \ cos (f (Lim F (\x. x))) \ 0 \ continuous F (\x. tan (f x))" + unfolding continuous_def by (rule tendsto_tan) + +lemma isCont_tan'' [continuous_intros]: + "continuous (at x) f \ cos (f x) \ 0 \ continuous (at x) (\x. tan (f x))" + unfolding continuous_at by (rule tendsto_tan) + +lemma continuous_within_tan [continuous_intros]: + "continuous (at x within s) f \ cos (f x) \ 0 \ continuous (at x within s) (\x. tan (f x))" + unfolding continuous_within by (rule tendsto_tan) + +lemma continuous_on_tan [continuous_on_intros]: + "continuous_on s f \ (\x\s. cos (f x) \ 0) \ continuous_on s (\x. tan (f x))" + unfolding continuous_on_def by (auto intro: tendsto_tan) + lemma LIM_cos_div_sin: "(%x. cos(x)/sin(x)) -- pi/2 --> 0" by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all) @@ -2403,7 +2457,7 @@ lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \ x = 0" using arctan_eq_iff [of x 0] by simp -lemma isCont_inverse_function2: +lemma isCont_inverse_function2: (* generalize with continuous_on *) fixes f g :: "real \ real" shows "\a < x; x < b; \z. a \ z \ z \ b \ g (f z) = z; @@ -2414,7 +2468,7 @@ apply (simp_all add: abs_le_iff) done -lemma isCont_arcsin: "\-1 < x; x < 1\ \ isCont arcsin x" +lemma isCont_arcsin: "\-1 < x; x < 1\ \ isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *) apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp) apply (rule isCont_inverse_function2 [where f=sin]) apply (erule (1) arcsin_lt_bounded [THEN conjunct1]) @@ -2422,7 +2476,7 @@ apply (fast intro: arcsin_sin, simp) done -lemma isCont_arccos: "\-1 < x; x < 1\ \ isCont arccos x" +lemma isCont_arccos: "\-1 < x; x < 1\ \ isCont arccos x" (* generalize with continuous_on {-1 .. 1} *) apply (subgoal_tac "isCont arccos (cos (arccos x))", simp) apply (rule isCont_inverse_function2 [where f=cos]) apply (erule (1) arccos_lt_bounded [THEN conjunct1]) @@ -2439,6 +2493,15 @@ apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le) done +lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \ ((\x. arctan (f x)) ---> arctan x) F" + by (rule isCont_tendsto_compose [OF isCont_arctan]) + +lemma continuous_arctan [continuous_intros]: "continuous F f \ continuous F (\x. arctan (f x))" + unfolding continuous_def by (rule tendsto_arctan) + +lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \ continuous_on s (\x. arctan (f x))" + unfolding continuous_on_def by (auto intro: tendsto_arctan) + lemma DERIV_arcsin: "\-1 < x; x < 1\ \ DERIV arcsin x :> inverse (sqrt (1 - x\))" apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])