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)
--- 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 "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
- shows "open S"
-proof -
- have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
- moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)
- ultimately show "open S" by simp
-qed
-
lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
unfolding image_def subset_eq by force
@@ -202,15 +193,23 @@
(simp add: subsetD [OF `A \<times> B \<subseteq> S`])
qed
+lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
+ unfolding continuous_def by (rule tendsto_fst)
+
+lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
+ unfolding continuous_def by (rule tendsto_snd)
+
+lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
+ unfolding continuous_def by (rule tendsto_Pair)
+
lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
- unfolding isCont_def by (rule tendsto_fst)
+ by (fact continuous_fst)
lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
- unfolding isCont_def by (rule tendsto_snd)
+ by (fact continuous_snd)
-lemma isCont_Pair [simp]:
- "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
- unfolding isCont_def by (rule tendsto_Pair)
+lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
+ by (fact continuous_Pair)
subsubsection {* Separation axioms *}
--- 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 = (\<lambda>h. f (x + h)) -- 0 --> f x"
by (simp add: isCont_def LIM_isCont_iff)
-lemma isCont_norm [simp]:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
- unfolding isCont_def by (rule tendsto_norm)
-
-lemma isCont_rabs [simp]:
- fixes f :: "'a::topological_space \<Rightarrow> real"
- shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
- unfolding isCont_def by (rule tendsto_rabs)
-
-lemma isCont_add [simp]:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
- unfolding isCont_def by (rule tendsto_add)
-
-lemma isCont_minus [simp]:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
- unfolding isCont_def by (rule tendsto_minus)
-
-lemma isCont_diff [simp]:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
- unfolding isCont_def by (rule tendsto_diff)
-
-lemma isCont_mult [simp]:
- fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
- shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
- unfolding isCont_def by (rule tendsto_mult)
-
-lemma isCont_inverse [simp]:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
- shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
- unfolding isCont_def by (rule tendsto_inverse)
-
-lemma isCont_divide [simp]:
- fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
- shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>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 "(\<lambda>x. g (f x)) -- a --> l"
by (rule LIM_compose2 [OF f g inj])
+
+lemma isCont_norm [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
+ by (fact continuous_norm)
+
+lemma isCont_rabs [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> real"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
+ by (fact continuous_rabs)
+
+lemma isCont_add [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
+ by (fact continuous_add)
+
+lemma isCont_minus [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
+ by (fact continuous_minus)
+
+lemma isCont_diff [simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
+ by (fact continuous_diff)
+
+lemma isCont_mult [simp]:
+ fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
+ by (fact continuous_mult)
+
lemma (in bounded_linear) isCont:
"isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
- unfolding isCont_def by (rule tendsto)
+ by (fact continuous)
lemma (in bounded_bilinear) isCont:
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>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 \<Rightarrow> 'b::{power,real_normed_algebra}"
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
- unfolding isCont_def by (rule tendsto_power)
-
-lemma isCont_sgn [simp]:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
- unfolding isCont_def by (rule tendsto_sgn)
+ by (fact continuous_power)
lemma isCont_setsum [simp]:
- fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
- fixes A :: "'a set"
+ fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>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
--- 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 \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
unfolding norm_conv_dist by (intro tendsto_intros)
+lemma continuous_norm [continuous_intros]:
+ "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
+ unfolding continuous_def by (rule tendsto_norm)
+
+lemma continuous_on_norm [continuous_on_intros]:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_norm)
+
lemma tendsto_norm_zero:
"(f ---> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) F"
by (drule tendsto_norm, simp)
@@ -252,6 +260,14 @@
"(f ---> (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) F"
by (fold real_norm_def, rule tendsto_norm)
+lemma continuous_rabs [continuous_intros]:
+ "continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)"
+ unfolding real_norm_def[symmetric] by (rule continuous_norm)
+
+lemma continuous_on_rabs [continuous_on_intros]:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)"
+ unfolding real_norm_def[symmetric] by (rule continuous_on_norm)
+
lemma tendsto_rabs_zero:
"(f ---> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) F"
by (fold real_norm_def, rule tendsto_norm_zero)
@@ -271,8 +287,18 @@
shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
+ unfolding continuous_def by (rule tendsto_add)
+
+lemma continuous_on_add [continuous_on_intros]:
+ fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
+ unfolding continuous_on_def by (auto intro: tendsto_add)
+
lemma tendsto_add_zero:
- fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>(f ---> 0) F; (g ---> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) F"
by (drule (1) tendsto_add, simp)
@@ -281,6 +307,16 @@
shows "(f ---> a) F \<Longrightarrow> ((\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
+ unfolding continuous_def by (rule tendsto_minus)
+
+lemma continuous_on_minus [continuous_on_intros]:
+ fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
+ unfolding continuous_on_def by (auto intro: tendsto_minus)
+
lemma tendsto_minus_cancel:
fixes a :: "'a::real_normed_vector"
shows "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
@@ -296,6 +332,16 @@
shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
+ unfolding continuous_on_def by (auto intro: tendsto_diff)
+
lemma tendsto_setsum [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) F"
@@ -308,6 +354,16 @@
by (simp add: tendsto_const)
qed
+lemma continuous_setsum [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
+ shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
+ unfolding continuous_def by (rule tendsto_setsum)
+
+lemma continuous_on_setsum [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::real_normed_vector"
+ shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>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 \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
+lemma (in bounded_linear) continuous:
+ "continuous F g \<Longrightarrow> continuous F (\<lambda>x. f (g x))"
+ using tendsto[of g _ F] by (auto simp: continuous_def)
+
+lemma (in bounded_linear) continuous_on:
+ "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
+ using tendsto[of g] by (auto simp: continuous_on_def)
+
lemma (in bounded_linear) tendsto_zero:
"(g ---> 0) F \<Longrightarrow> ((\<lambda>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 \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>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 \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>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 \<Longrightarrow> ((\<lambda>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 \<Rightarrow> 'b::{power,real_normed_algebra}"
+ shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
+ unfolding continuous_def by (rule tendsto_power)
+
+lemma continuous_on_power [continuous_on_intros]:
+ fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
+ shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
+ unfolding continuous_on_def by (auto intro: tendsto_power)
+
lemma tendsto_setprod [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) F"
@@ -374,6 +474,16 @@
by (simp add: tendsto_const)
qed
+lemma continuous_setprod [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
+ shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)"
+ unfolding continuous_def by (rule tendsto_setprod)
+
+lemma continuous_on_setprod [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
+ shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>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 \<Rightarrow> 'b::real_normed_div_algebra"
+ assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
+ shows "continuous F (\<lambda>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 \<Rightarrow> 'b::real_normed_div_algebra"
+ assumes "continuous (at a within s) f" and "f a \<noteq> 0"
+ shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
+ using assms unfolding continuous_within by (rule tendsto_inverse)
+
+lemma isCont_inverse[continuous_intros, simp]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
+ assumes "isCont f a" and "f a \<noteq> 0"
+ shows "isCont (\<lambda>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 \<Rightarrow> 'b::real_normed_div_algebra"
+ assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
+ shows "continuous_on s (\<lambda>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 "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
\<Longrightarrow> ((\<lambda>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 \<Rightarrow> 'b::real_normed_field"
+ assumes "continuous F f" and "continuous F g" and "g (Lim F (\<lambda>x. x)) \<noteq> 0"
+ shows "continuous F (\<lambda>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 \<Rightarrow> 'b::real_normed_field"
+ assumes "continuous (at a within s) f" "continuous (at a within s) g" and "g a \<noteq> 0"
+ shows "continuous (at a within s) (\<lambda>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 \<Rightarrow> 'b::real_normed_field"
+ assumes "isCont f a" "isCont g a" "g a \<noteq> 0"
+ shows "isCont (\<lambda>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 \<Rightarrow> 'b::real_normed_field"
+ assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
+ shows "continuous_on s (\<lambda>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 "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
unfolding sgn_div_norm by (simp add: tendsto_intros)
+lemma continuous_sgn:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
+ shows "continuous F (\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
+ assumes "continuous (at a within s) f" and "f a \<noteq> 0"
+ shows "continuous (at a within s) (\<lambda>x. sgn (f x))"
+ using assms unfolding continuous_within by (rule tendsto_sgn)
+
+lemma isCont_sgn[continuous_intros]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "isCont f a" and "f a \<noteq> 0"
+ shows "isCont (\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
+ assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
+ shows "continuous_on s (\<lambda>x. sgn (f x))"
+ using assms unfolding continuous_on_def by (fast intro: tendsto_sgn)
+
lemma filterlim_at_infinity:
fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
assumes "0 \<le> c"
--- 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]:
+ "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>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 (\<lambda>x. x))" and "f (Lim F (\<lambda>x. x)) \<noteq> 1" and "0 < g (Lim F (\<lambda>x. x))"
+ shows "continuous F (\<lambda>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 \<noteq> 1" and "0 < g a"
+ shows "continuous (at a within s) (\<lambda>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 \<noteq> 1" "0 < g a"
+ shows "isCont (\<lambda>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 "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
+ shows "continuous_on s (\<lambda>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 @@
"\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>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 (\<lambda>x. x))"
+ shows "continuous F (\<lambda>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) (\<lambda>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 (\<lambda>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 "\<forall>x\<in>s. 0 < f x"
+ shows "continuous_on s (\<lambda>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 (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
--- 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 :: "_ \<Rightarrow> 'a :: metric_space"
+ shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))"
+ unfolding continuous_def by (rule tendsto_dist)
+
+lemma continuous_on_dist[continuous_on_intros]:
+ fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
+ shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
+ unfolding continuous_on_def by (auto intro: tendsto_dist)
+
lemma tendsto_at_topI_sequentially:
fixes f :: "real \<Rightarrow> real"
assumes mono: "mono f"
--- 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 \<ge> 0" "b \<ge> 0" shows "0 \<le> a / (b::real)"
apply(cases "b=0") defer apply(rule divide_nonneg_pos) using assms by auto
-lemma continuous_setsum:
- fixes f :: "'i \<Rightarrow> 'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- assumes f: "\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)" shows "continuous F (\<lambda>x. \<Sum>i\<in>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 \<Rightarrow> 'b::euclidean_space"
assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = 0))"
--- 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 \<Rightarrow> 'b::real_normed_vector"
assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "x \<in> {a..b}" (is "x\<in>?I")
@@ -783,15 +779,12 @@
shows "\<exists>x\<in>{a<..<b}. (f b - f a = (f' x) (b - a))"
proof-
have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
- apply(rule rolle[OF assms(1), of "\<lambda>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 "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
fix x assume x:"x \<in> {a<..<b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>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
--- 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) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> 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
--- 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 \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> 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 \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
+ using continuous_on_compose[of s f g] by (simp add: comp_def)
+
subsection {* Paths. *}
definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
@@ -111,106 +119,32 @@
assumes "pathfinish g1 = pathstart g2"
shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> 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 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)"
- "g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>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} \<subseteq> {0..1}"
- "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \<subseteq> {0..1}"
+proof safe
+ assume cont: "continuous_on {0..1} (g1 +++ g2)"
+ have g1: "continuous_on {0..1} g1 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2))"
+ by (intro continuous_on_cong refl) (auto simp: joinpaths_def)
+ have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>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} \<union> {1/2 .. 1::real}"
by auto
- then show "continuous_on {0..1} g1 \<and> 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 \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
- then have "x \<le> 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 \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}"
- then have "x \<ge> 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} \<union> {(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 ***: "(\<lambda>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 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>x. x * 2) ` {0..1 / 2}"
+ by (intro image_eqI[where x="x/2"]) auto }
+ note 1 = this
+ { fix x :: real assume "0 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>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 _ "\<lambda>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 \<circ> (\<lambda>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) \<subseteq> (path_image g1 \<union> path_image g2)"
-proof
- fix x
- assume "x \<in> path_image (g1 +++ g2)"
- then obtain y where y:"y\<in>{0..1}" "x = (if y \<le> 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 \<in> path_image g1 \<union> path_image g2"
- apply (cases "y \<le> 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 \<subseteq> s" "path_image g2 \<subseteq> 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) \<union> (path_image g2)"
apply (rule, rule path_image_join_subset, rule)
unfolding Un_iff
@@ -240,7 +174,7 @@
then show "x \<in> 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
--- 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 \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b"
- where "Lim A f = (THE l. (f ---> l) A)"
-
-text{* Uniqueness of the limit, when nontrivial. *}
-
-lemma tendsto_Lim:
- fixes f :: "'a \<Rightarrow> 'b::t2_space"
- shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
- unfolding Lim_def using tendsto_unique[of net f] by auto
-
lemma Lim:
"(f ---> l) net \<longleftrightarrow>
trivial_limit net \<or>
@@ -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 \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
- where "continuous net f \<longleftrightarrow> (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 \<longleftrightarrow> (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 \<longleftrightarrow> (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 \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
-where
- "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
-
-lemma continuous_on_topological:
- "continuous_on s f \<longleftrightarrow>
- (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
- (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> 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 \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> 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 \<Longrightarrow> (f ---> l) net"
-unfolding tendsto_def by (simp add: trivial_limit_eq)
-
-lemma continuous_at_imp_continuous_on:
- assumes "\<forall>x\<in>s. continuous (at x) f"
- shows "continuous_on s f"
-unfolding continuous_on_def
-proof
- fix x assume "x \<in> 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 \<longleftrightarrow> (\<forall>x \<in> 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) (\<lambda>x. x)"
- unfolding continuous_within by (rule tendsto_ident_at_within)
-
-lemma continuous_at_id[continuous_intros]: "continuous (at a) (\<lambda>x. x)"
- unfolding continuous_at by (rule tendsto_ident_at)
-
-lemma continuous_const[continuous_intros]: "continuous F (\<lambda>x. c)"
- unfolding continuous_def by (rule tendsto_const)
-
-lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
- unfolding continuous_def by (rule tendsto_fst)
-
-lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
- unfolding continuous_def by (rule tendsto_snd)
-
-lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>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 (\<lambda>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 (\<lambda>x. infdist (f x) A)"
using assms unfolding continuous_def by (rule tendsto_infdist)
-lemma continuous_norm[continuous_intros]:
- shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
- unfolding continuous_def by (rule tendsto_norm)
-
lemma continuous_infnorm[continuous_intros]:
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
unfolding continuous_def by (rule tendsto_infnorm)
-lemma continuous_add[continuous_intros]:
- fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
- unfolding continuous_def by (rule tendsto_add)
-
-lemma continuous_minus[continuous_intros]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
- unfolding continuous_def by (rule tendsto_minus)
-
-lemma continuous_diff[continuous_intros]:
- fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
- unfolding continuous_def by (rule tendsto_diff)
-
-lemma continuous_scaleR[continuous_intros]:
- fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>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 \<Rightarrow> 'b::real_normed_algebra"
- shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>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 (\<lambda>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 \<Rightarrow> 'b::real_normed_div_algebra"
- assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
- shows "continuous F (\<lambda>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 \<Rightarrow> 'b::real_normed_div_algebra"
- assumes "continuous (at a within s) f" and "f a \<noteq> 0"
- shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
- using assms unfolding continuous_within by (rule tendsto_inverse)
-
-lemma continuous_at_inverse[continuous_intros]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
- assumes "continuous (at a) f" and "f a \<noteq> 0"
- shows "continuous (at a) (\<lambda>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 (\<lambda>x. x)"
- unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
-
-lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
- unfolding continuous_on_def by (auto intro: tendsto_intros)
-
-lemma continuous_on_norm[continuous_on_intros]:
- shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>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 \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
unfolding continuous_on by (fast intro: tendsto_infnorm)
-lemma continuous_on_minus[continuous_on_intros]:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g
- \<Longrightarrow> continuous_on s (\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g
- \<Longrightarrow> continuous_on s (\<lambda>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 \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
- unfolding continuous_on_def by (fast intro: tendsto)
-
-lemma (in bounded_bilinear) continuous_on[continuous_on_intros]:
- "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>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 \<Rightarrow> 'b::real_normed_vector"
- assumes "continuous_on s f" and "continuous_on s g"
- shows "continuous_on s (\<lambda>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 \<Rightarrow> 'b::real_normed_algebra"
- assumes "continuous_on s f" and "continuous_on s g"
- shows "continuous_on s (\<lambda>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 \<Rightarrow> '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 \<Rightarrow> 'b::real_normed_div_algebra"
- assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
- shows "continuous_on s (\<lambda>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 \<longleftrightarrow>
- (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
- (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> 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 \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> 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 \<times> s)" using `compact s` by (intro compact_Times)
moreover have "s \<times> s \<noteq> {}" using `s \<noteq> {}` by auto
moreover have "continuous_on (s \<times> s) (\<lambda>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 \<times> s" "\<lambda>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 \<Rightarrow> real"
+ fixes f g :: "'a::t2_space \<Rightarrow> real"
assumes f: "\<And>x. isCont f x"
assumes g: "\<And>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 \<Rightarrow> real"
+ fixes f g :: "'a::t2_space \<Rightarrow> real"
assumes f: "\<And>x. isCont f x"
assumes g: "\<And>x. isCont g x"
shows "closed {x. f x \<le> g x}"
@@ -5901,7 +5645,7 @@
qed
lemma closed_Collect_eq:
- fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+ fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
assumes f: "\<And>x. isCont f x"
assumes g: "\<And>x. isCont g x"
shows "closed {x. f x = g x}"
--- 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 \<Longrightarrow> 0 < n \<Longrightarrow> ((\<lambda>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 \<Longrightarrow> 0 < n \<Longrightarrow> continuous F (\<lambda>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 \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>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 \<Longrightarrow> ((\<lambda>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 \<Longrightarrow> continuous F (\<lambda>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 \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
+ unfolding sqrt_def by (rule continuous_on_real_root [OF _ pos2])
+
lemma DERIV_real_sqrt_generic:
assumes "x \<noteq> 0"
assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
--- 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 \<Rightarrow> 'b :: metric_space"
- shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>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 \<Rightarrow> 'b::ordered_euclidean_space"
assumes f: "f \<in> borel_measurable M"
@@ -794,8 +789,7 @@
have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> 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 "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
@@ -808,8 +802,7 @@
unfolding log_def by auto
lemma borel_measurable_exp[measurable]: "exp \<in> 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"
--- 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 = "\<lambda>x. if x = a then f a else if x = b then f b else if x \<in> {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 \<in> borel_measurable borel"
using borel_measurable_continuous_on_open[of "{a <..< b }" f "\<lambda>x. x" borel 0]
by (auto intro!: measurable_If[where P="\<lambda>x. x = a"] measurable_If[where P="\<lambda>x. x = b"])
--- 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 \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
unfolding INF_def by (rule open_Inter) auto
+lemma openI:
+ assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
+ shows "open S"
+proof -
+ have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
+ moreover have "\<Union>{T. open T \<and> T \<subseteq> 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 \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
"(f ---> l) F \<equiv> filterlim f (nhds l) F"
+definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "Lim A f = (THE l. (f ---> l) A)"
+
lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
by simp
@@ -919,11 +931,10 @@
"((\<lambda>x. x) ---> a) (at a within S)"
unfolding tendsto_def eventually_within eventually_at_topological by auto
-lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
+lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
by (simp add: tendsto_def)
-lemma tendsto_unique:
- fixes f :: "'a \<Rightarrow> 'b::t2_space"
+lemma (in t2_space) tendsto_unique:
assumes "\<not> 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 "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
+lemma (in t2_space) tendsto_const_iff:
+ assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
lemma increasing_tendsto:
@@ -1003,6 +1013,18 @@
shows "a \<le> x"
using F x tendsto_const a by (rule tendsto_le)
+subsubsection {* Rules about @{const Lim} *}
+
+lemma (in t2_space) tendsto_Lim:
+ "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
+ unfolding Lim_def using tendsto_unique[of net f] by auto
+
+lemma Lim_ident_at: "\<not> trivial_limit (at x) \<Longrightarrow> Lim (at x) (\<lambda>x. x) = x"
+ by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+
+lemma Lim_ident_at_within: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>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 \<equiv> (X ---> L) sequentially"
-definition
- lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where
- --{*Standard definition of limit using choice operator*}
- "lim X = (THE L. X ----> L)"
+abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "lim X \<equiv> Lim sequentially X"
definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
"convergent X = (\<exists>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 \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
- "isCont f a \<longleftrightarrow> f -- a --> f a"
+subsubsection {* Continuity on a set *}
+
+definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
+ "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
+
+lemma continuous_on_topological:
+ "continuous_on s f \<longleftrightarrow>
+ (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
+ unfolding continuous_on_def tendsto_def eventually_within eventually_at_topological by metis
+
+lemma continuous_on_open_invariant:
+ "continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> (\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s))"
+proof safe
+ fix B :: "'b set" assume "continuous_on s f" "open B"
+ then have "\<forall>x\<in>f -` B \<inter> s. (\<exists>A. open A \<and> x \<in> A \<and> s \<inter> A \<subseteq> f -` B)"
+ by (auto simp: continuous_on_topological subset_eq Ball_def imp_conjL)
+ then guess A unfolding bchoice_iff ..
+ then show "\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s"
+ by (intro exI[of _ "\<Union>x\<in>f -` B \<inter> s. A x"]) auto
+next
+ assume B: "\<forall>B. open B \<longrightarrow> (\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s)"
+ show "continuous_on s f"
+ unfolding continuous_on_topological
+ proof safe
+ fix x B assume "x \<in> s" "open B" "f x \<in> B"
+ with B obtain A where A: "open A" "A \<inter> s = f -` B \<inter> s" by auto
+ with `x \<in> s` `f x \<in> B` show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
+ by (intro exI[of _ A]) auto
+ qed
+qed
+
+lemma continuous_on_closed_invariant:
+ "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
+proof -
+ have *: "\<And>P Q::'b set\<Rightarrow>bool. (\<And>A. P A \<longleftrightarrow> Q (- A)) \<Longrightarrow> (\<forall>A. P A) \<longleftrightarrow> (\<forall>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 (\<lambda>x. x)"
+ unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
+
+lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
+ unfolding continuous_on_def by (auto intro: tendsto_const)
+
+lemma continuous_on_compose[continuous_on_intros]:
+ "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
+ unfolding continuous_on_topological by simp metis
+
+subsubsection {* Continuity at a point *}
+
+definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
+ "continuous F f \<longleftrightarrow> (f ---> f (Lim F (\<lambda>x. x))) F"
+
+ML {*
-lemma isCont_ident [simp]: "isCont (\<lambda>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 \<Longrightarrow> continuous net f"
+ by simp
+
+lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (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 \<longleftrightarrow>
+ (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> 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 \<Longrightarrow> continuous (at (f x) within f ` s) g \<Longrightarrow>
+ 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 \<Longrightarrow> continuous (at (f x) within f ` s) g \<Longrightarrow>
+ continuous (at x within s) (\<lambda>x. g (f x))"
+ using continuous_within_compose[of x s f g] by (simp add: comp_def)
-lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
- unfolding isCont_def by (rule tendsto_const)
+lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f -- x --> f x"
+ using continuous_within[of x UNIV f] by simp
+
+lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
+ unfolding continuous_within by (rule tendsto_ident_at_within)
+
+lemma continuous_const[continuous_intros, simp]: "continuous F (\<lambda>x. c)"
+ unfolding continuous_def by (rule tendsto_const)
+
+lemma continuous_on_eq_continuous_within:
+ "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. continuous (at x within s) f)"
+ unfolding continuous_on_def continuous_within ..
+
+abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
+ "isCont f a \<equiv> continuous (at a) f"
+
+lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
+ by (rule continuous_at)
+
+lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
+ by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
+
+lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> 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 \<Longrightarrow> isCont f x"
+ by simp
+
+lemma isCont_ident[continuous_intros, simp]: "isCont (\<lambda>x. x) a"
+ using continuous_ident by (rule isContI_continuous)
+
+lemmas isCont_const = continuous_const
+
+lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
+ unfolding isCont_def by (rule tendsto_compose)
+
+lemma isCont_o[continuous_intros]: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a"
+ unfolding o_def by (rule isCont_o2)
lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
unfolding isCont_def by (rule tendsto_compose)
-lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
- unfolding isCont_def by (rule tendsto_compose)
-
-lemma isCont_o: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g o f) a"
- unfolding o_def by (rule isCont_o2)
+lemma continuous_within_compose3:
+ "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
+ using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
end
--- 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 \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
by (rule isCont_tendsto_compose [OF isCont_exp])
+lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
+ unfolding continuous_def by (rule tendsto_exp)
+
+lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>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 @@
"\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
by (rule isCont_tendsto_compose [OF isCont_ln])
+lemma continuous_ln:
+ "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
+ unfolding continuous_def by (rule tendsto_ln)
+
+lemma isCont_ln' [continuous_intros]:
+ "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
+ unfolding continuous_at by (rule tendsto_ln)
+
+lemma continuous_within_ln [continuous_intros]:
+ "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
+ unfolding continuous_within by (rule tendsto_ln)
+
+lemma continuous_on_ln [continuous_on_intros]:
+ "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_ln)
+
lemma DERIV_ln: "0 < x \<Longrightarrow> 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 \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
by (rule isCont_tendsto_compose [OF isCont_cos])
+lemma continuous_sin [continuous_intros]:
+ "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
+ unfolding continuous_def by (rule tendsto_sin)
+
+lemma continuous_on_sin [continuous_on_intros]:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_sin)
+
+lemma continuous_cos [continuous_intros]:
+ "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
+ unfolding continuous_def by (rule tendsto_cos)
+
+lemma continuous_on_cos [continuous_on_intros]:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>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 @@
"\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
by (rule isCont_tendsto_compose [OF isCont_tan])
+lemma continuous_tan:
+ "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
+ unfolding continuous_def by (rule tendsto_tan)
+
+lemma isCont_tan'' [continuous_intros]:
+ "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
+ unfolding continuous_at by (rule tendsto_tan)
+
+lemma continuous_within_tan [continuous_intros]:
+ "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
+ unfolding continuous_within by (rule tendsto_tan)
+
+lemma continuous_on_tan [continuous_on_intros]:
+ "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>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 \<longleftrightarrow> 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 \<Rightarrow> real" shows
"\<lbrakk>a < x; x < b;
\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
@@ -2414,7 +2468,7 @@
apply (simp_all add: abs_le_iff)
done
-lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x"
+lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x"
+lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
+ by (rule isCont_tendsto_compose [OF isCont_arctan])
+
+lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
+ unfolding continuous_def by (rule tendsto_arctan)
+
+lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_arctan)
+
lemma DERIV_arcsin:
"\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])