# HG changeset patch # User huffman # Date 1312911000 25200 # Node ID 230a8665c919951e05cd79939354ea1ad4d50562 # Parent 4c2a61a897d8ded471303d8d2fca84c8461ee7ca mark some redundant theorems as legacy diff -r 4c2a61a897d8 -r 230a8665c919 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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="\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" diff -r 4c2a61a897d8 -r 230a8665c919 src/HOL/Multivariate_Analysis/Derivative.thy --- 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: "((\x. x) has_derivative (\h. h)) net" apply(rule bounded_linear.has_derivative) using bounded_linear_ident[unfolded id_def] by simp lemma has_derivative_const: "((\x. c) has_derivative (\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 (\x. (c::real) *\<^sub>R f x)" proof - @@ -156,7 +157,8 @@ lemma has_derivative_cmul: assumes "(f has_derivative f') net" shows "((\x. c *\<^sub>R f(x)) has_derivative (\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 \ 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 *:"\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 "norm (f' (basis i) - f'' (basis i))" assume "f' (basis i) \ 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 / \c\) *\<^sub>R f' (c *\<^sub>R basis i)) + (1 / \c\) *\<^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)) \ e * norm (x - y)" apply- apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\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 "\e>0. \d>0. \y\s. norm (y - x) < d \ norm (g y - g x - g' x (y - x)) \ e * norm (y - x)" proof(rule,rule) case goal1 @@ -1613,7 +1616,7 @@ apply(rule has_derivative_sequence[OF assms(1) _ assms(3), of "\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\s`) by(auto intro!: Lim_const) + apply(rule `a\s`) by(auto intro!: tendsto_const) qed auto lemma has_antiderivative_limit: @@ -1682,16 +1685,16 @@ using assms by auto have "((\y. f' (y - x)) ---> 0) (at x within s)" unfolding f'.zero[THEN sym] - apply(rule Lim_linear[of "\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' "\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 "((\y. f x + f' (y - x)) ---> f x) (at x within s)" - using Lim_add[OF Lim_const, of "\y. f' (y - x)" 0 "at x within s" "f x"] + using tendsto_add[OF tendsto_const, of "\y. f' (y - x)" 0 "at x within s" "f x"] by auto ultimately have *:"((\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 diff -r 4c2a61a897d8 -r 230a8665c919 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- 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 (\x. a * X x \ S) net" by (rule eventually_mono[OF _ *]) auto qed -qed auto +qed (auto intro: tendsto_const) lemma ereal_lim_uminus: fixes X :: "'a \ ereal" shows "((\i. - X i) ---> -L) net \ (X ---> L) net" @@ -460,12 +460,12 @@ assumes inc: "incseq X" and lim: "X ----> L" shows "X N \ 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 \ ereal" @@ -519,7 +519,7 @@ lemma lim_ereal_increasing: assumes "\n m. n >= m \ f n >= f m" obtains l where "f ----> (l::ereal)" proof(cases "f = (\x. - \)") - case True then show thesis using Lim_const[of "- \" sequentially] by (intro that[of "-\"]) auto + case True then show thesis using tendsto_const[of "- \" sequentially] by (intro that[of "-\"]) auto next case False from this obtain N where N_def: "f N > (-\)" 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 diff -r 4c2a61a897d8 -r 230a8665c919 src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ UNIV}" shows "g integrable_on {a..b} \ ((\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} \ 0" have fg:"\x\{a..b}. \ k. (f k x) $$ 0 \ (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\s") using assms(3) by auto - next case goal3 thus ?case apply-apply(cases "x\s") using assms(4) by auto + next case goal3 thus ?case apply-apply(cases "x\s") + using assms(4) by (auto intro: tendsto_const) next case goal4 note * = integral_nonneg have "\k. norm (integral {a..b} (\x. if x \ s then f k x else 0)) \ 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 (\x. f 0 x))" in exI) apply safe apply(erule_tac x="integral s (\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 "(\x. - g x) integrable_on s \ ((\k. integral s (\x. - f k x)) ---> integral s (\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). *} diff -r 4c2a61a897d8 -r 230a8665c919 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 "((\x. h (f x)) ---> h l) net" -using `bounded_linear h` `(f ---> l) net` -by (rule bounded_linear.tendsto) - -lemma Lim_ident_at: "((\x. x) ---> a) (at a)" - unfolding tendsto_def Limits.eventually_at_topological by fast - -lemma Lim_const[intro]: "((\x. a) ---> a) net" by (rule tendsto_const) - -lemma Lim_cmul[intro]: - fixes f :: "'a \ 'b::real_normed_vector" - shows "(f ---> l) net ==> ((\x. c *\<^sub>R f x) ---> c *\<^sub>R l) net" - by (intro tendsto_intros) - -lemma Lim_neg: - fixes f :: "'a \ 'b::real_normed_vector" - shows "(f ---> l) net ==> ((\x. -(f x)) ---> -l) net" - by (rule tendsto_minus) - -lemma Lim_add: fixes f :: "'a \ 'b::real_normed_vector" shows - "(f ---> l) net \ (g ---> m) net \ ((\x. f(x) + g(x)) ---> l + m) net" - by (rule tendsto_add) - -lemma Lim_sub: - fixes f :: "'a \ 'b::real_normed_vector" - shows "(f ---> l) net \ (g ---> m) net \ ((\x. f(x) - g(x)) ---> l - m) net" - by (rule tendsto_diff) - -lemma Lim_mul: - fixes f :: "'a \ 'b::real_normed_vector" - assumes "(c ---> d) net" "(f ---> l) net" - shows "((\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 \ real" and A :: "'a filter" assumes "(f ---> l) A" and "l \ 0" shows "((inverse o f) ---> inverse l) A" unfolding o_def using assms by (rule tendsto_inverse) -lemma Lim_vmul: - fixes c :: "'a \ real" and v :: "'b::real_normed_vector" - shows "(c ---> d) net ==> ((\x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net" - by (intro tendsto_intros) - lemma Lim_null: fixes f :: "'a \ 'b::real_normed_vector" - shows "(f ---> l) net \ ((\x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm) - -lemma Lim_null_norm: - fixes f :: "'a \ 'b::real_normed_vector" - shows "(f ---> 0) net \ ((\x. norm(f x)) ---> 0) net" + shows "(f ---> l) net \ ((\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 \ ('a::euclidean_space)" shows "(f ---> l) net \ ((\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 \ '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 "((\x. f x - g x) ---> 0) net" "(f ---> l) net" shows "(g ---> l) net" proof- - from assms have "((\x. f x - g x - f x) ---> 0 - l) net" using Lim_sub[of "\x. f x - g x" 0 net f l] by auto - thus "?thesis" using Lim_neg [of "\ x. - g x" "-l" net] by auto + from assms have "((\x. f x - g x - f x) ---> 0 - l) net" using tendsto_diff[of "\x. f x - g x" 0 net f l] by auto + thus "?thesis" using tendsto_minus [of "\ x. - g x" "-l" net] by auto qed lemma Lim_transform_eventually: @@ -1592,7 +1538,7 @@ proof assume "?lhs" moreover { assume "l \ 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: "\n. f (r n) = l" by auto hence "subseq r \ ((f \ r) ---> l) sequentially" - unfolding o_def by (simp add: fr Lim_const) + unfolding o_def by (simp add: fr tendsto_const) hence "\r. subseq r \ ((f \ r) ---> l) sequentially" by - (rule exI) from f have "\n. f (r n) \ s" by simp @@ -3597,7 +3543,7 @@ \ ((\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 (\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 \ 'b::real_normed_vector" shows "continuous net f ==> continuous net (\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 \ 'b::real_normed_vector" shows "continuous net f ==> continuous net (\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 \ 'b::real_normed_vector" shows "continuous net f \ continuous net g \ continuous net (\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 \ 'b::real_normed_vector" shows "continuous net f \ continuous net g \ continuous net (\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 (\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 \ 'b::real_normed_vector" @@ -3692,11 +3638,11 @@ proof- { fix x y assume "((\n. f (x n) - f (y n)) ---> 0) sequentially" hence "((\n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially" - using Lim_cmul[of "(\n. f (x n) - f (y n))" 0 sequentially c] + using scaleR.tendsto [OF tendsto_const, of "(\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 "((\n. f (x n) - f (y n)) ---> 0) sequentially" "((\n. g (x n) - g (y n)) ---> 0) sequentially" hence "((\xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially" - using Lim_add[of "\ n. f (x n) - f (y n)" 0 sequentially "\ n. g (x n) - g (y n)" 0] by auto + using tendsto_add[of "\ n. f (x n) - f (y n)" 0 sequentially "\ n. g (x n) - g (y n)" 0] by auto hence "((\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) (\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) (\x. x)" - unfolding continuous_at by (rule Lim_ident_at) + unfolding continuous_at by (rule LIM_ident) lemma continuous_on_id: "continuous_on s (\x. x)" @@ -4103,7 +4049,7 @@ lemma continuous_vmul: fixes c :: "'a::metric_space \ real" and v :: "'b::real_normed_vector" shows "continuous net c ==> continuous net (\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 \ real" @@ -4434,7 +4380,7 @@ proof (rule continuous_attains_sup [OF assms]) { fix x assume "x\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'\s" and r:"subseq r" and lr:"(((\n. fst (f n)) \ r) ---> l') sequentially" using assms(1)[unfolded compact_def, THEN spec[where x="\ n. fst (f n)"]] using f(2) by auto have "((\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' \ t" using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\ n. snd (f (r n))"], THEN spec[where x="l - l'"]] using f(3) by auto @@ -5126,8 +5072,8 @@ hence "((\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 "\n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] - using Lim_vmul[of "\n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto } + using tendsto_add[OF tendsto_const, of "\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 "\n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto } ultimately have "x \ closure {a<.. 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