--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 09 08:53:12 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 09 10:30:00 2011 -0700
@@ -3054,7 +3054,7 @@
apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
apply(rule assms[unfolded convex_def, rule_format]) prefer 6
- apply(rule Lim_add) apply(rule_tac [1-2] Lim_cmul) by auto
+ by (auto intro: tendsto_intros)
lemma convex_interior:
fixes s :: "'a::real_normed_vector set"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 09 08:53:12 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 09 10:30:00 2011 -0700
@@ -137,13 +137,14 @@
lemma (in bounded_linear) has_derivative: "(f has_derivative f) net"
unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
- unfolding diff by(simp add: Lim_const)
+ unfolding diff by (simp add: tendsto_const)
lemma has_derivative_id: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
apply(rule bounded_linear.has_derivative) using bounded_linear_ident[unfolded id_def] by simp
lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
- unfolding has_derivative_def apply(rule,rule bounded_linear_zero) by(simp add: Lim_const)
+ unfolding has_derivative_def
+ by (rule, rule bounded_linear_zero, simp add: tendsto_const)
lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)"
proof -
@@ -156,7 +157,8 @@
lemma has_derivative_cmul: assumes "(f has_derivative f') net" shows "((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net"
unfolding has_derivative_def apply(rule,rule bounded_linear.cmul)
- using assms[unfolded has_derivative_def] using Lim_cmul[OF assms[unfolded has_derivative_def,THEN conjunct2]]
+ using assms[unfolded has_derivative_def]
+ using scaleR.tendsto[OF tendsto_const assms[unfolded has_derivative_def,THEN conjunct2]]
unfolding scaleR_right_diff_distrib scaleR_right_distrib by auto
lemma has_derivative_cmul_eq: assumes "c \<noteq> 0"
@@ -177,7 +179,7 @@
proof-
note as = assms[unfolded has_derivative_def]
show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
- using Lim_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
+ using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
by (auto simp add:algebra_simps scaleR_right_diff_distrib scaleR_right_distrib)
qed
@@ -224,7 +226,8 @@
apply (rule bounded_linear_compose [OF scaleR.bounded_linear_left])
apply (rule bounded_linear_compose [OF bounded_linear_euclidean_component])
apply (rule derivative_linear [OF assms])
- apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR apply(rule Lim_vmul)
+ apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR
+ apply (intro tendsto_intros)
using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
apply(rule,assumption,rule disjI2,rule,rule) proof-
have *:"\<And>x. x - 0 = (x::'a)" by auto
@@ -368,7 +371,7 @@
by(rule linear_continuous_within[OF f'[THEN conjunct1]])
show ?thesis unfolding continuous_within
using f'[THEN conjunct2, THEN Lim_mul_norm_within]
- apply- apply(drule Lim_add)
+ apply- apply(drule tendsto_add)
apply(rule **[unfolded continuous_within])
unfolding Lim_within and dist_norm
apply (rule, rule)
@@ -618,7 +621,7 @@
fix i assume i:"i<DIM('a)" def e \<equiv> "norm (f' (basis i) - f'' (basis i))"
assume "f' (basis i) \<noteq> f'' (basis i)"
hence "e>0" unfolding e_def by auto
- guess d using Lim_sub[OF as(1,2)[THEN conjunct2], unfolded * Lim_within,rule_format,OF `e>0`] .. note d=this
+ guess d using tendsto_diff [OF as(1,2)[THEN conjunct2], unfolded * Lim_within,rule_format,OF `e>0`] .. note d=this
guess c using assms(3)[rule_format,OF i d[THEN conjunct1]] .. note c=this
have *:"norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R basis i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R basis i)) = norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R basis i)) + f'' (c *\<^sub>R basis i)))"
unfolding scaleR_right_distrib by auto
@@ -1522,7 +1525,7 @@
thus "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
apply-
apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\<lambda>m. (f n x - f n y) - (f m x - f m y)"])
- apply(rule Lim_sub Lim_const g[rule_format] as)+ by assumption
+ apply(rule tendsto_intros g[rule_format] as)+ by assumption
qed
qed
show ?thesis unfolding has_derivative_within_alt apply(rule_tac x=g in exI)
@@ -1559,12 +1562,12 @@
apply(rule tendsto_unique[OF trivial_limit_sequentially])
apply(rule lem3[rule_format])
unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format]
- apply(rule Lim_cmul) by(rule lem3[rule_format])
+ apply (intro tendsto_intros) by(rule lem3[rule_format])
show "g' x (y + z) = g' x y + g' x z"
apply(rule tendsto_unique[OF trivial_limit_sequentially])
apply(rule lem3[rule_format])
unfolding lin[unfolded bounded_linear_def additive_def,THEN conjunct1,rule_format]
- apply(rule Lim_add) by(rule lem3[rule_format])+
+ apply(rule tendsto_add) by(rule lem3[rule_format])+
qed
show "\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
proof(rule,rule) case goal1
@@ -1613,7 +1616,7 @@
apply(rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
apply(rule,rule)
apply(rule has_derivative_add_const, rule assms(2)[rule_format], assumption)
- apply(rule `a\<in>s`) by(auto intro!: Lim_const)
+ apply(rule `a\<in>s`) by(auto intro!: tendsto_const)
qed auto
lemma has_antiderivative_limit:
@@ -1682,16 +1685,16 @@
using assms by auto
have "((\<lambda>y. f' (y - x)) ---> 0) (at x within s)"
unfolding f'.zero[THEN sym]
- apply(rule Lim_linear[of "\<lambda>y. y - x" 0 "at x within s" f'])
- using Lim_sub[OF Lim_within_id Lim_const, of x x s]
+ using bounded_linear.tendsto [of f' "\<lambda>y. y - x" 0 "at x within s"]
+ using tendsto_diff [OF Lim_within_id tendsto_const, of x x s]
unfolding id_def using assms(1) unfolding has_derivative_def by auto
hence "((\<lambda>y. f x + f' (y - x)) ---> f x) (at x within s)"
- using Lim_add[OF Lim_const, of "\<lambda>y. f' (y - x)" 0 "at x within s" "f x"]
+ using tendsto_add[OF tendsto_const, of "\<lambda>y. f' (y - x)" 0 "at x within s" "f x"]
by auto
ultimately
have *:"((\<lambda>x'. h (f x + f' (x' - x)) ((1/(norm (x' - x))) *\<^sub>R (g x' - (g x + g' (x' - x))))
+ h ((1/ (norm (x' - x))) *\<^sub>R (f x' - (f x + f' (x' - x)))) (g x')) ---> h (f x) 0 + h 0 (g x)) (at x within s)"
- apply-apply(rule Lim_add) apply(rule_tac[!] Lim_bilinear[OF _ _ assms(3)])
+ apply-apply(rule tendsto_add) apply(rule_tac[!] Lim_bilinear[OF _ _ assms(3)])
using assms(1-2) unfolding has_derivative_within by auto
guess B using bounded_bilinear.pos_bounded[OF assms(3)] .. note B=this
guess C using f'.pos_bounded .. note C=this
@@ -1725,7 +1728,7 @@
apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
apply (rule bounded_linear_compose [OF h.bounded_linear_left `bounded_linear f'`])
done
- thus ?thesis using Lim_add[OF * **] unfolding has_derivative_within
+ thus ?thesis using tendsto_add[OF * **] unfolding has_derivative_within
unfolding g'.add f'.scaleR f'.add g'.scaleR f'.diff g'.diff
h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
scaleR_right_diff_distrib h.zero_right h.zero_left
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Aug 09 08:53:12 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Aug 09 10:30:00 2011 -0700
@@ -248,7 +248,7 @@
show "eventually (\<lambda>x. a * X x \<in> S) net"
by (rule eventually_mono[OF _ *]) auto
qed
-qed auto
+qed (auto intro: tendsto_const)
lemma ereal_lim_uminus:
fixes X :: "'a \<Rightarrow> ereal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
@@ -460,12 +460,12 @@
assumes inc: "incseq X" and lim: "X ----> L"
shows "X N \<le> L"
using inc
- by (intro ereal_lim_mono[of N, OF _ Lim_const lim]) (simp add: incseq_def)
+ by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
lemma decseq_ge_ereal: assumes dec: "decseq X"
and lim: "X ----> (L::ereal)" shows "X N >= L"
using dec
- by (intro ereal_lim_mono[of N, OF _ lim Lim_const]) (simp add: decseq_def)
+ by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
lemma liminf_bounded_open:
fixes x :: "nat \<Rightarrow> ereal"
@@ -519,7 +519,7 @@
lemma lim_ereal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
obtains l where "f ----> (l::ereal)"
proof(cases "f = (\<lambda>x. - \<infinity>)")
- case True then show thesis using Lim_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
+ case True then show thesis using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
next
case False
from this obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
@@ -1138,7 +1138,7 @@
by (induct i) (insert assms, auto) }
note this[simp]
show ?thesis unfolding sums_def
- by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan)
+ by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan intro: tendsto_const)
qed
lemma suminf_finite:
@@ -1298,4 +1298,4 @@
apply (subst SUP_commute) ..
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 09 08:53:12 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 09 10:30:00 2011 -0700
@@ -4476,7 +4476,7 @@
"bounded {integral {a..b} (f k) | k . k \<in> UNIV}"
shows "g integrable_on {a..b} \<and> ((\<lambda>k. integral ({a..b}) (f k)) ---> integral ({a..b}) g) sequentially"
proof(case_tac[!] "content {a..b} = 0") assume as:"content {a..b} = 0"
- show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using Lim_const by auto
+ show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using tendsto_const by auto
next assume ab:"content {a..b} \<noteq> 0"
have fg:"\<forall>x\<in>{a..b}. \<forall> k. (f k x) $$ 0 \<le> (g x) $$ 0"
proof safe case goal1 note assms(3)[rule_format,OF this]
@@ -4631,7 +4631,8 @@
proof(rule monotone_convergence_interval,safe)
case goal1 show ?case using int .
next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto
- next case goal3 thus ?case apply-apply(cases "x\<in>s") using assms(4) by auto
+ next case goal3 thus ?case apply-apply(cases "x\<in>s")
+ using assms(4) by (auto intro: tendsto_const)
next case goal4 note * = integral_nonneg
have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
unfolding real_norm_def apply(subst abs_of_nonneg) apply(rule *[OF int])
@@ -4681,13 +4682,13 @@
proof- case goal1 thus ?case using *[of x 0 "Suc k"] by auto
next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
- next case goal4 thus ?case apply-apply(rule Lim_sub)
- using seq_offset[OF assms(3)[rule_format],of x 1] by auto
+ next case goal4 thus ?case apply-apply(rule tendsto_diff)
+ using seq_offset[OF assms(3)[rule_format],of x 1] by (auto intro: tendsto_const)
next case goal5 thus ?case using assms(4) unfolding bounded_iff
apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
apply(rule order_trans[OF norm_triangle_ineq4]) by auto qed
- note conjunctD2[OF this] note Lim_add[OF this(2) Lim_const[of "integral s (f 0)"]]
+ note conjunctD2[OF this] note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]]
integrable_add[OF this(1) assms(1)[rule_format,of 0]]
thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub)
using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed
@@ -4702,11 +4703,11 @@
apply(rule_tac x=k in exI) unfolding integral_neg[OF assm(1)] by auto
have "(\<lambda>x. - g x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. - f k x))
---> integral s (\<lambda>x. - g x)) sequentially" apply(rule monotone_convergence_increasing)
- apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule Lim_neg)
+ apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule tendsto_minus)
apply(rule assm,assumption) unfolding * apply(rule bounded_scaling) using assm by auto
note * = conjunctD2[OF this]
show ?thesis apply rule using integrable_neg[OF *(1)] defer
- using Lim_neg[OF *(2)] apply- unfolding integral_neg[OF assm(1)]
+ using tendsto_minus[OF *(2)] apply- unfolding integral_neg[OF assm(1)]
unfolding integral_neg[OF *(1),THEN sym] by auto qed
subsection {* absolute integrability (this is the same as Lebesgue integrability). *}
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 09 08:53:12 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 09 10:30:00 2011 -0700
@@ -1223,62 +1223,15 @@
thus ?lhs unfolding islimpt_approachable by auto
qed
-text{* Basic arithmetical combining theorems for limits. *}
-
-lemma Lim_linear:
- assumes "(f ---> l) net" "bounded_linear h"
- shows "((\<lambda>x. h (f x)) ---> h l) net"
-using `bounded_linear h` `(f ---> l) net`
-by (rule bounded_linear.tendsto)
-
-lemma Lim_ident_at: "((\<lambda>x. x) ---> a) (at a)"
- unfolding tendsto_def Limits.eventually_at_topological by fast
-
-lemma Lim_const[intro]: "((\<lambda>x. a) ---> a) net" by (rule tendsto_const)
-
-lemma Lim_cmul[intro]:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> l) net ==> ((\<lambda>x. c *\<^sub>R f x) ---> c *\<^sub>R l) net"
- by (intro tendsto_intros)
-
-lemma Lim_neg:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
- by (rule tendsto_minus)
-
-lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows
- "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) ---> l + m) net"
- by (rule tendsto_add)
-
-lemma Lim_sub:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
- by (rule tendsto_diff)
-
-lemma Lim_mul:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes "(c ---> d) net" "(f ---> l) net"
- shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
- using assms by (rule scaleR.tendsto)
-
-lemma Lim_inv:
+lemma Lim_inv: (* TODO: delete *)
fixes f :: "'a \<Rightarrow> real" and A :: "'a filter"
assumes "(f ---> l) A" and "l \<noteq> 0"
shows "((inverse o f) ---> inverse l) A"
unfolding o_def using assms by (rule tendsto_inverse)
-lemma Lim_vmul:
- fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
- by (intro tendsto_intros)
-
lemma Lim_null:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
-
-lemma Lim_null_norm:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. norm(f x)) ---> 0) net"
+ shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net"
by (simp add: Lim dist_norm)
lemma Lim_null_comparison:
@@ -1297,15 +1250,10 @@
using assms `e>0` unfolding tendsto_iff by auto
qed
-lemma Lim_component:
+lemma Lim_component: (* TODO: rename and declare [tendsto_intros] *)
fixes f :: "'a \<Rightarrow> ('a::euclidean_space)"
shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $$i) ---> l$$i) net"
- unfolding tendsto_iff
- apply (clarify)
- apply (drule spec, drule (1) mp)
- apply (erule eventually_elim1)
- apply (erule le_less_trans [OF dist_nth_le])
- done
+ unfolding euclidean_component_def by (intro tendsto_intros)
lemma Lim_transform_bound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -1422,8 +1370,6 @@
unfolding tendsto_def Limits.eventually_within eventually_at_topological
by auto
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
lemma Lim_at_id: "(id ---> a) (at a)"
apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
@@ -1478,10 +1424,10 @@
unfolding netlimit_def
apply (rule some_equality)
apply (rule Lim_at_within)
-apply (rule Lim_ident_at)
+apply (rule LIM_ident)
apply (erule tendsto_unique [OF assms])
apply (rule Lim_at_within)
-apply (rule Lim_ident_at)
+apply (rule LIM_ident)
done
lemma netlimit_at:
@@ -1498,8 +1444,8 @@
assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
shows "(g ---> l) net"
proof-
- from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using Lim_sub[of "\<lambda>x. f x - g x" 0 net f l] by auto
- thus "?thesis" using Lim_neg [of "\<lambda> x. - g x" "-l" net] by auto
+ from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using tendsto_diff[of "\<lambda>x. f x - g x" 0 net f l] by auto
+ thus "?thesis" using tendsto_minus [of "\<lambda> x. - g x" "-l" net] by auto
qed
lemma Lim_transform_eventually:
@@ -1592,7 +1538,7 @@
proof
assume "?lhs" moreover
{ assume "l \<in> S"
- hence "?rhs" using Lim_const[of l sequentially] by auto
+ hence "?rhs" using tendsto_const[of l sequentially] by auto
} moreover
{ assume "l islimpt S"
hence "?rhs" unfolding islimpt_sequential by auto
@@ -2809,7 +2755,7 @@
by (rule infinite_enumerate)
then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = l" by auto
hence "subseq r \<and> ((f \<circ> r) ---> l) sequentially"
- unfolding o_def by (simp add: fr Lim_const)
+ unfolding o_def by (simp add: fr tendsto_const)
hence "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
by - (rule exI)
from f have "\<forall>n. f (r n) \<in> s" by simp
@@ -3597,7 +3543,7 @@
\<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
(* BH: maybe the previous lemma should replace this one? *)
unfolding uniformly_continuous_on_sequentially'
-unfolding dist_norm Lim_null_norm [symmetric] ..
+unfolding dist_norm tendsto_norm_zero_iff ..
text{* The usual transformation theorems. *}
@@ -3628,34 +3574,34 @@
text{* Combination results for pointwise continuity. *}
lemma continuous_const: "continuous net (\<lambda>x. c)"
- by (auto simp add: continuous_def Lim_const)
+ by (auto simp add: continuous_def tendsto_const)
lemma continuous_cmul:
fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
- by (auto simp add: continuous_def Lim_cmul)
+ by (auto simp add: continuous_def intro: tendsto_intros)
lemma continuous_neg:
fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
- by (auto simp add: continuous_def Lim_neg)
+ by (auto simp add: continuous_def tendsto_minus)
lemma continuous_add:
fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
- by (auto simp add: continuous_def Lim_add)
+ by (auto simp add: continuous_def tendsto_add)
lemma continuous_sub:
fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
- by (auto simp add: continuous_def Lim_sub)
+ by (auto simp add: continuous_def tendsto_diff)
text{* Same thing for setwise continuity. *}
lemma continuous_on_const:
"continuous_on s (\<lambda>x. c)"
- unfolding continuous_on_def by auto
+ unfolding continuous_on_def by (auto intro: tendsto_intros)
lemma continuous_on_cmul:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
@@ -3692,11 +3638,11 @@
proof-
{ fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
- using Lim_cmul[of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
+ using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
}
thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
- unfolding dist_norm Lim_null_norm [symmetric] by auto
+ unfolding dist_norm tendsto_norm_zero_iff by auto
qed
lemma dist_minus:
@@ -3718,10 +3664,10 @@
{ fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
"((\<lambda>n. g (x n) - g (y n)) ---> 0) sequentially"
hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
- using Lim_add[of "\<lambda> n. f (x n) - f (y n)" 0 sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
+ using tendsto_add[of "\<lambda> n. f (x n) - f (y n)" 0 sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto }
thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
- unfolding dist_norm Lim_null_norm [symmetric] by auto
+ unfolding dist_norm tendsto_norm_zero_iff by auto
qed
lemma uniformly_continuous_on_sub:
@@ -3736,11 +3682,11 @@
lemma continuous_within_id:
"continuous (at a within s) (\<lambda>x. x)"
- unfolding continuous_within by (rule Lim_at_within [OF Lim_ident_at])
+ unfolding continuous_within by (rule Lim_at_within [OF LIM_ident])
lemma continuous_at_id:
"continuous (at a) (\<lambda>x. x)"
- unfolding continuous_at by (rule Lim_ident_at)
+ unfolding continuous_at by (rule LIM_ident)
lemma continuous_on_id:
"continuous_on s (\<lambda>x. x)"
@@ -4103,7 +4049,7 @@
lemma continuous_vmul:
fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
- unfolding continuous_def using Lim_vmul[of c] by auto
+ unfolding continuous_def by (intro tendsto_intros)
lemma continuous_mul:
fixes c :: "'a::metric_space \<Rightarrow> real"
@@ -4434,7 +4380,7 @@
proof (rule continuous_attains_sup [OF assms])
{ fix x assume "x\<in>s"
have "(dist a ---> dist a x) (at x within s)"
- by (intro tendsto_dist tendsto_const Lim_at_within Lim_ident_at)
+ by (intro tendsto_dist tendsto_const Lim_at_within LIM_ident)
}
thus "continuous_on s (dist a)"
unfolding continuous_on ..
@@ -4681,7 +4627,7 @@
obtain l' r where "l'\<in>s" and r:"subseq r" and lr:"(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially"
using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially"
- using Lim_sub[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
+ using tendsto_diff[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
hence "l - l' \<in> t"
using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
using f(3) by auto
@@ -5126,8 +5072,8 @@
hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
unfolding Lim_sequentially by(auto simp add: dist_norm)
hence "(f ---> x) sequentially" unfolding f_def
- using Lim_add[OF Lim_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
- using Lim_vmul[of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto }
+ using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
+ using scaleR.tendsto [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto }
ultimately have "x \<in> closure {a<..<b}"
using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto }
thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
@@ -6157,4 +6103,18 @@
(** TODO move this someplace else within this theory **)
instance euclidean_space \<subseteq> banach ..
+text {* Legacy theorem names *}
+
+lemmas Lim_ident_at = LIM_ident
+lemmas Lim_const = tendsto_const
+lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
+lemmas Lim_neg = tendsto_minus
+lemmas Lim_add = tendsto_add
+lemmas Lim_sub = tendsto_diff
+lemmas Lim_mul = scaleR.tendsto
+lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
+lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
+lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
+lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
+
end