# HG changeset patch # User wenzelm # Date 1451470914 -3600 # Node ID 0c7e865fa7cb5280060753572dc1f19661c5537c # Parent a70b89a3e02ec0fd82549339ec18cd8ff061136d more symbols; diff -r a70b89a3e02e -r 0c7e865fa7cb NEWS --- a/NEWS Tue Dec 29 23:50:44 2015 +0100 +++ b/NEWS Wed Dec 30 11:21:54 2015 +0100 @@ -502,6 +502,7 @@ notation Preorder.equiv ("op ~~") and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) + notation (in topological_space) tendsto (infixr "--->" 55) notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Complex.thy --- a/src/HOL/Complex.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Complex.thy Wed Dec 30 11:21:54 2015 +0100 @@ -382,14 +382,14 @@ lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im] lemma tendsto_Complex [tendsto_intros]: - "(f ---> a) F \ (g ---> b) F \ ((\x. Complex (f x) (g x)) ---> Complex a b) F" + "(f \ a) F \ (g \ b) F \ ((\x. Complex (f x) (g x)) \ Complex a b) F" by (auto intro!: tendsto_intros) lemma tendsto_complex_iff: - "(f ---> x) F \ (((\x. Re (f x)) ---> Re x) F \ ((\x. Im (f x)) ---> Im x) F)" + "(f \ x) F \ (((\x. Re (f x)) \ Re x) F \ ((\x. Im (f x)) \ Im x) F)" proof safe - assume "((\x. Re (f x)) ---> Re x) F" "((\x. Im (f x)) ---> Im x) F" - from tendsto_Complex[OF this] show "(f ---> x) F" + assume "((\x. Re (f x)) \ Re x) F" "((\x. Im (f x)) \ Im x) F" + from tendsto_Complex[OF this] show "(f \ x) F" unfolding complex.collapse . qed (auto intro: tendsto_intros) @@ -530,7 +530,7 @@ lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj] lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj] -lemma lim_cnj: "((\x. cnj(f x)) ---> cnj l) F \ (f ---> l) F" +lemma lim_cnj: "((\x. cnj(f x)) \ cnj l) F \ (f \ l) F" by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff) lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Deriv.thy Wed Dec 30 11:21:54 2015 +0100 @@ -20,7 +20,7 @@ where "(f has_derivative f') F \ (bounded_linear f' \ - ((\y. ((f y - f (Lim F (\x. x))) - f' (y - Lim F (\x. x))) /\<^sub>R norm (y - Lim F (\x. x))) ---> 0) F)" + ((\y. ((f y - f (Lim F (\x. x))) - f' (y - Lim F (\x. x))) /\<^sub>R norm (y - Lim F (\x. x))) \ 0) F)" text \ Usually the filter @{term F} is @{term "at x within s"}. @{term "(f has_derivative D) @@ -115,9 +115,9 @@ proof safe let ?x = "Lim F (\x. x)" let ?D = "\f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)" - have "((\x. ?D f f' x + ?D g g' x) ---> (0 + 0)) F" + have "((\x. ?D f f' x + ?D g g' x) \ (0 + 0)) F" using f g by (intro tendsto_add) (auto simp: has_derivative_def) - then show "(?D (\x. f x + g x) (\x. f' x + g' x) ---> 0) F" + then show "(?D (\x. f x + g x) (\x. f' x + g' x) \ 0) F" by (simp add: field_simps scaleR_add_right scaleR_diff_right) qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear) @@ -138,12 +138,12 @@ lemma has_derivative_at_within: "(f has_derivative f') (at x within s) \ - (bounded_linear f' \ ((\y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s))" + (bounded_linear f' \ ((\y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \ 0) (at x within s))" by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at) lemma has_derivative_iff_norm: "(f has_derivative f') (at x within s) \ - (bounded_linear f' \ ((\y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) ---> 0) (at x within s))" + (bounded_linear f' \ ((\y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) \ 0) (at x within s))" using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric] by (simp add: has_derivative_at_within divide_inverse ac_simps) @@ -164,20 +164,20 @@ done lemma has_derivativeI: - "bounded_linear f' \ ((\y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s) \ + "bounded_linear f' \ ((\y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \ 0) (at x within s) \ (f has_derivative f') (at x within s)" by (simp add: has_derivative_at_within) lemma has_derivativeI_sandwich: assumes e: "0 < e" and bounded: "bounded_linear f'" and sandwich: "(\y. y \ s \ y \ x \ dist y x < e \ norm ((f y - f x) - f' (y - x)) / norm (y - x) \ H y)" - and "(H ---> 0) (at x within s)" + and "(H \ 0) (at x within s)" shows "(f has_derivative f') (at x within s)" unfolding has_derivative_iff_norm proof safe - show "((\y. norm (f y - f x - f' (y - x)) / norm (y - x)) ---> 0) (at x within s)" + show "((\y. norm (f y - f x - f' (y - x)) / norm (y - x)) \ 0) (at x within s)" proof (rule tendsto_sandwich[where f="\x. 0"]) - show "(H ---> 0) (at x within s)" by fact + show "(H \ 0) (at x within s)" by fact show "eventually (\n. norm (f n - f x - f' (n - x)) / norm (n - x) \ H n) (at x within s)" unfolding eventually_at using e sandwich by auto qed (auto simp: le_divide_eq) @@ -197,7 +197,7 @@ proof - from f interpret F: bounded_linear f' by (rule has_derivative_bounded_linear) note F.tendsto[tendsto_intros] - let ?L = "\f. (f ---> 0) (at x within s)" + let ?L = "\f. (f \ 0) (at x within s)" have "?L (\y. norm ((f y - f x) - f' (y - x)) / norm (y - x))" using f unfolding has_derivative_iff_norm by blast then have "?L (\y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m) @@ -216,7 +216,7 @@ subsection \Composition\ -lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \ (f ---> y) (at x within s) \ (f ---> y) (inf (nhds x) (principal s))" +lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \ (f \ y) (at x within s) \ (f \ y) (inf (nhds x) (principal s))" unfolding tendsto_def eventually_inf_principal eventually_at_filter by (intro ext all_cong imp_cong) (auto elim!: eventually_mono) @@ -231,7 +231,7 @@ from G.bounded obtain kG where kG: "\x. norm (g' x) \ norm x * kG" by fast note G.tendsto[tendsto_intros] - let ?L = "\f. (f ---> 0) (at x within s)" + let ?L = "\f. (f \ 0) (at x within s)" let ?D = "\f f' x y. (f y - f x) - f' (y - x)" let ?N = "\f f' x y. norm (?D f f' x y) / norm (y - x)" let ?gf = "\x. g (f x)" and ?gf' = "\x. g' (f' x)" @@ -263,20 +263,20 @@ next have [tendsto_intros]: "?L Nf" using f unfolding has_derivative_iff_norm Nf_def .. - from f have "(f ---> f x) (at x within s)" + from f have "(f \ f x) (at x within s)" by (blast intro: has_derivative_continuous continuous_within[THEN iffD1]) then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))" unfolding filterlim_def by (simp add: eventually_filtermap eventually_at_filter le_principal) - have "((?N g g' (f x)) ---> 0) (at (f x) within f`s)" + have "((?N g g' (f x)) \ 0) (at (f x) within f`s)" using g unfolding has_derivative_iff_norm .. - then have g': "((?N g g' (f x)) ---> 0) (inf (nhds (f x)) (principal (f`s)))" + then have g': "((?N g g' (f x)) \ 0) (inf (nhds (f x)) (principal (f`s)))" by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp have [tendsto_intros]: "?L Ng" unfolding Ng_def by (rule filterlim_compose[OF g' f']) - show "((\y. Nf y * kG + Ng y * (Nf y + kF)) ---> 0) (at x within s)" + show "((\y. Nf y * kG + Ng y * (Nf y + kF)) \ 0) (at x within s)" by (intro tendsto_eq_intros) auto qed simp qed @@ -310,13 +310,13 @@ bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left] has_derivative_bounded_linear [OF g] has_derivative_bounded_linear [OF f]) next - from g have "(g ---> g x) ?F" + from g have "(g \ g x) ?F" by (intro continuous_within[THEN iffD1] has_derivative_continuous) - moreover from f g have "(Nf ---> 0) ?F" "(Ng ---> 0) ?F" + moreover from f g have "(Nf \ 0) ?F" "(Ng \ 0) ?F" by (simp_all add: has_derivative_iff_norm Ng_def Nf_def) - ultimately have "(?fun2 ---> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F" + ultimately have "(?fun2 \ norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F" by (intro tendsto_intros) (simp_all add: LIM_zero_iff) - then show "(?fun2 ---> 0) ?F" + then show "(?fun2 \ 0) ?F" by simp next fix y::'d assume "y \ x" @@ -377,7 +377,7 @@ next show "0 < norm x" using x by simp next - show "((\y. norm (?inv y - ?inv x) * norm (?inv x)) ---> 0) (at x within s)" + show "((\y. norm (?inv y - ?inv x) * norm (?inv x)) \ 0) (at x within s)" apply (rule tendsto_mult_left_zero) apply (rule tendsto_norm_zero) apply (rule LIM_zero) @@ -1438,7 +1438,7 @@ lemma DERIV_pos_imp_increasing_at_bot: fixes f :: "real => real" assumes "\x. x \ b \ (EX y. DERIV f x :> y & y > 0)" - and lim: "(f ---> flim) at_bot" + and lim: "(f \ flim) at_bot" shows "flim < f b" proof - have "flim \ f (b - 1)" @@ -1455,7 +1455,7 @@ lemma DERIV_neg_imp_decreasing_at_top: fixes f :: "real => real" assumes der: "\x. x \ b \ (EX y. DERIV f x :> y & y < 0)" - and lim: "(f ---> flim) at_top" + and lim: "(f \ flim) at_top" shows "flim < f b" apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\i. f (-i)" and b = "-b", simplified]) apply (metis DERIV_mirror der le_minus_iff neg_0_less_iff_less) @@ -1592,7 +1592,7 @@ lemma isCont_If_ge: fixes a :: "'a :: linorder_topology" - shows "continuous (at_left a) g \ (f ---> g a) (at_right a) \ isCont (\x. if x \ a then g x else f x) a" + shows "continuous (at_left a) g \ (f \ g a) (at_right a) \ isCont (\x. if x \ a then g x else f x) a" unfolding isCont_def continuous_within apply (intro filterlim_split_at) apply (subst filterlim_cong[OF refl refl, where g=g]) @@ -1603,15 +1603,15 @@ lemma lhopital_right_0: fixes f0 g0 :: "real \ real" - assumes f_0: "(f0 ---> 0) (at_right 0)" - assumes g_0: "(g0 ---> 0) (at_right 0)" + assumes f_0: "(f0 \ 0) (at_right 0)" + assumes g_0: "(g0 \ 0) (at_right 0)" assumes ev: "eventually (\x. g0 x \ 0) (at_right 0)" "eventually (\x. g' x \ 0) (at_right 0)" "eventually (\x. DERIV f0 x :> f' x) (at_right 0)" "eventually (\x. DERIV g0 x :> g' x) (at_right 0)" - assumes lim: "((\ x. (f' x / g' x)) ---> x) (at_right 0)" - shows "((\ x. f0 x / g0 x) ---> x) (at_right 0)" + assumes lim: "((\ x. (f' x / g' x)) \ x) (at_right 0)" + shows "((\ x. f0 x / g0 x) \ x) (at_right 0)" proof - def f \ "\x. if x \ 0 then 0 else f0 x" then have "f 0 = 0" by simp @@ -1674,15 +1674,15 @@ moreover from \ have "eventually (\x. norm (\ x) \ x) (at_right 0)" by eventually_elim auto - then have "((\x. norm (\ x)) ---> 0) (at_right 0)" + then have "((\x. norm (\ x)) \ 0) (at_right 0)" by (rule_tac real_tendsto_sandwich[where f="\x. 0" and h="\x. x"]) auto - then have "(\ ---> 0) (at_right 0)" + then have "(\ \ 0) (at_right 0)" by (rule tendsto_norm_zero_cancel) with \ have "filterlim \ (at_right 0) (at_right 0)" by (auto elim!: eventually_mono simp: filterlim_at) - from this lim have "((\t. f' (\ t) / g' (\ t)) ---> x) (at_right 0)" + from this lim have "((\t. f' (\ t) / g' (\ t)) \ x) (at_right 0)" by (rule_tac filterlim_compose[of _ _ _ \]) - ultimately have "((\t. f t / g t) ---> x) (at_right 0)" (is ?P) + ultimately have "((\t. f t / g t) \ x) (at_right 0)" (is ?P) by (rule_tac filterlim_cong[THEN iffD1, OF refl refl]) (auto elim: eventually_mono) also have "?P \ ?thesis" @@ -1691,35 +1691,35 @@ qed lemma lhopital_right: - "((f::real \ real) ---> 0) (at_right x) \ (g ---> 0) (at_right x) \ + "((f::real \ real) \ 0) (at_right x) \ (g \ 0) (at_right x) \ eventually (\x. g x \ 0) (at_right x) \ eventually (\x. g' x \ 0) (at_right x) \ eventually (\x. DERIV f x :> f' x) (at_right x) \ eventually (\x. DERIV g x :> g' x) (at_right x) \ - ((\ x. (f' x / g' x)) ---> y) (at_right x) \ - ((\ x. f x / g x) ---> y) (at_right x)" + ((\ x. (f' x / g' x)) \ y) (at_right x) \ + ((\ x. f x / g x) \ y) (at_right x)" unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift by (rule lhopital_right_0) lemma lhopital_left: - "((f::real \ real) ---> 0) (at_left x) \ (g ---> 0) (at_left x) \ + "((f::real \ real) \ 0) (at_left x) \ (g \ 0) (at_left x) \ eventually (\x. g x \ 0) (at_left x) \ eventually (\x. g' x \ 0) (at_left x) \ eventually (\x. DERIV f x :> f' x) (at_left x) \ eventually (\x. DERIV g x :> g' x) (at_left x) \ - ((\ x. (f' x / g' x)) ---> y) (at_left x) \ - ((\ x. f x / g x) ---> y) (at_left x)" + ((\ x. (f' x / g' x)) \ y) (at_left x) \ + ((\ x. f x / g x) \ y) (at_left x)" unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror by (rule lhopital_right[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) lemma lhopital: - "((f::real \ real) ---> 0) (at x) \ (g ---> 0) (at x) \ + "((f::real \ real) \ 0) (at x) \ (g \ 0) (at x) \ eventually (\x. g x \ 0) (at x) \ eventually (\x. g' x \ 0) (at x) \ eventually (\x. DERIV f x :> f' x) (at x) \ eventually (\x. DERIV g x :> g' x) (at x) \ - ((\ x. (f' x / g' x)) ---> y) (at x) \ - ((\ x. f x / g x) ---> y) (at x)" + ((\ x. (f' x / g' x)) \ y) (at x) \ + ((\ x. f x / g x) \ y) (at x)" unfolding eventually_at_split filterlim_at_split by (auto intro!: lhopital_right[of f x g g' f'] lhopital_left[of f x g g' f']) @@ -1730,8 +1730,8 @@ "eventually (\x. g' x \ 0) (at_right 0)" "eventually (\x. DERIV f x :> f' x) (at_right 0)" "eventually (\x. DERIV g x :> g' x) (at_right 0)" - assumes lim: "((\ x. (f' x / g' x)) ---> x) (at_right 0)" - shows "((\ x. f x / g x) ---> x) (at_right 0)" + assumes lim: "((\ x. (f' x / g' x)) \ x) (at_right 0)" + shows "((\ x. f x / g x) \ x) (at_right 0)" unfolding tendsto_iff proof safe fix e :: real assume "0 < e" @@ -1756,21 +1756,21 @@ using g_0 by (auto elim: eventually_mono simp: filterlim_at_top_dense) moreover - have inv_g: "((\x. inverse (g x)) ---> 0) (at_right 0)" + have inv_g: "((\x. inverse (g x)) \ 0) (at_right 0)" using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl] by (rule filterlim_compose) - then have "((\x. norm (1 - g a * inverse (g x))) ---> norm (1 - g a * 0)) (at_right 0)" + then have "((\x. norm (1 - g a * inverse (g x))) \ norm (1 - g a * 0)) (at_right 0)" by (intro tendsto_intros) - then have "((\x. norm (1 - g a / g x)) ---> 1) (at_right 0)" + then have "((\x. norm (1 - g a / g x)) \ 1) (at_right 0)" by (simp add: inverse_eq_divide) from this[unfolded tendsto_iff, rule_format, of 1] have "eventually (\x. norm (1 - g a / g x) < 2) (at_right 0)" by (auto elim!: eventually_mono simp: dist_real_def) moreover - from inv_g have "((\t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)" + from inv_g have "((\t. norm ((f a - x * g a) * inverse (g t))) \ norm ((f a - x * g a) * 0)) (at_right 0)" by (intro tendsto_intros) - then have "((\t. norm (f a - x * g a) / norm (g t)) ---> 0) (at_right 0)" + then have "((\t. norm (f a - x * g a) / norm (g t)) \ 0) (at_right 0)" by (simp add: inverse_eq_divide) from this[unfolded tendsto_iff, rule_format, of "e / 2"] \0 < e\ have "eventually (\t. norm (f a - x * g a) / norm (g t) < e / 2) (at_right 0)" @@ -1808,8 +1808,8 @@ eventually (\x. g' x \ 0) (at_right x) \ eventually (\x. DERIV f x :> f' x) (at_right x) \ eventually (\x. DERIV g x :> g' x) (at_right x) \ - ((\ x. (f' x / g' x)) ---> y) (at_right x) \ - ((\ x. f x / g x) ---> y) (at_right x)" + ((\ x. (f' x / g' x)) \ y) (at_right x) \ + ((\ x. f x / g x) \ y) (at_right x)" unfolding eventually_at_right_to_0[of _ x] filterlim_at_right_to_0[of _ _ x] DERIV_shift by (rule lhopital_right_0_at_top) @@ -1818,8 +1818,8 @@ eventually (\x. g' x \ 0) (at_left x) \ eventually (\x. DERIV f x :> f' x) (at_left x) \ eventually (\x. DERIV g x :> g' x) (at_left x) \ - ((\ x. (f' x / g' x)) ---> y) (at_left x) \ - ((\ x. f x / g x) ---> y) (at_left x)" + ((\ x. (f' x / g' x)) \ y) (at_left x) \ + ((\ x. f x / g x) \ y) (at_left x)" unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror by (rule lhopital_right_at_top[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) @@ -1828,8 +1828,8 @@ eventually (\x. g' x \ 0) (at x) \ eventually (\x. DERIV f x :> f' x) (at x) \ eventually (\x. DERIV g x :> g' x) (at x) \ - ((\ x. (f' x / g' x)) ---> y) (at x) \ - ((\ x. f x / g x) ---> y) (at x)" + ((\ x. (f' x / g' x)) \ y) (at x) \ + ((\ x. f x / g x) \ y) (at x)" unfolding eventually_at_split filterlim_at_split by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f']) @@ -1839,8 +1839,8 @@ assumes g': "eventually (\x. g' x \ 0) at_top" assumes Df: "eventually (\x. DERIV f x :> f' x) at_top" assumes Dg: "eventually (\x. DERIV g x :> g' x) at_top" - assumes lim: "((\ x. (f' x / g' x)) ---> x) at_top" - shows "((\ x. f x / g x) ---> x) at_top" + assumes lim: "((\ x. (f' x / g' x)) \ x) at_top" + shows "((\ x. f x / g x) \ x) at_top" unfolding filterlim_at_top_to_right proof (rule lhopital_right_0_at_top) let ?F = "\x. f (inverse x)" @@ -1874,7 +1874,7 @@ using g' eventually_ge_at_top[where c="1::real"] by eventually_elim auto - show "((\x. ?D f' x / ?D g' x) ---> x) ?R" + show "((\x. ?D f' x / ?D g' x) \ x) ?R" unfolding filterlim_at_right_to_top apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim]) using eventually_ge_at_top[where c="1::real"] diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Library/Extended_Real.thy Wed Dec 30 11:21:54 2015 +0100 @@ -1749,11 +1749,11 @@ assumes f: "continuous_on s f" shows "continuous_on s (\x. ereal (f x))" by (rule continuous_on_compose2 [OF continuous_onI_mono[of ereal UNIV] f]) auto -lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \ ((\x. ereal (f x)) ---> ereal x) F" +lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f \ x) F \ ((\x. ereal (f x)) \ ereal x) F" using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\x. x"] by (simp add: continuous_on_eq_continuous_at) -lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \ ((\x. - f x::ereal) ---> - x) F" +lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f \ x) F \ ((\x. - f x::ereal) \ - x) F" apply (rule tendsto_compose[where g=uminus]) apply (auto intro!: order_tendstoI simp: eventually_at_topological) apply (rule_tac x="{..< -a}" in exI) @@ -1770,7 +1770,7 @@ apply (metis PInfty_neq_ereal(2) ereal_less_eq(3) ereal_top le_cases order_trans) done -lemma ereal_Lim_uminus: "(f ---> f0) net \ ((\x. - f x::ereal) ---> - f0) net" +lemma ereal_Lim_uminus: "(f \ f0) net \ ((\x. - f x::ereal) \ - f0) net" using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\x. - f x" "- f0" net] by auto @@ -1781,10 +1781,10 @@ by (cases a b c rule: ereal3_cases) (auto simp: field_simps) lemma tendsto_cmult_ereal[tendsto_intros, simp, intro]: - assumes c: "\c\ \ \" and f: "(f ---> x) F" shows "((\x. c * f x::ereal) ---> c * x) F" + assumes c: "\c\ \ \" and f: "(f \ x) F" shows "((\x. c * f x::ereal) \ c * x) F" proof - { fix c :: ereal assume "0 < c" "c < \" - then have "((\x. c * f x::ereal) ---> c * x) F" + then have "((\x. c * f x::ereal) \ c * x) F" apply (intro tendsto_compose[OF _ f]) apply (auto intro!: order_tendstoI simp: eventually_at_topological) apply (rule_tac x="{a/c <..}" in exI) @@ -1801,7 +1801,7 @@ assume "- \ < c" "c < 0" then have "0 < - c" "- c < \" by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0]) - then have "((\x. (- c) * f x) ---> (- c) * x) F" + then have "((\x. (- c) * f x) \ (- c) * x) F" by (rule *) from tendsto_uminus_ereal[OF this] show ?thesis by simp @@ -1809,7 +1809,7 @@ qed lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]: - assumes "x \ 0" and f: "(f ---> x) F" shows "((\x. c * f x::ereal) ---> c * x) F" + assumes "x \ 0" and f: "(f \ x) F" shows "((\x. c * f x::ereal) \ c * x) F" proof cases assume "\c\ = \" show ?thesis @@ -1828,7 +1828,7 @@ qed (rule tendsto_cmult_ereal[OF _ f]) lemma tendsto_cadd_ereal[tendsto_intros, simp, intro]: - assumes c: "y \ - \" "x \ - \" and f: "(f ---> x) F" shows "((\x. f x + y::ereal) ---> x + y) F" + assumes c: "y \ - \" "x \ - \" and f: "(f \ x) F" shows "((\x. f x + y::ereal) \ x + y) F" apply (intro tendsto_compose[OF _ f]) apply (auto intro!: order_tendstoI simp: eventually_at_topological) apply (rule_tac x="{a - y <..}" in exI) @@ -1838,7 +1838,7 @@ done lemma tendsto_add_left_ereal[tendsto_intros, simp, intro]: - assumes c: "\y\ \ \" and f: "(f ---> x) F" shows "((\x. f x + y::ereal) ---> x + y) F" + assumes c: "\y\ \ \" and f: "(f \ x) F" shows "((\x. f x + y::ereal) \ x + y) F" apply (intro tendsto_compose[OF _ f]) apply (auto intro!: order_tendstoI simp: eventually_at_topological) apply (rule_tac x="{a - y <..}" in exI) @@ -2337,10 +2337,10 @@ lemma eventually_finite: fixes x :: ereal - assumes "\x\ \ \" "(f ---> x) F" + assumes "\x\ \ \" "(f \ x) F" shows "eventually (\x. \f x\ \ \) F" proof - - have "(f ---> ereal (real_of_ereal x)) F" + have "(f \ ereal (real_of_ereal x)) F" using assms by (cases x) auto then have "eventually (\x. f x \ ereal ` UNIV) F" by (rule topological_tendstoD) (auto intro: open_ereal) @@ -2436,8 +2436,8 @@ subsubsection \Convergent sequences\ lemma lim_real_of_ereal[simp]: - assumes lim: "(f ---> ereal x) net" - shows "((\x. real_of_ereal (f x)) ---> x) net" + assumes lim: "(f \ ereal x) net" + shows "((\x. real_of_ereal (f x)) \ x) net" proof (intro topological_tendstoI) fix S assume "open S" and "x \ S" @@ -2447,7 +2447,7 @@ by (auto intro: eventually_mono [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]]) qed -lemma lim_ereal[simp]: "((\n. ereal (f n)) ---> ereal x) net \ (f ---> x) net" +lemma lim_ereal[simp]: "((\n. ereal (f n)) \ ereal x) net \ (f \ x) net" by (auto dest!: lim_real_of_ereal) lemma convergent_real_imp_convergent_ereal: @@ -2460,7 +2460,7 @@ thus "lim (\n. ereal (a n)) = ereal (lim a)" using lim L limI by metis qed -lemma tendsto_PInfty: "(f ---> \) F \ (\r. eventually (\x. ereal r < f x) F)" +lemma tendsto_PInfty: "(f \ \) F \ (\r. eventually (\x. ereal r < f x) F)" proof - { fix l :: ereal @@ -2473,10 +2473,10 @@ qed lemma tendsto_PInfty_eq_at_top: - "((\z. ereal (f z)) ---> \) F \ (LIM z F. f z :> at_top)" + "((\z. ereal (f z)) \ \) F \ (LIM z F. f z :> at_top)" unfolding tendsto_PInfty filterlim_at_top_dense by simp -lemma tendsto_MInfty: "(f ---> -\) F \ (\r. eventually (\x. f x < ereal r) F)" +lemma tendsto_MInfty: "(f \ -\) F \ (\r. eventually (\x. f x < ereal r) F)" unfolding tendsto_def proof safe fix S :: "ereal set" @@ -2558,8 +2558,8 @@ lemma tendsto_ereal_realD: fixes f :: "'a \ ereal" assumes "x \ 0" - and tendsto: "((\x. ereal (real_of_ereal (f x))) ---> x) net" - shows "(f ---> x) net" + and tendsto: "((\x. ereal (real_of_ereal (f x))) \ x) net" + shows "(f \ x) net" proof (intro topological_tendstoI) fix S assume S: "open S" "x \ S" @@ -2572,8 +2572,8 @@ lemma tendsto_ereal_realI: fixes f :: "'a \ ereal" - assumes x: "\x\ \ \" and tendsto: "(f ---> x) net" - shows "((\x. ereal (real_of_ereal (f x))) ---> x) net" + assumes x: "\x\ \ \" and tendsto: "(f \ x) net" + shows "((\x. ereal (real_of_ereal (f x))) \ x) net" proof (intro topological_tendstoI) fix S assume "open S" and "x \ S" @@ -2592,15 +2592,15 @@ lemma tendsto_add_ereal: fixes x y :: ereal assumes x: "\x\ \ \" and y: "\y\ \ \" - assumes f: "(f ---> x) F" and g: "(g ---> y) F" - shows "((\x. f x + g x) ---> x + y) F" + assumes f: "(f \ x) F" and g: "(g \ y) F" + shows "((\x. f x + g x) \ x + y) F" proof - from x obtain r where x': "x = ereal r" by (cases x) auto - with f have "((\i. real_of_ereal (f i)) ---> r) F" by simp + with f have "((\i. real_of_ereal (f i)) \ r) F" by simp moreover from y obtain p where y': "y = ereal p" by (cases y) auto - with g have "((\i. real_of_ereal (g i)) ---> p) F" by simp - ultimately have "((\i. real_of_ereal (f i) + real_of_ereal (g i)) ---> r + p) F" + with g have "((\i. real_of_ereal (g i)) \ p) F" by simp + ultimately have "((\i. real_of_ereal (f i) + real_of_ereal (g i)) \ r + p) F" by (rule tendsto_add) moreover from eventually_finite[OF x f] eventually_finite[OF y g] @@ -3408,7 +3408,7 @@ lemma Liminf_PInfty: fixes f :: "'a \ ereal" assumes "\ trivial_limit net" - shows "(f ---> \) net \ Liminf net f = \" + shows "(f \ \) net \ Liminf net f = \" unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto @@ -3416,7 +3416,7 @@ lemma Limsup_MInfty: fixes f :: "'a \ ereal" assumes "\ trivial_limit net" - shows "(f ---> -\) net \ Limsup net f = -\" + shows "(f \ -\) net \ Limsup net f = -\" unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto @@ -3582,23 +3582,23 @@ by (auto simp add: ereal_all_split ereal_ex_split) lemma ereal_tendsto_simps1: - "((f \ real_of_ereal) ---> y) (at_left (ereal x)) \ (f ---> y) (at_left x)" - "((f \ real_of_ereal) ---> y) (at_right (ereal x)) \ (f ---> y) (at_right x)" - "((f \ real_of_ereal) ---> y) (at_left (\::ereal)) \ (f ---> y) at_top" - "((f \ real_of_ereal) ---> y) (at_right (-\::ereal)) \ (f ---> y) at_bot" + "((f \ real_of_ereal) \ y) (at_left (ereal x)) \ (f \ y) (at_left x)" + "((f \ real_of_ereal) \ y) (at_right (ereal x)) \ (f \ y) (at_right x)" + "((f \ real_of_ereal) \ y) (at_left (\::ereal)) \ (f \ y) at_top" + "((f \ real_of_ereal) \ y) (at_right (-\::ereal)) \ (f \ y) at_bot" unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf by (auto simp: filtermap_filtermap filtermap_ident) lemma ereal_tendsto_simps2: - "((ereal \ f) ---> ereal a) F \ (f ---> a) F" - "((ereal \ f) ---> \) F \ (LIM x F. f x :> at_top)" - "((ereal \ f) ---> -\) F \ (LIM x F. f x :> at_bot)" + "((ereal \ f) \ ereal a) F \ (f \ a) F" + "((ereal \ f) \ \) F \ (LIM x F. f x :> at_top)" + "((ereal \ f) \ -\) F \ (LIM x F. f x :> at_bot)" unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense using lim_ereal by (simp_all add: comp_def) lemma inverse_infty_ereal_tendsto_0: "inverse -- \ --> (0::ereal)" proof - - have **: "((\x. ereal (inverse x)) ---> ereal 0) at_infinity" + have **: "((\x. ereal (inverse x)) \ ereal 0) at_infinity" by (intro tendsto_intros tendsto_inverse_0) show ?thesis @@ -3619,7 +3619,7 @@ intro!: Lim_transform_eventually[OF _ **] t1_space_nhds) qed (insert \0 < x\, auto intro!: inverse_infty_ereal_tendsto_0) -lemma inverse_ereal_tendsto_at_right_0: "(inverse ---> \) (at_right (0::ereal))" +lemma inverse_ereal_tendsto_at_right_0: "(inverse \ \) (at_right (0::ereal))" unfolding tendsto_compose_filtermap[symmetric] at_right_ereal zero_ereal_def by (subst filterlim_cong[OF refl refl, where g="\x. ereal (inverse x)"]) (auto simp: eventually_at_filter tendsto_PInfty_eq_at_top filterlim_inverse_at_top_right) diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Library/Liminf_Limsup.thy Wed Dec 30 11:21:54 2015 +0100 @@ -192,7 +192,7 @@ lemma lim_imp_Liminf: fixes f :: "'a \ _ :: {complete_linorder,linorder_topology}" assumes ntriv: "\ trivial_limit F" - assumes lim: "(f ---> f0) F" + assumes lim: "(f \ f0) F" shows "Liminf F f = f0" proof (intro Liminf_eqI) fix P assume P: "eventually P F" @@ -231,7 +231,7 @@ lemma lim_imp_Limsup: fixes f :: "'a \ _ :: {complete_linorder,linorder_topology}" assumes ntriv: "\ trivial_limit F" - assumes lim: "(f ---> f0) F" + assumes lim: "(f \ f0) F" shows "Limsup F f = f0" proof (intro Limsup_eqI) fix P assume P: "eventually P F" @@ -271,7 +271,7 @@ fixes f0 :: "'a :: {complete_linorder,linorder_topology}" assumes ntriv: "\ trivial_limit F" and lim: "Liminf F f = f0" "Limsup F f = f0" - shows "(f ---> f0) F" + shows "(f \ f0) F" proof (rule order_tendstoI) fix a assume "f0 < a" with assms have "Limsup F f < a" by simp @@ -290,7 +290,7 @@ lemma tendsto_iff_Liminf_eq_Limsup: fixes f0 :: "'a :: {complete_linorder,linorder_topology}" - shows "\ trivial_limit F \ (f ---> f0) F \ (Liminf F f = f0 \ Limsup F f = f0)" + shows "\ trivial_limit F \ (f \ f0) F \ (Liminf F f = f0 \ Limsup F f = f0)" by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf) lemma liminf_subseq_mono: diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Library/Product_Vector.thy Wed Dec 30 11:21:54 2015 +0100 @@ -152,8 +152,8 @@ subsubsection \Continuity of operations\ lemma tendsto_fst [tendsto_intros]: - assumes "(f ---> a) F" - shows "((\x. fst (f x)) ---> fst a) F" + assumes "(f \ a) F" + shows "((\x. fst (f x)) \ fst a) F" proof (rule topological_tendstoI) fix S assume "open S" and "fst a \ S" then have "open (fst -` S)" and "a \ fst -` S" @@ -165,8 +165,8 @@ qed lemma tendsto_snd [tendsto_intros]: - assumes "(f ---> a) F" - shows "((\x. snd (f x)) ---> snd a) F" + assumes "(f \ a) F" + shows "((\x. snd (f x)) \ snd a) F" proof (rule topological_tendstoI) fix S assume "open S" and "snd a \ S" then have "open (snd -` S)" and "a \ snd -` S" @@ -178,18 +178,18 @@ qed lemma tendsto_Pair [tendsto_intros]: - assumes "(f ---> a) F" and "(g ---> b) F" - shows "((\x. (f x, g x)) ---> (a, b)) F" + assumes "(f \ a) F" and "(g \ b) F" + shows "((\x. (f x, g x)) \ (a, b)) F" proof (rule topological_tendstoI) fix S assume "open S" and "(a, b) \ S" then obtain A B where "open A" "open B" "a \ A" "b \ B" "A \ B \ S" unfolding open_prod_def by fast have "eventually (\x. f x \ A) F" - using \(f ---> a) F\ \open A\ \a \ A\ + using \(f \ a) F\ \open A\ \a \ A\ by (rule topological_tendstoD) moreover have "eventually (\x. g x \ B) F" - using \(g ---> b) F\ \open B\ \b \ B\ + using \(g \ b) F\ \open B\ \b \ B\ by (rule topological_tendstoD) ultimately show "eventually (\x. (f x, g x) \ S) F" @@ -491,7 +491,7 @@ let ?Rg = "\y. g y - g x - g' (y - x)" let ?R = "\y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))" - show "((\y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)" + show "((\y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) \ 0) (at x within s)" using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm) fix y :: 'a assume "y \ x" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Limits.thy Wed Dec 30 11:21:54 2015 +0100 @@ -43,7 +43,7 @@ by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl]) lemma lim_infinity_imp_sequentially: - "(f ---> l) at_infinity \ ((\n. f(n)) ---> l) sequentially" + "(f \ l) at_infinity \ ((\n. f(n)) \ l) sequentially" by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially) @@ -485,19 +485,19 @@ lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] -lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\x. f x - a) F" +lemma tendsto_Zfun_iff: "(f \ a) F = Zfun (\x. f x - a) F" by (simp only: tendsto_iff Zfun_def dist_norm) -lemma tendsto_0_le: "\(f ---> 0) F; eventually (\x. norm (g x) \ norm (f x) * K) F\ - \ (g ---> 0) F" +lemma tendsto_0_le: "\(f \ 0) F; eventually (\x. norm (g x) \ norm (f x) * K) F\ + \ (g \ 0) F" by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) subsubsection \Distance and norms\ lemma tendsto_dist [tendsto_intros]: fixes l m :: "'a :: metric_space" - assumes f: "(f ---> l) F" and g: "(g ---> m) F" - shows "((\x. dist (f x) (g x)) ---> dist l m) F" + assumes f: "(f \ l) F" and g: "(g \ m) F" + shows "((\x. dist (f x) (g x)) \ dist l m) F" proof (rule tendstoI) fix e :: real assume "0 < e" hence e2: "0 < e/2" by simp @@ -526,7 +526,7 @@ unfolding continuous_on_def by (auto intro: tendsto_dist) lemma tendsto_norm [tendsto_intros]: - "(f ---> a) F \ ((\x. norm (f x)) ---> norm a) F" + "(f \ a) F \ ((\x. norm (f x)) \ norm a) F" unfolding norm_conv_dist by (intro tendsto_intros) lemma continuous_norm [continuous_intros]: @@ -538,19 +538,19 @@ unfolding continuous_on_def by (auto intro: tendsto_norm) lemma tendsto_norm_zero: - "(f ---> 0) F \ ((\x. norm (f x)) ---> 0) F" + "(f \ 0) F \ ((\x. norm (f x)) \ 0) F" by (drule tendsto_norm, simp) lemma tendsto_norm_zero_cancel: - "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" + "((\x. norm (f x)) \ 0) F \ (f \ 0) F" unfolding tendsto_iff dist_norm by simp lemma tendsto_norm_zero_iff: - "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" + "((\x. norm (f x)) \ 0) F \ (f \ 0) F" unfolding tendsto_iff dist_norm by simp lemma tendsto_rabs [tendsto_intros]: - "(f ---> (l::real)) F \ ((\x. \f x\) ---> \l\) F" + "(f \ (l::real)) F \ ((\x. \f x\) \ \l\) F" by (fold real_norm_def, rule tendsto_norm) lemma continuous_rabs [continuous_intros]: @@ -562,22 +562,22 @@ unfolding real_norm_def[symmetric] by (rule continuous_on_norm) lemma tendsto_rabs_zero: - "(f ---> (0::real)) F \ ((\x. \f x\) ---> 0) F" + "(f \ (0::real)) F \ ((\x. \f x\) \ 0) F" by (fold real_norm_def, rule tendsto_norm_zero) lemma tendsto_rabs_zero_cancel: - "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" + "((\x. \f x\) \ (0::real)) F \ (f \ 0) F" by (fold real_norm_def, rule tendsto_norm_zero_cancel) lemma tendsto_rabs_zero_iff: - "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" + "((\x. \f x\) \ (0::real)) F \ (f \ 0) F" by (fold real_norm_def, rule tendsto_norm_zero_iff) subsubsection \Addition and subtraction\ lemma tendsto_add [tendsto_intros]: fixes a b :: "'a::real_normed_vector" - shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x + g x) ---> a + b) F" + shows "\(f \ a) F; (g \ b) F\ \ ((\x. f x + g x) \ a + b) F" by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) lemma continuous_add [continuous_intros]: @@ -592,12 +592,12 @@ lemma tendsto_add_zero: fixes f g :: "_ \ 'b::real_normed_vector" - shows "\(f ---> 0) F; (g ---> 0) F\ \ ((\x. f x + g x) ---> 0) F" + shows "\(f \ 0) F; (g \ 0) F\ \ ((\x. f x + g x) \ 0) F" by (drule (1) tendsto_add, simp) lemma tendsto_minus [tendsto_intros]: fixes a :: "'a::real_normed_vector" - shows "(f ---> a) F \ ((\x. - f x) ---> - a) F" + shows "(f \ a) F \ ((\x. - f x) \ - a) F" by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) lemma continuous_minus [continuous_intros]: @@ -612,17 +612,17 @@ lemma tendsto_minus_cancel: fixes a :: "'a::real_normed_vector" - shows "((\x. - f x) ---> - a) F \ (f ---> a) F" + shows "((\x. - f x) \ - a) F \ (f \ a) F" by (drule tendsto_minus, simp) lemma tendsto_minus_cancel_left: - "(f ---> - (y::_::real_normed_vector)) F \ ((\x. - f x) ---> y) F" + "(f \ - (y::_::real_normed_vector)) F \ ((\x. - f x) \ y) F" using tendsto_minus_cancel[of f "- y" F] tendsto_minus[of f "- y" F] by auto lemma tendsto_diff [tendsto_intros]: fixes a b :: "'a::real_normed_vector" - shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x - g x) ---> a - b) F" + shows "\(f \ a) F; (g \ b) F\ \ ((\x. f x - g x) \ a - b) F" using tendsto_add [of f a F "\x. - g x" "- b"] by (simp add: tendsto_minus) lemma continuous_diff [continuous_intros]: @@ -640,8 +640,8 @@ lemma tendsto_setsum [tendsto_intros]: fixes f :: "'a \ 'b \ 'c::real_normed_vector" - assumes "\i. i \ S \ (f i ---> a i) F" - shows "((\x. \i\S. f i x) ---> (\i\S. a i)) F" + assumes "\i. i \ S \ (f i \ a i) F" + shows "((\x. \i\S. f i x) \ (\i\S. a i)) F" proof (cases "finite S") assume "finite S" thus ?thesis using assms by (induct, simp, simp add: tendsto_add) @@ -666,7 +666,7 @@ by (auto simp: linearI distrib_left) lemma (in bounded_linear) tendsto: - "(g ---> a) F \ ((\x. f (g x)) ---> f a) F" + "(g \ a) F \ ((\x. f (g x)) \ f a) F" by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) lemma (in bounded_linear) continuous: @@ -678,11 +678,11 @@ using tendsto[of g] by (auto simp: continuous_on_def) lemma (in bounded_linear) tendsto_zero: - "(g ---> 0) F \ ((\x. f (g x)) ---> 0) F" + "(g \ 0) F \ ((\x. f (g x)) \ 0) F" by (drule tendsto, simp only: zero) lemma (in bounded_bilinear) tendsto: - "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x ** g x) ---> a ** b) F" + "\(f \ a) F; (g \ b) F\ \ ((\x. f x ** g x) \ a ** b) F" by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) @@ -695,17 +695,17 @@ 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" - shows "((\x. f x ** g x) ---> 0) F" + assumes f: "(f \ 0) F" + assumes g: "(g \ 0) F" + shows "((\x. f x ** g x) \ 0) F" using tendsto [OF f g] by (simp add: zero_left) lemma (in bounded_bilinear) tendsto_left_zero: - "(f ---> 0) F \ ((\x. f x ** c) ---> 0) F" + "(f \ 0) F \ ((\x. f x ** c) \ 0) F" by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) lemma (in bounded_bilinear) tendsto_right_zero: - "(f ---> 0) F \ ((\x. c ** f x) ---> 0) F" + "(f \ 0) F \ ((\x. c ** f x) \ 0) F" by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) lemmas tendsto_of_real [tendsto_intros] = @@ -719,12 +719,12 @@ lemma tendsto_mult_left: fixes c::"'a::real_normed_algebra" - shows "(f ---> l) F \ ((\x. c * (f x)) ---> c * l) F" + shows "(f \ l) F \ ((\x. c * (f x)) \ c * l) F" by (rule tendsto_mult [OF tendsto_const]) lemma tendsto_mult_right: fixes c::"'a::real_normed_algebra" - shows "(f ---> l) F \ ((\x. (f x) * c) ---> l * c) F" + shows "(f \ l) F \ ((\x. (f x) * c) \ l * c) F" by (rule tendsto_mult [OF _ tendsto_const]) lemmas continuous_of_real [continuous_intros] = @@ -756,7 +756,7 @@ lemma tendsto_power [tendsto_intros]: fixes f :: "'a \ 'b::{power,real_normed_algebra}" - shows "(f ---> a) F \ ((\x. f x ^ n) ---> a ^ n) F" + shows "(f \ a) F \ ((\x. f x ^ n) \ a ^ n) F" by (induct n) (simp_all add: tendsto_mult) lemma continuous_power [continuous_intros]: @@ -771,8 +771,8 @@ lemma tendsto_setprod [tendsto_intros]: fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}" - assumes "\i. i \ S \ (f i ---> L i) F" - shows "((\x. \i\S. f i x) ---> (\i\S. L i)) F" + assumes "\i. i \ S \ (f i \ L i) F" + shows "((\x. \i\S. f i x) \ (\i\S. L i)) F" proof (cases "finite S") assume "finite S" thus ?thesis using assms by (induct, simp, simp add: tendsto_mult) @@ -789,11 +789,11 @@ unfolding continuous_on_def by (auto intro: tendsto_setprod) lemma tendsto_of_real_iff: - "((\x. of_real (f x) :: 'a :: real_normed_div_algebra) ---> of_real c) F \ (f ---> c) F" + "((\x. of_real (f x) :: 'a :: real_normed_div_algebra) \ of_real c) F \ (f \ c) F" unfolding tendsto_iff by simp lemma tendsto_add_const_iff: - "((\x. c + f x :: 'a :: real_normed_vector) ---> c + d) F \ (f ---> d) F" + "((\x. c + f x :: 'a :: real_normed_vector) \ c + d) F \ (f \ d) F" using tendsto_add[OF tendsto_const[of c], of f d] tendsto_add[OF tendsto_const[of "-c"], of "\x. c + f x" "c + d"] by auto @@ -842,7 +842,7 @@ lemma Bfun_inverse: fixes a :: "'a::real_normed_div_algebra" - assumes f: "(f ---> a) F" + assumes f: "(f \ a) F" assumes a: "a \ 0" shows "Bfun (\x. inverse (f x)) F" proof - @@ -877,9 +877,9 @@ lemma tendsto_inverse [tendsto_intros]: fixes a :: "'a::real_normed_div_algebra" - assumes f: "(f ---> a) F" + assumes f: "(f \ a) F" assumes a: "a \ 0" - shows "((\x. inverse (f x)) ---> inverse a) F" + shows "((\x. inverse (f x)) \ inverse a) F" proof - from a have "0 < norm a" by simp with f have "eventually (\x. dist (f x) a < norm a) F" @@ -923,8 +923,8 @@ lemma tendsto_divide [tendsto_intros]: fixes a b :: "'a::real_normed_field" - shows "\(f ---> a) F; (g ---> b) F; b \ 0\ - \ ((\x. f x / g x) ---> a / b) F" + shows "\(f \ a) F; (g \ b) F; b \ 0\ + \ ((\x. f x / g x) \ a / b) F" by (simp add: tendsto_mult tendsto_inverse divide_inverse) lemma continuous_divide: @@ -953,7 +953,7 @@ lemma tendsto_sgn [tendsto_intros]: fixes l :: "'a::real_normed_vector" - shows "\(f ---> l) F; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) F" + shows "\(f \ l) F; l \ 0\ \ ((\x. sgn (f x)) \ sgn l) F" unfolding sgn_div_norm by (simp add: tendsto_intros) lemma continuous_sgn: @@ -1001,7 +1001,7 @@ lemma not_tendsto_and_filterlim_at_infinity: assumes "F \ bot" - assumes "(f ---> (c :: 'a :: real_normed_vector)) F" + assumes "(f \ (c :: 'a :: real_normed_vector)) F" assumes "filterlim f at_infinity F" shows False proof - @@ -1142,7 +1142,7 @@ lemma tendsto_inverse_0: fixes x :: "_ \ 'a::real_normed_div_algebra" - shows "(inverse ---> (0::'a)) at_infinity" + shows "(inverse \ (0::'a)) at_infinity" unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity proof safe fix r :: real assume "0 < r" @@ -1157,12 +1157,12 @@ qed lemma tendsto_add_filterlim_at_infinity: - assumes "(f ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)" + assumes "(f \ (c :: 'b :: real_normed_vector)) (F :: 'a filter)" assumes "filterlim g at_infinity F" shows "filterlim (\x. f x + g x) at_infinity F" proof (subst filterlim_at_infinity[OF order_refl], safe) fix r :: real assume r: "r > 0" - from assms(1) have "((\x. norm (f x)) ---> norm c) F" by (rule tendsto_norm) + from assms(1) have "((\x. norm (f x)) \ norm c) F" by (rule tendsto_norm) hence "eventually (\x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all with assms(2) have "eventually (\x. norm (g x) \ r + norm c + 1) F" @@ -1178,7 +1178,7 @@ lemma tendsto_add_filterlim_at_infinity': assumes "filterlim f at_infinity F" - assumes "(g ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)" + assumes "(g \ (c :: 'b :: real_normed_vector)) (F :: 'a filter)" shows "filterlim (\x. f x + g x) at_infinity F" by (subst add.commute) (rule tendsto_add_filterlim_at_infinity assms)+ @@ -1188,7 +1188,7 @@ (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl) lemma filterlim_inverse_at_top: - "(f ---> (0 :: real)) F \ eventually (\x. 0 < f x) F \ LIM x F. inverse (f x) :> at_top" + "(f \ (0 :: real)) F \ eventually (\x. 0 < f x) F \ LIM x F. inverse (f x) :> at_top" by (intro filterlim_compose[OF filterlim_inverse_at_top_right]) (simp add: filterlim_def eventually_filtermap eventually_mono at_within_def le_principal) @@ -1197,7 +1197,7 @@ by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right) lemma filterlim_inverse_at_bot: - "(f ---> (0 :: real)) F \ eventually (\x. f x < 0) F \ LIM x F. inverse (f x) :> at_bot" + "(f \ (0 :: real)) F \ eventually (\x. f x < 0) F \ LIM x F. inverse (f x) :> at_bot" unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric] by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric]) @@ -1258,11 +1258,11 @@ qed lemma tendsto_mult_filterlim_at_infinity: - assumes "F \ bot" "(f ---> (c :: 'a :: real_normed_field)) F" "c \ 0" + assumes "F \ bot" "(f \ (c :: 'a :: real_normed_field)) F" "c \ 0" assumes "filterlim g at_infinity F" shows "filterlim (\x. f x * g x) at_infinity F" proof - - have "((\x. inverse (f x) * inverse (g x)) ---> inverse c * 0) F" + have "((\x. inverse (f x) * inverse (g x)) \ inverse c * 0) F" by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0]) hence "filterlim (\x. inverse (f x) * inverse (g x)) (at (inverse c * 0)) F" unfolding filterlim_at using assms @@ -1270,7 +1270,7 @@ thus ?thesis by (subst filterlim_inverse_at_iff[symmetric]) simp_all qed -lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \ ((\x. inverse (f x) :: real) ---> 0) F" +lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \ ((\x. inverse (f x) :: real) \ 0) F" by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) lemma mult_nat_left_at_top: "c > 0 \ filterlim (\x. c * x :: nat) at_top sequentially" @@ -1283,7 +1283,7 @@ fixes x :: "'a :: {real_normed_field,field}" shows "(at (0::'a)) = filtermap inverse at_infinity" proof (rule antisym) - have "(inverse ---> (0::'a)) at_infinity" + have "(inverse \ (0::'a)) at_infinity" by (fact tendsto_inverse_0) then show "filtermap inverse at_infinity \ at (0::'a)" apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def) @@ -1299,12 +1299,12 @@ lemma lim_at_infinity_0: fixes l :: "'a :: {real_normed_field,field}" - shows "(f ---> l) at_infinity \ ((f o inverse) ---> l) (at (0::'a))" + shows "(f \ l) at_infinity \ ((f o inverse) \ l) (at (0::'a))" by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap) lemma lim_zero_infinity: fixes l :: "'a :: {real_normed_field,field}" - shows "((\x. f(1 / x)) ---> l) (at (0::'a)) \ (f ---> l) at_infinity" + shows "((\x. f(1 / x)) \ l) (at (0::'a)) \ (f \ l) at_infinity" by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def) @@ -1316,7 +1316,7 @@ \ lemma filterlim_tendsto_pos_mult_at_top: - assumes f: "(f ---> c) F" and c: "0 < c" + assumes f: "(f \ c) F" and c: "0 < c" assumes g: "LIM x F. g x :> at_top" shows "LIM x F. (f x * g x :: real) :> at_top" unfolding filterlim_at_top_gt[where c=0] @@ -1359,13 +1359,13 @@ qed lemma filterlim_tendsto_pos_mult_at_bot: - assumes "(f ---> c) F" "0 < (c::real)" "filterlim g at_bot F" + assumes "(f \ c) F" "0 < (c::real)" "filterlim g at_bot F" shows "LIM x F. f x * g x :> at_bot" using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\x. - g x"] assms(3) unfolding filterlim_uminus_at_bot by simp lemma filterlim_tendsto_neg_mult_at_bot: - assumes c: "(f ---> c) F" "(c::real) < 0" and g: "filterlim g at_top F" + assumes c: "(f \ c) F" "(c::real) < 0" and g: "filterlim g at_top F" shows "LIM x F. f x * g x :> at_bot" using c filterlim_tendsto_pos_mult_at_top[of "\x. - f x" "- c" F, OF _ _ g] unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp @@ -1390,7 +1390,7 @@ using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_bot) lemma filterlim_tendsto_add_at_top: - assumes f: "(f ---> c) F" + assumes f: "(f \ c) F" assumes g: "LIM x F. g x :> at_top" shows "LIM x F. (f x + g x :: real) :> at_top" unfolding filterlim_at_top_gt[where c=0] @@ -1406,8 +1406,8 @@ lemma LIM_at_top_divide: fixes f g :: "'a \ real" - assumes f: "(f ---> a) F" "0 < a" - assumes g: "(g ---> 0) F" "eventually (\x. 0 < g x) F" + assumes f: "(f \ a) F" "0 < a" + assumes g: "(g \ 0) F" "eventually (\x. 0 < g x) F" shows "LIM x F. f x / g x :> at_top" unfolding divide_inverse by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) @@ -1429,9 +1429,9 @@ lemma tendsto_divide_0: fixes f :: "_ \ 'a::{real_normed_div_algebra, division_ring}" - assumes f: "(f ---> c) F" + assumes f: "(f \ c) F" assumes g: "LIM x F. g x :> at_infinity" - shows "((\x. f x / g x) ---> 0) F" + shows "((\x. f x / g x) \ 0) F" using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse) lemma linear_plus_1_le_power: @@ -1510,16 +1510,16 @@ lemma Lim_transform: fixes a b :: "'a::real_normed_vector" - shows "\(g ---> a) F; ((\x. f x - g x) ---> 0) F\ \ (f ---> a) F" + shows "\(g \ a) F; ((\x. f x - g x) \ 0) F\ \ (f \ a) F" using tendsto_add [of g a F "\x. f x - g x" 0] by simp lemma Lim_transform2: fixes a b :: "'a::real_normed_vector" - shows "\(f ---> a) F; ((\x. f x - g x) ---> 0) F\ \ (g ---> a) F" + shows "\(f \ a) F; ((\x. f x - g x) \ 0) F\ \ (g \ a) F" by (erule Lim_transform) (simp add: tendsto_minus_cancel) lemma Lim_transform_eventually: - "eventually (\x. f x = g x) net \ (f ---> l) net \ (g ---> l) net" + "eventually (\x. f x = g x) net \ (f \ l) net \ (g \ l) net" apply (rule topological_tendstoI) apply (drule (2) topological_tendstoD) apply (erule (1) eventually_elim2, simp) @@ -1528,19 +1528,19 @@ lemma Lim_transform_within: assumes "0 < d" and "\x'\S. 0 < dist x' x \ dist x' x < d \ f x' = g x'" - and "(f ---> l) (at x within S)" - shows "(g ---> l) (at x within S)" + and "(f \ l) (at x within S)" + shows "(g \ l) (at x within S)" proof (rule Lim_transform_eventually) show "eventually (\x. f x = g x) (at x within S)" using assms(1,2) by (auto simp: dist_nz eventually_at) - show "(f ---> l) (at x within S)" by fact + show "(f \ l) (at x within S)" by fact qed lemma Lim_transform_at: assumes "0 < d" and "\x'. 0 < dist x' x \ dist x' x < d \ f x' = g x'" - and "(f ---> l) (at x)" - shows "(g ---> l) (at x)" + and "(f \ l) (at x)" + shows "(g \ l) (at x)" using _ assms(3) proof (rule Lim_transform_eventually) show "eventually (\x. f x = g x) (at x)" @@ -1554,10 +1554,10 @@ fixes a b :: "'a::t1_space" assumes "a \ b" and "\x\S. x \ a \ x \ b \ f x = g x" - and "(f ---> l) (at a within S)" - shows "(g ---> l) (at a within S)" + and "(f \ l) (at a within S)" + shows "(g \ l) (at a within S)" proof (rule Lim_transform_eventually) - show "(f ---> l) (at a within S)" by fact + show "(f \ l) (at a within S)" by fact show "eventually (\x. f x = g x) (at a within S)" unfolding eventually_at_topological by (rule exI [where x="- {b}"], simp add: open_Compl assms) @@ -1567,8 +1567,8 @@ fixes a b :: "'a::t1_space" assumes ab: "a\b" and fg: "\x. x \ a \ x \ b \ f x = g x" - and fl: "(f ---> l) (at a)" - shows "(g ---> l) (at a)" + and fl: "(f \ l) (at a)" + shows "(g \ l) (at a)" using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp text\Alternatively, within an open set.\ @@ -1576,13 +1576,13 @@ lemma Lim_transform_within_open: assumes "open S" and "a \ S" and "\x\S. x \ a \ f x = g x" - and "(f ---> l) (at a)" - shows "(g ---> l) (at a)" + and "(f \ l) (at a)" + shows "(g \ l) (at a)" proof (rule Lim_transform_eventually) show "eventually (\x. f x = g x) (at a)" unfolding eventually_at_topological using assms(1,2,3) by auto - show "(f ---> l) (at a)" by fact + show "(f \ l) (at a)" by fact qed text\A congruence rule allowing us to transform limits assuming not at point.\ @@ -1594,14 +1594,14 @@ and "x = y" and "S = T" and "\x. x \ b \ x \ T \ f x = g x" - shows "(f ---> x) (at a within S) \ (g ---> y) (at b within T)" + shows "(f \ x) (at a within S) \ (g \ y) (at b within T)" unfolding tendsto_def eventually_at_topological using assms by simp lemma Lim_cong_at(*[cong add]*): assumes "a = b" "x = y" and "\x. x \ a \ f x = g x" - shows "((\x. f x) ---> x) (at a) \ ((g ---> y) (at a))" + shows "((\x. f x) \ x) (at a) \ ((g \ y) (at a))" unfolding tendsto_def eventually_at_topological using assms by simp text\An unbounded sequence's inverse tends to 0\ @@ -1636,7 +1636,7 @@ using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]] by auto -lemma lim_1_over_n: "((\n. 1 / of_nat n) ---> (0::'a::real_normed_field)) sequentially" +lemma lim_1_over_n: "((\n. 1 / of_nat n) \ (0::'a::real_normed_field)) sequentially" proof (subst lim_sequentially, intro allI impI exI) fix e :: real assume e: "e > 0" fix n :: nat assume n: "n \ nat \inverse e + 1\" @@ -1646,7 +1646,7 @@ by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide) qed -lemma lim_inverse_n: "((\n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially" +lemma lim_inverse_n: "((\n. inverse(of_nat n)) \ (0::'a::real_normed_field)) sequentially" using lim_1_over_n by (simp add: inverse_eq_divide) lemma LIMSEQ_Suc_n_over_n: "(\n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \ 1" @@ -1979,17 +1979,17 @@ lemma LIM_zero: fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" + shows "(f \ l) F \ ((\x. f x - l) \ 0) F" unfolding tendsto_iff dist_norm by simp lemma LIM_zero_cancel: fixes f :: "'a::topological_space \ 'b::real_normed_vector" - shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" + shows "((\x. f x - l) \ 0) F \ (f \ l) F" unfolding tendsto_iff dist_norm by simp lemma LIM_zero_iff: fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "((\x. f x - l) ---> 0) F = (f ---> l) F" + shows "((\x. f x - l) \ 0) F = (f \ l) F" unfolding tendsto_iff dist_norm by simp lemma LIM_imp_LIM: @@ -2152,7 +2152,7 @@ assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" shows "0 \ f x" proof (rule tendsto_le_const) - show "(f ---> f x) (at_left x)" + show "(f \ f x) (at_left x)" using \isCont f x\ by (simp add: filterlim_at_split isCont_def) show "eventually (\x. 0 \ f x) (at_left x)" using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"]) diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Wed Dec 30 11:21:54 2015 +0100 @@ -355,8 +355,8 @@ lemma tendsto_componentwise1: fixes a::"'a::euclidean_space \\<^sub>L 'b::real_normed_vector" and b::"'c \ 'a \\<^sub>L 'b" - assumes "(\j. j \ Basis \ ((\n. b n j) ---> a j) F)" - shows "(b ---> a) F" + assumes "(\j. j \ Basis \ ((\n. b n j) \ a j) F)" + shows "(b \ a) F" proof - have "\j. j \ Basis \ Zfun (\x. norm (b x j - a j)) F" using assms unfolding tendsto_Zfun_iff Zfun_norm_iff . @@ -408,8 +408,8 @@ done lemma tendsto_blinfun_of_matrix: - assumes "\i j. i \ Basis \ j \ Basis \ ((\n. b n i j) ---> a i j) F" - shows "((\n. blinfun_of_matrix (b n)) ---> blinfun_of_matrix a) F" + assumes "\i j. i \ Basis \ j \ Basis \ ((\n. b n i j) \ a i j) F" + shows "((\n. blinfun_of_matrix (b n)) \ blinfun_of_matrix a) F" proof - have "\i j. i \ Basis \ j \ Basis \ Zfun (\x. norm (b x i j - a i j)) F" using assms unfolding tendsto_Zfun_iff Zfun_norm_iff . @@ -423,7 +423,7 @@ lemma tendsto_componentwise: fixes a::"'a::euclidean_space \\<^sub>L 'b::euclidean_space" and b::"'c \ 'a \\<^sub>L 'b" - shows "(\i j. i \ Basis \ j \ Basis \ ((\n. b n j \ i) ---> a j \ i) F) \ (b ---> a) F" + shows "(\i j. i \ Basis \ j \ Basis \ ((\n. b n j \ i) \ a j \ i) F) \ (b \ a) F" apply (subst blinfun_of_matrix_works[of a, symmetric]) apply (subst blinfun_of_matrix_works[of "b x" for x, symmetric, abs_def]) by (rule tendsto_blinfun_of_matrix) @@ -495,7 +495,7 @@ by (metis (lifting) bounded_subset f' image_subsetI s') then obtain l2 r2 where r2: "subseq r2" - and lr2: "((\i. f (r1 (r2 i)) k) ---> l2) sequentially" + and lr2: "((\i. f (r1 (r2 i)) k) \ l2) sequentially" using bounded_imp_convergent_subsequence[of "\i. f (r1 i) k"] by (auto simp: o_def) def r \ "r1 \ r2" @@ -585,9 +585,9 @@ ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" using eventually_elim2 by force } - then have *: "((f \ r) ---> l) sequentially" + then have *: "((f \ r) \ l) sequentially" unfolding o_def tendsto_iff by simp - with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" + with r show "\l r. subseq r \ ((f \ r) \ l) sequentially" by auto qed diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Dec 30 11:21:54 2015 +0100 @@ -842,7 +842,7 @@ have "bounded (range (\i. f (r1 i) $ k))" by (metis (lifting) bounded_subset image_subsetI f' s') then obtain l2 r2 where r2: "subseq r2" - and lr2: "((\i. f (r1 (r2 i)) $ k) ---> l2) sequentially" + and lr2: "((\i. f (r1 (r2 i)) $ k) \ l2) sequentially" using bounded_imp_convergent_subsequence[of "\i. f (r1 i) $ k"] by (auto simp: o_def) def r \ "r1 \ r2" have r: "subseq r" @@ -888,8 +888,8 @@ ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" by (rule eventually_mono) } - hence "((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp - with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" by auto + hence "((f \ r) \ l) sequentially" unfolding o_def tendsto_iff by simp + with r show "\l r. subseq r \ ((f \ r) \ l) sequentially" by auto qed lemma interval_cart: @@ -1014,19 +1014,19 @@ lemma Lim_component_le_cart: fixes f :: "'a \ real^'n" - assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. f x $i \ b) net" + assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. f x $i \ b) net" shows "l$i \ b" by (rule tendsto_le[OF assms(2) tendsto_const tendsto_vec_nth, OF assms(1, 3)]) lemma Lim_component_ge_cart: fixes f :: "'a \ real^'n" - assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)$i) net" + assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)$i) net" shows "b \ l$i" by (rule tendsto_le[OF assms(2) tendsto_vec_nth tendsto_const, OF assms(1, 3)]) lemma Lim_component_eq_cart: fixes f :: "'a \ real^'n" - assumes net: "(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)$i = b) net" + assumes net: "(f \ l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)$i = b) net" shows "l$i = b" using ev[unfolded order_eq_iff eventually_conj_iff] and Lim_component_ge_cart[OF net, of b i] and diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Dec 30 11:21:54 2015 +0100 @@ -2664,7 +2664,7 @@ then have "\d>0. \y\s. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using d1 by blast } - then have *: "((\y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) ---> 0) (at x within s)" + then have *: "((\y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) \ 0) (at x within s)" by (simp add: Lim_within dist_norm inverse_eq_divide) show ?thesis apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right) @@ -5237,7 +5237,7 @@ and noleB: "\t. t \ {0..1} \ norm (vector_derivative \ (at t)) \ B" and \: "valid_path \" and [simp]: "~ (trivial_limit F)" - shows "l contour_integrable_on \" "((\n. contour_integral \ (f n)) ---> contour_integral \ l) F" + shows "l contour_integrable_on \" "((\n. contour_integral \ (f n)) \ contour_integral \ l) F" proof - have "0 \ B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one) { fix e::real @@ -5292,7 +5292,7 @@ apply (blast intro: *)+ done } - then show "((\n. contour_integral \ (f n)) ---> contour_integral \ l) F" + then show "((\n. contour_integral \ (f n)) \ contour_integral \ l) F" by (rule tendstoI) qed @@ -5300,7 +5300,7 @@ assumes ev_fint: "eventually (\n::'a. (f n) contour_integrable_on (circlepath z r)) F" and ev_no: "\e. 0 < e \ eventually (\n. \x \ path_image (circlepath z r). norm(f n x - l x) < e) F" and [simp]: "~ (trivial_limit F)" "0 < r" - shows "l contour_integrable_on (circlepath z r)" "((\n. contour_integral (circlepath z r) (f n)) ---> contour_integral (circlepath z r) l) F" + shows "l contour_integrable_on (circlepath z r)" "((\n. contour_integral (circlepath z r) (f n)) \ contour_integral (circlepath z r) l) F" by (auto simp: vector_derivative_circlepath norm_mult intro: contour_integral_uniform_limit assms) @@ -6156,7 +6156,7 @@ text\ These weak Liouville versions don't even need the derivative formula.\ lemma Liouville_weak_0: - assumes holf: "f holomorphic_on UNIV" and inf: "(f ---> 0) at_infinity" + assumes holf: "f holomorphic_on UNIV" and inf: "(f \ 0) at_infinity" shows "f z = 0" proof (rule ccontr) assume fz: "f z \ 0" @@ -6182,7 +6182,7 @@ qed proposition Liouville_weak: - assumes "f holomorphic_on UNIV" and "(f ---> l) at_infinity" + assumes "f holomorphic_on UNIV" and "(f \ l) at_infinity" shows "f z = l" using Liouville_weak_0 [of "\z. f z - l"] by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero) @@ -6195,7 +6195,7 @@ { assume f: "\z. f z \ 0" have 1: "(\x. 1 / f x) holomorphic_on UNIV" by (simp add: holomorphic_on_divide holomorphic_on_const assms f) - have 2: "((\x. 1 / f x) ---> 0) at_infinity" + have 2: "((\x. 1 / f x) \ 0) at_infinity" apply (rule tendstoI [OF eventually_mono]) apply (rule_tac B="2/e" in unbounded) apply (simp add: dist_norm norm_divide divide_simps mult_ac) @@ -6274,16 +6274,16 @@ done have g_cint: "(\u. g u/(u - w)) contour_integrable_on circlepath z r" by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \0 < r\]) - have cif_tends_cig: "((\n. contour_integral(circlepath z r) (\u. f n u / (u - w))) ---> contour_integral(circlepath z r) (\u. g u/(u - w))) F" + have cif_tends_cig: "((\n. contour_integral(circlepath z r) (\u. f n u / (u - w))) \ contour_integral(circlepath z r) (\u. g u/(u - w))) F" by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \0 < r\]) - have f_tends_cig: "((\n. 2 * of_real pi * ii * f n w) ---> contour_integral (circlepath z r) (\u. g u / (u - w))) F" + have f_tends_cig: "((\n. 2 * of_real pi * ii * f n w) \ contour_integral (circlepath z r) (\u. g u / (u - w))) F" apply (rule Lim_transform_eventually [where f = "\n. contour_integral (circlepath z r) (\u. f n u/(u - w))"]) apply (rule eventually_mono [OF cont]) apply (rule contour_integral_unique [OF Cauchy_integral_circlepath]) using w apply (auto simp: norm_minus_commute dist_norm cif_tends_cig) done - have "((\n. 2 * of_real pi * \ * f n w) ---> 2 * of_real pi * \ * g w) F" + have "((\n. 2 * of_real pi * \ * f n w) \ 2 * of_real pi * \ * g w) F" apply (rule tendsto_mult_left [OF tendstoI]) apply (rule eventually_mono [OF lim], assumption) using w @@ -6314,7 +6314,7 @@ and F: "~ trivial_limit F" and "0 < r" obtains g' where "continuous_on (cball z r) g" - "\w. w \ ball z r \ (g has_field_derivative (g' w)) (at w) \ ((\n. f' n w) ---> g' w) F" + "\w. w \ ball z r \ (g has_field_derivative (g' w)) (at w) \ ((\n. f' n w) \ g' w) F" proof - let ?conint = "contour_integral (circlepath z r)" have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r" @@ -6325,7 +6325,7 @@ by (fastforce simp add: holomorphic_on_open) then have derg: "\x. x \ ball z r \ deriv g x = g' x" by (simp add: DERIV_imp_deriv) - have tends_f'n_g': "((\n. f' n w) ---> g' w) F" if w: "w \ ball z r" for w + have tends_f'n_g': "((\n. f' n w) \ g' w) F" if w: "w \ ball z r" for w proof - have eq_f': "?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \)" if cont_fn: "continuous_on (cball z r) (f n)" @@ -6359,17 +6359,17 @@ apply (force simp add: dist_norm dle intro: less_le_trans) done have "((\n. contour_integral (circlepath z r) (\x. f n x / (x - w)\<^sup>2)) - ---> contour_integral (circlepath z r) ((\x. g x / (x - w)\<^sup>2))) F" + \ contour_integral (circlepath z r) ((\x. g x / (x - w)\<^sup>2))) F" by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \0 < r\]) - then have tendsto_0: "((\n. 1 / (2 * of_real pi * \) * (?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2))) ---> 0) F" + then have tendsto_0: "((\n. 1 / (2 * of_real pi * \) * (?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2))) \ 0) F" using Lim_null by (force intro!: tendsto_mult_right_zero) - have "((\n. f' n w - g' w) ---> 0) F" + have "((\n. f' n w - g' w) \ 0) F" apply (rule Lim_transform_eventually [OF _ tendsto_0]) apply (force simp add: divide_simps intro: eq_f' eventually_mono [OF cont]) done then show ?thesis using Lim_null by blast qed - obtain g' where "\w. w \ ball z r \ (g has_field_derivative (g' w)) (at w) \ ((\n. f' n w) ---> g' w) F" + obtain g' where "\w. w \ ball z r \ (g has_field_derivative (g' w)) (at w) \ ((\n. f' n w) \ g' w) F" by (blast intro: tends_f'n_g' g' ) then show ?thesis using g using that by blast diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Dec 30 11:21:54 2015 +0100 @@ -42,28 +42,28 @@ lemma tendsto_Re_upper: assumes "~ (trivial_limit F)" - "(f ---> l) F" + "(f \ l) F" "eventually (\x. Re(f x) \ b) F" shows "Re(l) \ b" by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Re) lemma tendsto_Re_lower: assumes "~ (trivial_limit F)" - "(f ---> l) F" + "(f \ l) F" "eventually (\x. b \ Re(f x)) F" shows "b \ Re(l)" by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Re) lemma tendsto_Im_upper: assumes "~ (trivial_limit F)" - "(f ---> l) F" + "(f \ l) F" "eventually (\x. Im(f x) \ b) F" shows "Im(l) \ b" by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Im) lemma tendsto_Im_lower: assumes "~ (trivial_limit F)" - "(f ---> l) F" + "(f \ l) F" "eventually (\x. b \ Im(f x)) F" shows "b \ Im(l)" by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Im) @@ -237,7 +237,7 @@ lemma real_lim: fixes l::complex - assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\a. P a \ f a \ \" + assumes "(f \ l) F" and "~(trivial_limit F)" and "eventually P F" and "\a. P a \ f a \ \" shows "l \ \" proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)]) show "eventually (\x. f x \ \) F" @@ -246,7 +246,7 @@ lemma real_lim_sequentially: fixes l::complex - shows "(f ---> l) sequentially \ (\N. \n\N. f n \ \) \ l \ \" + shows "(f \ l) sequentially \ (\N. \n\N. f n \ \) \ l \ \" by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially) lemma real_series: @@ -256,7 +256,7 @@ by (metis real_lim_sequentially setsum_in_Reals) lemma Lim_null_comparison_Re: - assumes "eventually (\x. norm(f x) \ Re(g x)) F" "(g ---> 0) F" shows "(f ---> 0) F" + assumes "eventually (\x. norm(f x) \ Re(g x)) F" "(g \ 0) F" shows "(f \ 0) F" by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp subsection\Holomorphic functions\ @@ -812,11 +812,11 @@ assumes cvs: "convex s" and df: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x within s)" and conv: "\e. 0 < e \ \N. \n x. n \ N \ x \ s \ norm (f' n x - g' x) \ e" - and "\x l. x \ s \ ((\n. f n x) ---> l) sequentially" - shows "\g. \x \ s. ((\n. f n x) ---> g x) sequentially \ + and "\x l. x \ s \ ((\n. f n x) \ l) sequentially" + shows "\g. \x \ s. ((\n. f n x) \ g x) sequentially \ (g has_field_derivative (g' x)) (at x within s)" proof - - from assms obtain x l where x: "x \ s" and tf: "((\n. f n x) ---> l) sequentially" + from assms obtain x l where x: "x \ s" and tf: "((\n. f n x) \ l) sequentially" by blast { fix e::real assume e: "e > 0" then obtain N where N: "\n\N. \x. x \ s \ cmod (f' n x - g' x) \ e" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Wed Dec 30 11:21:54 2015 +0100 @@ -1564,7 +1564,7 @@ lemma lim_Ln_over_power: fixes s::complex assumes "0 < Re s" - shows "((\n. Ln n / (n powr s)) ---> 0) sequentially" + shows "((\n. Ln n / (n powr s)) \ 0) sequentially" proof (simp add: lim_sequentially dist_norm, clarify) fix e::real assume e: "0 < e" @@ -1603,7 +1603,7 @@ done qed -lemma lim_Ln_over_n: "((\n. Ln(of_nat n) / of_nat n) ---> 0) sequentially" +lemma lim_Ln_over_n: "((\n. Ln(of_nat n) / of_nat n) \ 0) sequentially" using lim_Ln_over_power [of 1] by simp @@ -1616,14 +1616,14 @@ lemma lim_ln_over_power: fixes s :: real assumes "0 < s" - shows "((\n. ln n / (n powr s)) ---> 0) sequentially" + shows "((\n. ln n / (n powr s)) \ 0) sequentially" using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms apply (subst filterlim_sequentially_Suc [symmetric]) apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) done -lemma lim_ln_over_n: "((\n. ln(real_of_nat n) / of_nat n) ---> 0) sequentially" +lemma lim_ln_over_n: "((\n. ln(real_of_nat n) / of_nat n) \ 0) sequentially" using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]] apply (subst filterlim_sequentially_Suc [symmetric]) apply (simp add: lim_sequentially dist_norm) @@ -1631,7 +1631,7 @@ lemma lim_1_over_complex_power: assumes "0 < Re s" - shows "((\n. 1 / (of_nat n powr s)) ---> 0) sequentially" + shows "((\n. 1 / (of_nat n powr s)) \ 0) sequentially" proof - have "\n>0. 3 \ n \ 1 \ ln (real_of_nat n)" using ln3_gt_1 @@ -1648,14 +1648,14 @@ lemma lim_1_over_real_power: fixes s :: real assumes "0 < s" - shows "((\n. 1 / (of_nat n powr s)) ---> 0) sequentially" + shows "((\n. 1 / (of_nat n powr s)) \ 0) sequentially" using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms apply (subst filterlim_sequentially_Suc [symmetric]) apply (simp add: lim_sequentially dist_norm) apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide) done -lemma lim_1_over_Ln: "((\n. 1 / Ln(of_nat n)) ---> 0) sequentially" +lemma lim_1_over_Ln: "((\n. 1 / Ln(of_nat n)) \ 0) sequentially" proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps) fix r::real assume "0 < r" @@ -1680,7 +1680,7 @@ done qed -lemma lim_1_over_ln: "((\n. 1 / ln(real_of_nat n)) ---> 0) sequentially" +lemma lim_1_over_ln: "((\n. 1 / ln(real_of_nat n)) \ 0) sequentially" using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms apply (subst filterlim_sequentially_Suc [symmetric]) apply (simp add: lim_sequentially dist_norm) diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Dec 30 11:21:54 2015 +0100 @@ -70,12 +70,12 @@ text \These are the only cases we'll care about, probably.\ lemma has_derivative_within: "(f has_derivative f') (at x within s) \ - bounded_linear f' \ ((\y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)" + bounded_linear f' \ ((\y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \ 0) (at x within s)" unfolding has_derivative_def Lim by (auto simp add: netlimit_within field_simps) lemma has_derivative_at: "(f has_derivative f') (at x) \ - bounded_linear f' \ ((\y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)" + bounded_linear f' \ ((\y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \ 0) (at x)" using has_derivative_within [of f f' x UNIV] by simp @@ -111,14 +111,14 @@ fixes f :: "real \ real" and y :: "real" shows "(f has_derivative (op * y)) (at x within ({x <..} \ I)) \ - ((\t. (f x - f t) / (x - t)) ---> y) (at x within ({x <..} \ I))" + ((\t. (f x - f t) / (x - t)) \ y) (at x within ({x <..} \ I))" proof - - have "((\t. (f t - (f x + y * (t - x))) / \t - x\) ---> 0) (at x within ({x<..} \ I)) \ - ((\t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \ I))" + have "((\t. (f t - (f x + y * (t - x))) / \t - x\) \ 0) (at x within ({x<..} \ I)) \ + ((\t. (f t - f x) / (t - x) - y) \ 0) (at x within ({x<..} \ I))" by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib) - also have "\ \ ((\t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \ I))" + also have "\ \ ((\t. (f t - f x) / (t - x)) \ y) (at x within ({x<..} \ I))" by (simp add: Lim_null[symmetric]) - also have "\ \ ((\t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \ I))" + also have "\ \ ((\t. (f x - f t) / (x - t)) \ y) (at x within ({x<..} \ I))" by (intro Lim_cong_within) (simp_all add: field_simps) finally show ?thesis by (simp add: bounded_linear_mult_right has_derivative_within) @@ -127,7 +127,7 @@ subsubsection \Caratheodory characterization\ lemma DERIV_within_iff: - "(f has_field_derivative D) (at a within s) \ ((\z. (f z - f a) / (z - a)) ---> D) (at a within s)" + "(f has_field_derivative D) (at a within s) \ ((\z. (f z - f a) / (z - a)) \ D) (at a within s)" proof - have 1: "\w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)" by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult.commute) @@ -816,8 +816,8 @@ using \a < x2\ by (auto simp: trivial_limit_within islimpt_in_closure) moreover - have "((\x1. (\ x1 - \ a) + e * (x1 - a) + e) ---> (\ x2 - \ a) + e * (x2 - a) + e) (at x2 within {a <..x1. norm (f x1 - f a)) ---> norm (f x2 - f a)) (at x2 within {a <..x1. (\ x1 - \ a) + e * (x1 - a) + e) \ (\ x2 - \ a) + e * (x2 - a) + e) (at x2 within {a <..x1. norm (f x1 - f a)) \ norm (f x2 - f a)) (at x2 within {a <..n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" and "\e>0. \N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" and "x0 \ s" - and "((\n. f n x0) ---> l) sequentially" - shows "\g. \x\s. ((\n. f n x) ---> g x) sequentially \ (g has_derivative g'(x)) (at x within s)" + and "((\n. f n x0) \ l) sequentially" + shows "\g. \x\s. ((\n. f n x) \ g x) sequentially \ (g has_derivative g'(x)) (at x within s)" proof - have lem1: "\e>0. \N. \m\N. \n\N. \x\s. \y\s. norm ((f m x - f n x) - (f m y - f n y)) \ e * norm (x - y)" using assms(1,2,3) by (rule has_derivative_sequence_lipschitz) - have "\g. \x\s. ((\n. f n x) ---> g x) sequentially" + have "\g. \x\s. ((\n. f n x) \ g x) sequentially" apply (rule bchoice) unfolding convergent_eq_cauchy proof @@ -1970,7 +1970,7 @@ proof rule+ fix n x y assume as: "N \ n" "x \ s" "y \ s" - have "((\m. norm (f n x - f n y - (f m x - f m y))) ---> norm (f n x - f n y - (g x - g y))) sequentially" + have "((\m. norm (f n x - f n y - (f m x - f m y))) \ norm (f n x - f n y - (g x - g y))) sequentially" by (intro tendsto_intros g[rule_format] as) moreover have "eventually (\m. norm (f n x - f n y - (f m x - f m y)) \ e * norm (x - y)) sequentially" unfolding eventually_sequentially @@ -1988,14 +1988,14 @@ by (rule tendsto_ge_const[OF trivial_limit_sequentially]) qed qed - have "\x\s. ((\n. f n x) ---> g x) sequentially \ (g has_derivative g' x) (at x within s)" + have "\x\s. ((\n. f n x) \ g x) sequentially \ (g has_derivative g' x) (at x within s)" unfolding has_derivative_within_alt2 proof (intro ballI conjI) fix x assume "x \ s" - then show "((\n. f n x) ---> g x) sequentially" + then show "((\n. f n x) \ g x) sequentially" by (simp add: g) - have lem3: "\u. ((\n. f' n x u) ---> g' x u) sequentially" + have lem3: "\u. ((\n. f' n x u) \ g' x u) sequentially" unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm proof (intro allI impI) fix u @@ -2554,7 +2554,7 @@ from c have "c \ interior A \ closure {c<..}" by auto also have "\ \ closure (interior A \ {c<..})" by (intro open_inter_closure_subset) auto finally have "at c within ?A' \ bot" by (subst at_within_eq_bot_iff) auto - moreover from deriv have "((\y. (f y - f c) / (y - c)) ---> f') (at c within ?A')" + moreover from deriv have "((\y. (f y - f c) / (y - c)) \ f') (at c within ?A')" unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le) moreover from eventually_at_right_real[OF xc] have "eventually (\y. (f y - f c) / (y - c) \ (f x - f c) / (x - c)) (at_right c)" @@ -2576,7 +2576,7 @@ from c have "c \ interior A \ closure {.. \ closure (interior A \ {.. bot" by (subst at_within_eq_bot_iff) auto - moreover from deriv have "((\y. (f y - f c) / (y - c)) ---> f') (at c within ?A')" + moreover from deriv have "((\y. (f y - f c) / (y - c)) \ f') (at c within ?A')" unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le) moreover from eventually_at_left_real[OF xc] have "eventually (\y. (f y - f c) / (y - c) \ (f x - f c) / (x - c)) (at_left c)" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Wed Dec 30 11:21:54 2015 +0100 @@ -324,7 +324,7 @@ by (auto simp: filter_eq_iff eventually_at_filter le_less) moreover have "0 < x \ at x within {0 ..} = at x" using at_within_interior[of x "{0 ..}"] by (simp add: interior_Ici[of "- \"]) - ultimately show "(inverse ---> inverse x) (at x within {0..})" + ultimately show "(inverse \ inverse x) (at x within {0..})" by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos) qed diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Dec 30 11:21:54 2015 +0100 @@ -196,8 +196,8 @@ qed lemma tendsto_vec_nth [tendsto_intros]: - assumes "((\x. f x) ---> a) net" - shows "((\x. f x $ i) ---> a $ i) net" + assumes "((\x. f x) \ a) net" + shows "((\x. f x $ i) \ a $ i) net" proof (rule topological_tendstoI) fix S assume "open S" "a $ i \ S" then have "open ((\y. y $ i) -` S)" "a \ ((\y. y $ i) -` S)" @@ -212,8 +212,8 @@ unfolding isCont_def by (rule tendsto_vec_nth) lemma vec_tendstoI: - assumes "\i. ((\x. f x $ i) ---> a $ i) net" - shows "((\x. f x) ---> a) net" + assumes "\i. ((\x. f x $ i) \ a $ i) net" + shows "((\x. f x) \ a) net" proof (rule topological_tendstoI) fix S assume "open S" and "a \ S" then obtain A where A: "\i. open (A i)" "\i. a $ i \ A i" @@ -228,8 +228,8 @@ qed lemma tendsto_vec_lambda [tendsto_intros]: - assumes "\i. ((\x. f x i) ---> a i) net" - shows "((\x. \ i. f x i) ---> (\ i. a i)) net" + assumes "\i. ((\x. f x i) \ a i) net" + shows "((\x. \ i. f x i) \ (\ i. a i)) net" using assms by (simp add: vec_tendstoI) lemma open_image_vec_nth: assumes "open S" shows "open ((\x. x $ i) ` S)" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Dec 30 11:21:54 2015 +0100 @@ -9665,9 +9665,9 @@ fixes f :: "nat \ 'n::euclidean_space \ real" assumes "\k. (f k) integrable_on cbox a b" and "\k. \x\cbox a b.(f k x) \ f (Suc k) x" - and "\x\cbox a b. ((\k. f k x) ---> g x) sequentially" + and "\x\cbox a b. ((\k. f k x) \ g x) sequentially" and "bounded {integral (cbox a b) (f k) | k . k \ UNIV}" - shows "g integrable_on cbox a b \ ((\k. integral (cbox a b) (f k)) ---> integral (cbox a b) g) sequentially" + shows "g integrable_on cbox a b \ ((\k. integral (cbox a b) (f k)) \ integral (cbox a b) g) sequentially" proof (cases "content (cbox a b) = 0") case True show ?thesis @@ -9692,7 +9692,7 @@ apply auto done qed - have "\i. ((\k. integral (cbox a b) (f k)) ---> i) sequentially" + have "\i. ((\k. integral (cbox a b) (f k)) \ i) sequentially" apply (rule bounded_increasing_convergent) defer apply rule @@ -9935,15 +9935,15 @@ fixes f :: "nat \ 'n::euclidean_space \ real" assumes "\k. (f k) integrable_on s" and "\k. \x\s. (f k x) \ (f (Suc k) x)" - and "\x\s. ((\k. f k x) ---> g x) sequentially" + and "\x\s. ((\k. f k x) \ g x) sequentially" and "bounded {integral s (f k)| k. True}" - shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" -proof - - have lem: "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" + shows "g integrable_on s \ ((\k. integral s (f k)) \ integral s g) sequentially" +proof - + have lem: "g integrable_on s \ ((\k. integral s (f k)) \ integral s g) sequentially" if "\k. \x\s. 0 \ f k x" and "\k. (f k) integrable_on s" and "\k. \x\s. f k x \ f (Suc k) x" - and "\x\s. ((\k. f k x) ---> g x) sequentially" + and "\x\s. ((\k. f k x) \ g x) sequentially" and "bounded {integral s (f k)| k. True}" for f :: "nat \ 'n::euclidean_space \ real" and g s proof - @@ -9962,7 +9962,7 @@ done note fg=this[rule_format] - have "\i. ((\k. integral s (f k)) ---> i) sequentially" + have "\i. ((\k. integral s (f k)) \ i) sequentially" apply (rule bounded_increasing_convergent) apply (rule that(5)) apply rule @@ -10004,7 +10004,7 @@ apply (rule int) done have "\a b. (\x. if x \ s then g x else 0) integrable_on cbox a b \ - ((\k. integral (cbox a b) (\x. if x \ s then f k x else 0)) ---> + ((\k. integral (cbox a b) (\x. if x \ s then f k x else 0)) \ integral (cbox a b) (\x. if x \ s then g x else 0)) sequentially" proof (rule monotone_convergence_interval, safe, goal_cases) case 1 @@ -10140,7 +10140,7 @@ apply auto done note * = this[rule_format] - have "(\x. g x - f 0 x) integrable_on s \ ((\k. integral s (\x. f (Suc k) x - f 0 x)) ---> + have "(\x. g x - f 0 x) integrable_on s \ ((\k. integral s (\x. f (Suc k) x - f 0 x)) \ integral s (\x. g x - f 0 x)) sequentially" apply (rule lem) apply safe @@ -10225,9 +10225,9 @@ fixes f :: "nat \ 'n::euclidean_space \ real" assumes "\k. (f k) integrable_on s" and "\k. \x\s. f (Suc k) x \ f k x" - and "\x\s. ((\k. f k x) ---> g x) sequentially" + and "\x\s. ((\k. f k x) \ g x) sequentially" and "bounded {integral s (f k)| k. True}" - shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" + shows "g integrable_on s \ ((\k. integral s (f k)) \ integral s g) sequentially" proof - note assm = assms[rule_format] have *: "{integral s (\x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}" @@ -10240,7 +10240,7 @@ apply auto done have "(\x. - g x) integrable_on s \ - ((\k. integral s (\x. - f k x)) ---> integral s (\x. - g x)) sequentially" + ((\k. integral s (\x. - f k x)) \ integral s (\x. - g x)) sequentially" apply (rule monotone_convergence_increasing) apply safe apply (rule integrable_neg) @@ -11842,7 +11842,7 @@ obtains I J where "\n. (f n has_integral I n) (cbox a b)" "(g has_integral J) (cbox a b)" - "(I ---> J) F" + "(I \ J) F" proof - have fi[simp]: "f n integrable_on (cbox a b)" for n by (auto intro!: integrable_continuous assms) @@ -11858,7 +11858,7 @@ moreover - have "(I ---> J) F" + have "(I \ J) F" proof cases assume "content (cbox a b) = 0" hence "I = (\_. 0)" "J = 0" @@ -11906,9 +11906,9 @@ fixes f :: "nat \ 'n::euclidean_space \ real" assumes "\k. (f k) integrable_on s" "h integrable_on s" and "\k. \x \ s. norm (f k x) \ h x" - and "\x \ s. ((\k. f k x) ---> g x) sequentially" + and "\x \ s. ((\k. f k x) \ g x) sequentially" shows "g integrable_on s" - and "((\k. integral s (f k)) ---> integral s g) sequentially" + and "((\k. integral s (f k)) \ integral s g) sequentially" proof - have bdd_below[simp]: "\x P. x \ s \ bdd_below {f n x |n. P n}" proof (safe intro!: bdd_belowI) @@ -11922,7 +11922,7 @@ qed have "\m. (\x. Inf {f j x |j. m \ j}) integrable_on s \ - ((\k. integral s (\x. Inf {f j x |j. j \ {m..m + k}})) ---> + ((\k. integral s (\x. Inf {f j x |j. j \ {m..m + k}})) \ integral s (\x. Inf {f j x |j. m \ j}))sequentially" proof (rule monotone_convergence_decreasing, safe) fix m :: nat @@ -11962,7 +11962,7 @@ show "Inf {f j x |j. j \ {m..m + Suc k}} \ Inf {f j x |j. j \ {m..m + k}}" by (rule cInf_superset_mono) auto let ?S = "{f j x| j. m \ j}" - show "((\k. Inf {f j x |j. j \ {m..m + k}}) ---> Inf ?S) sequentially" + show "((\k. Inf {f j x |j. j \ {m..m + k}}) \ Inf ?S) sequentially" proof (rule LIMSEQ_I, goal_cases) case r: (1 r) @@ -11993,7 +11993,7 @@ note dec1 = conjunctD2[OF this] have "\m. (\x. Sup {f j x |j. m \ j}) integrable_on s \ - ((\k. integral s (\x. Sup {f j x |j. j \ {m..m + k}})) ---> + ((\k. integral s (\x. Sup {f j x |j. j \ {m..m + k}})) \ integral s (\x. Sup {f j x |j. m \ j})) sequentially" proof (rule monotone_convergence_increasing,safe) fix m :: nat @@ -12033,7 +12033,7 @@ show "Sup {f j x |j. j \ {m..m + Suc k}} \ Sup {f j x |j. j \ {m..m + k}}" by (rule cSup_subset_mono) auto let ?S = "{f j x| j. m \ j}" - show "((\k. Sup {f j x |j. j \ {m..m + k}}) ---> Sup ?S) sequentially" + show "((\k. Sup {f j x |j. j \ {m..m + k}}) \ Sup ?S) sequentially" proof (rule LIMSEQ_I, goal_cases) case r: (1 r) have "\y\?S. Sup ?S - r < y" @@ -12062,7 +12062,7 @@ note inc1 = conjunctD2[OF this] have "g integrable_on s \ - ((\k. integral s (\x. Inf {f j x |j. k \ j})) ---> integral s g) sequentially" + ((\k. integral s (\x. Inf {f j x |j. k \ j})) \ integral s g) sequentially" apply (rule monotone_convergence_increasing,safe) apply fact proof - @@ -12110,7 +12110,7 @@ note inc2 = conjunctD2[OF this] have "g integrable_on s \ - ((\k. integral s (\x. Sup {f j x |j. k \ j})) ---> integral s g) sequentially" + ((\k. integral s (\x. Sup {f j x |j. k \ j})) \ integral s g) sequentially" apply (rule monotone_convergence_decreasing,safe) apply fact proof - @@ -12135,7 +12135,7 @@ show "Sup {f j x |j. k \ j} \ Sup {f j x |j. Suc k \ j}" by (rule cSup_subset_mono) (auto simp: \x\s\) - show "((\k. Sup {f j x |j. k \ j}) ---> g x) sequentially" + show "((\k. Sup {f j x |j. k \ j}) \ g x) sequentially" proof (rule LIMSEQ_I, goal_cases) case r: (1 r) then have "0k. integral s (f k)) ---> integral s g) sequentially" + show "((\k. integral s (f k)) \ integral s g) sequentially" proof (rule LIMSEQ_I, goal_cases) case r: (1 r) from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def] diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Dec 30 11:21:54 2015 +0100 @@ -2881,8 +2881,8 @@ qed lemma tendsto_infnorm [tendsto_intros]: - assumes "(f ---> a) F" - shows "((\x. infnorm (f x)) ---> infnorm a) F" + assumes "(f \ a) F" + shows "((\x. infnorm (f x)) \ infnorm a) F" proof (rule tendsto_compose [OF LIM_I assms]) fix r :: real assume "r > 0" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Dec 30 11:21:54 2015 +0100 @@ -48,7 +48,7 @@ lemma Lim_within_open: fixes f :: "'a::topological_space \ 'b::topological_space" - shows "a \ S \ open S \ (f ---> l)(at a within S) \ (f ---> l)(at a)" + shows "a \ S \ open S \ (f \ l)(at a within S) \ (f \ l)(at a)" by (fact tendsto_within_open) lemma continuous_on_union: @@ -2293,48 +2293,48 @@ subsection \Limits\ lemma Lim: - "(f ---> l) net \ + "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" unfolding tendsto_iff trivial_limit_eq by auto text\Show that they yield usual definitions in the various cases.\ -lemma Lim_within_le: "(f ---> l)(at a within S) \ +lemma Lim_within_le: "(f \ l)(at a within S) \ (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at_le dist_nz) -lemma Lim_within: "(f ---> l) (at a within S) \ +lemma Lim_within: "(f \ l) (at a within S) \ (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at dist_nz) -lemma Lim_at: "(f ---> l) (at a) \ +lemma Lim_at: "(f \ l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at2) lemma Lim_at_infinity: - "(f ---> l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" + "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at_infinity) -lemma Lim_eventually: "eventually (\x. f x = l) net \ (f ---> l) net" +lemma Lim_eventually: "eventually (\x. f x = l) net \ (f \ l) net" by (rule topological_tendstoI, auto elim: eventually_mono) text\The expected monotonicity property.\ lemma Lim_Un: - assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)" - shows "(f ---> l) (at x within (S \ T))" + assumes "(f \ l) (at x within S)" "(f \ l) (at x within T)" + shows "(f \ l) (at x within (S \ T))" using assms unfolding at_within_union by (rule filterlim_sup) lemma Lim_Un_univ: - "(f ---> l) (at x within S) \ (f ---> l) (at x within T) \ - S \ T = UNIV \ (f ---> l) (at x)" + "(f \ l) (at x within S) \ (f \ l) (at x within T) \ + S \ T = UNIV \ (f \ l) (at x)" by (metis Lim_Un) text\Interrelations between restricted and unrestricted limits.\ lemma Lim_at_imp_Lim_at_within: - "(f ---> l) (at x) \ (f ---> l) (at x within S)" + "(f \ l) (at x) \ (f \ l) (at x within S)" by (metis order_refl filterlim_mono subset_UNIV at_le) lemma eventually_within_interior: @@ -2366,7 +2366,7 @@ lemma Lim_within_LIMSEQ: fixes a :: "'a::first_countable_topology" assumes "\S. (\n. S n \ a \ S n \ T) \ S \ a \ (\n. X (S n)) \ L" - shows "(X ---> L) (at a within T)" + shows "(X \ L) (at a within T)" using assms unfolding tendsto_def [where l=L] by (simp add: sequentially_imp_eventually_within) @@ -2375,7 +2375,7 @@ 'b::{linorder_topology, conditionally_complete_linorder}" assumes mono: "\a b. a \ I \ b \ I \ x < a \ a \ b \ f a \ f b" and bnd: "\a. a \ I \ x < a \ K \ f a" - shows "(f ---> Inf (f ` ({x<..} \ I))) (at x within ({x<..} \ I))" + shows "(f \ Inf (f ` ({x<..} \ I))) (at x within ({x<..} \ I))" proof (cases "{x<..} \ I = {}") case True then show ?thesis by simp @@ -2411,7 +2411,7 @@ lemma islimpt_sequential: fixes x :: "'a::first_countable_topology" - shows "x islimpt S \ (\f. (\n::nat. f n \ S - {x}) \ (f ---> x) sequentially)" + shows "x islimpt S \ (\f. (\n::nat. f n \ S - {x}) \ (f \ x) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs @@ -2456,13 +2456,13 @@ lemma Lim_null: fixes f :: "'a \ 'b::real_normed_vector" - shows "(f ---> l) net \ ((\x. f(x) - l) ---> 0) net" + shows "(f \ l) net \ ((\x. f(x) - l) \ 0) net" by (simp add: Lim dist_norm) lemma Lim_null_comparison: fixes f :: "'a \ 'b::real_normed_vector" - assumes "eventually (\x. norm (f x) \ g x) net" "(g ---> 0) net" - shows "(f ---> 0) net" + assumes "eventually (\x. norm (f x) \ g x) net" "(g \ 0) net" + shows "(f \ 0) net" using assms(2) proof (rule metric_tendsto_imp_tendsto) show "eventually (\x. dist (f x) 0 \ dist (g x) 0) net" @@ -2473,8 +2473,8 @@ fixes f :: "'a \ 'b::real_normed_vector" and g :: "'a \ 'c::real_normed_vector" assumes "eventually (\n. norm (f n) \ norm (g n)) net" - and "(g ---> 0) net" - shows "(f ---> 0) net" + and "(g \ 0) net" + shows "(f \ 0) net" using assms(1) tendsto_norm_zero [OF assms(2)] by (rule Lim_null_comparison) @@ -2483,7 +2483,7 @@ lemma Lim_in_closed_set: assumes "closed S" and "eventually (\x. f(x) \ S) net" - and "\ trivial_limit net" "(f ---> l) net" + and "\ trivial_limit net" "(f \ l) net" shows "l \ S" proof (rule ccontr) assume "l \ S" @@ -2501,21 +2501,21 @@ lemma Lim_dist_ubound: assumes "\(trivial_limit net)" - and "(f ---> l) net" + and "(f \ l) net" and "eventually (\x. dist a (f x) \ e) net" shows "dist a l \ e" using assms by (fast intro: tendsto_le tendsto_intros) lemma Lim_norm_ubound: fixes f :: "'a \ 'b::real_normed_vector" - assumes "\(trivial_limit net)" "(f ---> l) net" "eventually (\x. norm(f x) \ e) net" + assumes "\(trivial_limit net)" "(f \ l) net" "eventually (\x. norm(f x) \ e) net" shows "norm(l) \ e" using assms by (fast intro: tendsto_le tendsto_intros) lemma Lim_norm_lbound: fixes f :: "'a \ 'b::real_normed_vector" assumes "\ trivial_limit net" - and "(f ---> l) net" + and "(f \ l) net" and "eventually (\x. e \ norm (f x)) net" shows "e \ norm l" using assms by (fast intro: tendsto_le tendsto_intros) @@ -2523,25 +2523,25 @@ text\Limit under bilinear function\ lemma Lim_bilinear: - assumes "(f ---> l) net" - and "(g ---> m) net" + assumes "(f \ l) net" + and "(g \ m) net" and "bounded_bilinear h" - shows "((\x. h (f x) (g x)) ---> (h l m)) net" - using \bounded_bilinear h\ \(f ---> l) net\ \(g ---> m) net\ + shows "((\x. h (f x) (g x)) \ (h l m)) net" + using \bounded_bilinear h\ \(f \ l) net\ \(g \ m) net\ by (rule bounded_bilinear.tendsto) text\These are special for limits out of the same vector space.\ -lemma Lim_within_id: "(id ---> a) (at a within s)" +lemma Lim_within_id: "(id \ a) (at a within s)" unfolding id_def by (rule tendsto_ident_at) -lemma Lim_at_id: "(id ---> a) (at a)" +lemma Lim_at_id: "(id \ a) (at a)" unfolding id_def by (rule tendsto_ident_at) lemma Lim_at_zero: fixes a :: "'a::real_normed_vector" and l :: "'b::topological_space" - shows "(f ---> l) (at a) \ ((\x. f(a + x)) ---> l) (at 0)" + shows "(f \ l) (at a) \ ((\x. f(a + x)) \ l) (at 0)" using LIM_offset_zero LIM_offset_zero_cancel .. text\It's also sometimes useful to extract the limit point from the filter.\ @@ -2558,7 +2558,7 @@ using netlimit_within [of a UNIV] by simp lemma lim_within_interior: - "x \ interior S \ (f ---> l) (at x within S) \ (f ---> l) (at x)" + "x \ interior S \ (f \ l) (at x within S) \ (f \ l) (at x)" by (metis at_within_interior) lemma netlimit_within_interior: @@ -2587,7 +2587,7 @@ lemma closure_sequential: fixes l :: "'a::first_countable_topology" - shows "l \ closure S \ (\x. (\n. x n \ S) \ (x ---> l) sequentially)" + shows "l \ closure S \ (\x. (\n. x n \ S) \ (x \ l) sequentially)" (is "?lhs = ?rhs") proof assume "?lhs" @@ -2610,7 +2610,7 @@ lemma closed_sequential_limits: fixes S :: "'a::first_countable_topology set" - shows "closed S \ (\x l. (\n. x n \ S) \ (x ---> l) sequentially \ l \ S)" + shows "closed S \ (\x l. (\n. x n \ S) \ (x \ l) sequentially \ l \ S)" by (metis closure_sequential closure_subset_eq subset_iff) lemma closure_approachable: @@ -2795,8 +2795,8 @@ qed lemma tendsto_infdist [tendsto_intros]: - assumes f: "(f ---> l) F" - shows "((\x. infdist (f x) A) ---> infdist l A) F" + assumes f: "(f \ l) F" + shows "((\x. infdist (f x) A) \ infdist l A) F" proof (rule tendstoI) fix e ::real assume "e > 0" @@ -2820,13 +2820,13 @@ using assms by (rule eventually_sequentially_seg [THEN iffD2]) lemma seq_offset_neg: (* TODO: move to Topological_Spaces.thy *) - "(f ---> l) sequentially \ ((\i. f(i - k)) ---> l) sequentially" + "(f \ l) sequentially \ ((\i. f(i - k)) \ l) sequentially" apply (erule filterlim_compose) apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially) apply arith done -lemma seq_harmonic: "((\n. inverse (real n)) ---> 0) sequentially" +lemma seq_harmonic: "((\n. inverse (real n)) \ 0) sequentially" using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) (* TODO: move to Limits.thy *) subsection \More properties of closed balls\ @@ -3224,7 +3224,7 @@ { fix y assume "y \ closure S" - then obtain f where f: "\n. f n \ S" "(f ---> y) sequentially" + then obtain f where f: "\n. f n \ S" "(f \ y) sequentially" unfolding closure_sequential by auto have "\n. f n \ S \ dist x (f n) \ a" using a by simp then have "eventually (\n. dist x (f n) \ a) sequentially" @@ -3567,7 +3567,7 @@ lemma sequence_infinite_lemma: fixes f :: "nat \ 'a::t1_space" assumes "\n. f n \ l" - and "(f ---> l) sequentially" + and "(f \ l) sequentially" shows "infinite (range f)" proof assume "finite (range f)" @@ -3664,7 +3664,7 @@ lemma sequence_unique_limpt: fixes f :: "nat \ 'a::t2_space" - assumes "(f ---> l) sequentially" + assumes "(f \ l) sequentially" and "l' islimpt (range f)" shows "l' = l" proof (rule ccontr) @@ -3701,7 +3701,7 @@ proof - { fix x l - assume as: "\n::nat. x n \ s" "(x ---> l) sequentially" + assume as: "\n::nat. x n \ s" "(x \ l) sequentially" then have "l \ s" proof (cases "\n. x n \ l") case False @@ -3974,16 +3974,16 @@ definition seq_compact :: "'a::topological_space set \ bool" where "seq_compact S \ - (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ ((f \ r) ---> l) sequentially))" + (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ ((f \ r) \ l) sequentially))" lemma seq_compactI: - assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f \ r) ---> l) sequentially" + assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f \ r) \ l) sequentially" shows "seq_compact S" unfolding seq_compact_def using assms by fast lemma seq_compactE: assumes "seq_compact S" "\n. f n \ S" - obtains l r where "l \ S" "subseq r" "((f \ r) ---> l) sequentially" + obtains l r where "l \ S" "subseq r" "((f \ r) \ l) sequentially" using assms unfolding seq_compact_def by fast lemma closed_sequentially: (* TODO: move upwards *) @@ -4184,7 +4184,7 @@ { fix f :: "nat \ 'a" assume f: "\n. f n \ s" - have "\l\s. \r. subseq r \ ((f \ r) ---> l) sequentially" + have "\l\s. \r. subseq r \ ((f \ r) \ l) sequentially" proof (cases "finite (range f)") case True obtain l where "infinite {n. f n = f l}" @@ -4200,9 +4200,9 @@ with f assms have "\x\s. \U. x\U \ open U \ infinite (U \ range f)" by auto then obtain l where "l \ s" "\U. l\U \ open U \ infinite (U \ range f)" .. - from this(2) have "\r. subseq r \ ((f \ r) ---> l) sequentially" + from this(2) have "\r. subseq r \ ((f \ r) \ l) sequentially" using acc_point_range_imp_convergent_subsequence[of l f] by auto - with \l \ s\ show "\l\s. \r. subseq r \ ((f \ r) ---> l) sequentially" .. + with \l \ s\ show "\l\s. \r. subseq r \ ((f \ r) \ l) sequentially" .. qed } then show ?thesis @@ -4261,7 +4261,7 @@ qed simp then obtain x where "\n::nat. x n \ s" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)" by blast - then obtain l r where "l \ s" and r:"subseq r" and "((x \ r) ---> l) sequentially" + then obtain l r where "l \ s" and r:"subseq r" and "((x \ r) \ l) sequentially" using assms by (metis seq_compact_def) from this(3) have "Cauchy (x \ r)" using LIMSEQ_imp_Cauchy by auto @@ -4358,7 +4358,7 @@ class heine_borel = metric_space + assumes bounded_imp_convergent_subsequence: - "bounded (range f) \ \l r. subseq r \ ((f \ r) ---> l) sequentially" + "bounded (range f) \ \l r. subseq r \ ((f \ r) \ l) sequentially" lemma bounded_closed_imp_seq_compact: fixes s::"'a::heine_borel set" @@ -4370,13 +4370,13 @@ assume f: "\n. f n \ s" with \bounded s\ have "bounded (range f)" by (auto intro: bounded_subset) - obtain l r where r: "subseq r" and l: "((f \ r) ---> l) sequentially" + obtain l r where r: "subseq r" and l: "((f \ r) \ l) sequentially" using bounded_imp_convergent_subsequence [OF \bounded (range f)\] by auto from f have fr: "\n. (f \ r) n \ s" by simp have "l \ s" using \closed s\ fr l by (rule closed_sequentially) - show "\l\s. \r. subseq r \ ((f \ r) ---> l) sequentially" + show "\l\s. \r. subseq r \ ((f \ r) \ l) sequentially" using \l \ s\ r l by blast qed @@ -4451,7 +4451,7 @@ by simp have "bounded (range (\i. f (r1 i) \ k))" by (metis (lifting) bounded_subset f' image_subsetI s') - then obtain l2 r2 where r2:"subseq r2" and lr2:"((\i. f (r1 (r2 i)) \ k) ---> l2) sequentially" + then obtain l2 r2 where r2:"subseq r2" and lr2:"((\i. f (r1 (r2 i)) \ k) \ l2) sequentially" using bounded_imp_convergent_subsequence[of "\i. f (r1 i) \ k"] by (auto simp: o_def) def r \ "r1 \ r2" @@ -4509,9 +4509,9 @@ ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" by (rule eventually_mono) } - then have *: "((f \ r) ---> l) sequentially" + then have *: "((f \ r) \ l) sequentially" unfolding o_def tendsto_iff by simp - with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" + with r show "\l r. subseq r \ ((f \ r) \ l) sequentially" by auto qed @@ -4535,16 +4535,16 @@ using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast from f have s2: "bounded (range (snd \ f \ r1))" by (auto simp add: image_comp intro: bounded_snd bounded_subset) - obtain l2 r2 where r2: "subseq r2" and l2: "((\n. snd (f (r1 (r2 n)))) ---> l2) sequentially" + obtain l2 r2 where r2: "subseq r2" and l2: "((\n. snd (f (r1 (r2 n)))) \ l2) sequentially" using bounded_imp_convergent_subsequence [OF s2] unfolding o_def by fast - have l1': "((\n. fst (f (r1 (r2 n)))) ---> l1) sequentially" + have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially" using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def . - have l: "((f \ (r1 \ r2)) ---> (l1, l2)) sequentially" + have l: "((f \ (r1 \ r2)) \ (l1, l2)) sequentially" using tendsto_Pair [OF l1' l2] unfolding o_def by simp have r: "subseq (r1 \ r2)" using r1 r2 unfolding subseq_def by simp - show "\l r. subseq r \ ((f \ r) ---> l) sequentially" + show "\l r. subseq r \ ((f \ r) \ l) sequentially" using l r by fast qed @@ -4601,7 +4601,7 @@ } then have "\N. \n\N. dist (f n) l < e" by blast } - then have "\l\s. (f ---> l) sequentially" using \l\s\ + then have "\l\s. (f \ l) sequentially" using \l\s\ unfolding lim_sequentially by auto } then show ?thesis unfolding complete_def by auto @@ -4777,7 +4777,7 @@ by (rule compact_imp_complete) moreover have "\n. f n \ closure (range f)" using closure_subset [of "range f"] by auto - ultimately have "\l\closure (range f). (f ---> l) sequentially" + ultimately have "\l\closure (range f). (f \ l) sequentially" using \Cauchy f\ unfolding complete_def by auto then show "convergent f" unfolding convergent_def by auto @@ -4840,12 +4840,12 @@ lemma convergent_eq_cauchy: fixes s :: "nat \ 'a::complete_space" - shows "(\l. (s ---> l) sequentially) \ Cauchy s" + shows "(\l. (s \ l) sequentially) \ Cauchy s" unfolding Cauchy_convergent_iff convergent_def .. lemma convergent_imp_bounded: fixes s :: "nat \ 'a::metric_space" - shows "(s ---> l) sequentially \ bounded (range s)" + shows "(s \ l) sequentially \ bounded (range s)" by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) lemma compact_cball[simp]: @@ -4940,7 +4940,7 @@ } then have "Cauchy t" unfolding cauchy_def by auto - then obtain l where l:"(t ---> l) sequentially" + then obtain l where l:"(t \ l) sequentially" using complete_UNIV unfolding complete_def by auto { fix n :: nat @@ -5035,9 +5035,9 @@ apply (erule_tac x=e in allE) apply auto done - then obtain l where l: "\x. P x \ ((\n. s n x) ---> l x) sequentially" + then obtain l where l: "\x. P x \ ((\n. s n x) \ l x) sequentially" unfolding convergent_eq_cauchy[symmetric] - using choice[of "\x l. P x \ ((\n. s n x) ---> l) sequentially"] + using choice[of "\x l. P x \ ((\n. s n x) \ l) sequentially"] by auto { fix e :: real @@ -5230,7 +5230,7 @@ "continuous (at x) f \ continuous (at x within s) f" unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto -lemma Lim_trivial_limit: "trivial_limit net \ (f ---> l) net" +lemma Lim_trivial_limit: "trivial_limit net \ (f \ l) net" by simp lemmas continuous_on = continuous_on_def \ "legacy theorem name" @@ -5253,8 +5253,8 @@ lemma continuous_within_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a within s) f \ - (\x. (\n::nat. x n \ s) \ (x ---> a) sequentially - \ ((f \ x) ---> f a) sequentially)" + (\x. (\n::nat. x n \ s) \ (x \ a) sequentially + \ ((f \ x) \ f a) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs @@ -5286,14 +5286,14 @@ lemma continuous_at_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a) f \ - (\x. (x ---> a) sequentially --> ((f \ x) ---> f a) sequentially)" + (\x. (x \ a) sequentially --> ((f \ x) \ f a) sequentially)" using continuous_within_sequentially[of a UNIV f] by simp lemma continuous_on_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous_on s f \ - (\x. \a \ s. (\n. x(n) \ s) \ (x ---> a) sequentially - --> ((f \ x) ---> f a) sequentially)" + (\x. \a \ s. (\n. x(n) \ s) \ (x \ a) sequentially + --> ((f \ x) \ f a) sequentially)" (is "?lhs = ?rhs") proof assume ?rhs @@ -5311,15 +5311,15 @@ lemma uniformly_continuous_on_sequentially: "uniformly_continuous_on s f \ (\x y. (\n. x n \ s) \ (\n. y n \ s) \ - ((\n. dist (x n) (y n)) ---> 0) sequentially - \ ((\n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs") + ((\n. dist (x n) (y n)) \ 0) sequentially + \ ((\n. dist (f(x n)) (f(y n))) \ 0) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs { fix x y assume x: "\n. x n \ s" and y: "\n. y n \ s" - and xy: "((\n. dist (x n) (y n)) ---> 0) sequentially" + and xy: "((\n. dist (x n) (y n)) \ 0) sequentially" { fix e :: real assume "e > 0" @@ -5340,7 +5340,7 @@ then have "\N. \n\N. dist (f (x n)) (f (y n)) < e" by auto } - then have "((\n. dist (f(x n)) (f(y n))) ---> 0) sequentially" + then have "((\n. dist (f(x n)) (f(y n))) \ 0) sequentially" unfolding lim_sequentially and dist_real_def by auto } then show ?rhs by auto @@ -5390,14 +5390,14 @@ lemma continuous_on_tendsto_compose: assumes f_cont: "continuous_on s f" - assumes g: "(g ---> l) F" + assumes g: "(g \ l) F" assumes l: "l \ s" assumes ev: "\\<^sub>F x in F. g x \ s" - shows "((\x. f (g x)) ---> f l) F" + shows "((\x. f (g x)) \ f l) F" proof - - from f_cont have f: "(f ---> f l) (at l within s)" + from f_cont have f: "(f \ f l) (at l within s)" by (auto simp: l continuous_on) - have i: "((\x. if g x = l then f l else f (g x)) ---> f l) F" + have i: "((\x. if g x = l then f l else f (g x)) \ f l) F" by (rule filterlim_If) (auto intro!: filterlim_compose[OF f] eventually_conj tendsto_mono[OF _ g] simp: filterlim_at eventually_inf_principal eventually_mono[OF ev]) @@ -5422,7 +5422,7 @@ using assms(3) by auto have "f x = g x" using assms(1,2,3) by auto - then show "(f ---> g x) (at x within s)" + then show "(f \ g x) (at x within s)" using assms(4) unfolding continuous_within by simp qed @@ -5822,7 +5822,7 @@ proof - obtain U where "open U" and "f x \ U" and "a \ U" using t1_space [OF \f x \ a\] by fast - have "(f ---> f x) (at x within s)" + have "(f \ f x) (at x within s)" using assms(1) by (simp add: continuous_within) then have "eventually (\y. f y \ U) (at x within s)" using \open U\ and \f x \ U\ @@ -6015,10 +6015,10 @@ lemma linear_lim_0: assumes "bounded_linear f" - shows "(f ---> 0) (at (0))" + shows "(f \ 0) (at (0))" proof - interpret f: bounded_linear f by fact - have "(f ---> f 0) (at 0)" + have "(f \ f 0) (at 0)" using tendsto_ident_at by (rule f.tendsto) then show ?thesis unfolding f.zero . qed @@ -6267,7 +6267,7 @@ { fix x assume "x\s" - have "(dist a ---> dist a x) (at x within s)" + have "(dist a \ dist a x) (at x within s)" by (intro tendsto_dist tendsto_const tendsto_ident_at) } then show "continuous_on s (dist a)" @@ -6570,12 +6570,12 @@ let ?S = "{x + y |x y. x \ s \ y \ t}" { fix x l - assume as: "\n. x n \ ?S" "(x ---> l) sequentially" + assume as: "\n. x n \ ?S" "(x \ l) sequentially" from as(1) obtain f where f: "\n. x n = fst (f n) + snd (f n)" "\n. fst (f n) \ s" "\n. snd (f n) \ t" using choice[of "\n y. x n = (fst y) + (snd y) \ fst y \ s \ snd y \ t"] by auto - obtain l' r where "l'\s" and r: "subseq r" and lr: "(((\n. fst (f n)) \ r) ---> l') sequentially" + 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" + have "((\n. snd (f (r n))) \ l - l') sequentially" using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) unfolding o_def by auto @@ -6906,7 +6906,7 @@ lemma Lim_component_le: fixes f :: "'a \ 'b::euclidean_space" - assumes "(f ---> l) net" + assumes "(f \ l) net" and "\ (trivial_limit net)" and "eventually (\x. f(x)\i \ b) net" shows "l\i \ b" @@ -6914,7 +6914,7 @@ lemma Lim_component_ge: fixes f :: "'a \ 'b::euclidean_space" - assumes "(f ---> l) net" + assumes "(f \ l) net" and "\ (trivial_limit net)" and "eventually (\x. b \ (f x)\i) net" shows "b \ l\i" @@ -6922,7 +6922,7 @@ lemma Lim_component_eq: fixes f :: "'a \ 'b::euclidean_space" - assumes net: "(f ---> l) net" "\ trivial_limit net" + assumes net: "(f \ l) net" "\ trivial_limit net" and ev:"eventually (\x. f(x)\i = b) net" shows "l\i = b" using ev[unfolded order_eq_iff eventually_conj_iff] @@ -6939,13 +6939,13 @@ by (auto elim!: eventually_rev_mp) lemma Lim_within_union: - "(f ---> l) (at x within (s \ t)) \ - (f ---> l) (at x within s) \ (f ---> l) (at x within t)" + "(f \ l) (at x within (s \ t)) \ + (f \ l) (at x within s) \ (f \ l) (at x within t)" unfolding tendsto_def by (auto simp add: eventually_within_Un) lemma Lim_topological: - "(f ---> l) net \ + "(f \ l) net \ trivial_limit net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" unfolding tendsto_def trivial_limit_eq by auto @@ -7266,7 +7266,7 @@ } moreover { - assume "\ (f ---> x) sequentially" + assume "\ (f \ x) sequentially" { fix e :: real assume "e > 0" @@ -7281,9 +7281,9 @@ by (auto intro!: that le_less_trans [OF _ N]) then have "\N::nat. \n\N. inverse (real n + 1) < e" by auto } - then have "((\n. inverse (real n + 1)) ---> 0) sequentially" + then have "((\n. inverse (real n + 1)) \ 0) sequentially" unfolding lim_sequentially by(auto simp add: dist_norm) - then have "(f ---> x) sequentially" + then have "(f \ x) sequentially" unfolding f_def 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 tendsto_scaleR [OF _ tendsto_const, of "\n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] @@ -7815,11 +7815,11 @@ then have "f \ x = g" unfolding fun_eq_iff by auto - then obtain l where "l\s" and l:"(x ---> l) sequentially" + then obtain l where "l\s" and l:"(x \ l) sequentially" using cs[unfolded complete_def, THEN spec[where x="x"]] using cauchy_isometric[OF \0 < e\ s f normf] and cfg and x(1) by auto - then have "\l\f ` s. (g ---> l) sequentially" + then have "\l\f ` s. (g \ l) sequentially" using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l] unfolding \f \ x = g\ by auto @@ -8186,7 +8186,7 @@ } then have "Cauchy z" unfolding cauchy_def by auto - then obtain x where "x\s" and x:"(z ---> x) sequentially" + then obtain x where "x\s" and x:"(z \ x) sequentially" using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto def e \ "dist (f x) x" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Multivariate_Analysis/Uniform_Limit.thy --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Wed Dec 30 11:21:54 2015 +0100 @@ -54,11 +54,11 @@ by (fastforce dest: spec[where x = "e / 2" for e]) lemma swap_uniform_limit: - assumes f: "\\<^sub>F n in F. (f n ---> g n) (at x within S)" - assumes g: "(g ---> l) F" + assumes f: "\\<^sub>F n in F. (f n \ g n) (at x within S)" + assumes g: "(g \ l) F" assumes uc: "uniform_limit S f h F" assumes "\trivial_limit F" - shows "(h ---> l) (at x within S)" + shows "(h \ l) (at x within S)" proof (rule tendstoI) fix e :: real def e' \ "e/3" @@ -101,7 +101,7 @@ tendsto_uniform_limitI: assumes "uniform_limit S f l F" assumes "x \ S" - shows "((\y. f y x) ---> l x) F" + shows "((\y. f y x) \ l x) F" using assms by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD) @@ -113,10 +113,10 @@ unfolding continuous_on_def proof safe fix x assume "x \ A" - then have "\\<^sub>F n in F. (f n ---> f n x) (at x within A)" "((\n. f n x) ---> l x) F" + then have "\\<^sub>F n in F. (f n \ f n x) (at x within A)" "((\n. f n x) \ l x) F" using c ul by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI) - then show "(l ---> l x) (at x within A)" + then show "(l \ l x) (at x within A)" by (rule swap_uniform_limit) fact+ qed diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/NthRoot.thy Wed Dec 30 11:21:54 2015 +0100 @@ -268,7 +268,7 @@ qed (simp add: root_def[abs_def]) lemma tendsto_real_root[tendsto_intros]: - "(f ---> x) F \ ((\x. root n (f x)) ---> root n x) F" + "(f \ x) F \ ((\x. root n (f x)) \ root n x) F" using isCont_tendsto_compose[OF isCont_real_root, of f x F] . lemma continuous_real_root[continuous_intros]: @@ -457,7 +457,7 @@ unfolding sqrt_def by (rule isCont_real_root) lemma tendsto_real_sqrt[tendsto_intros]: - "(f ---> x) F \ ((\x. sqrt (f x)) ---> sqrt x) F" + "(f \ x) F \ ((\x. sqrt (f x)) \ sqrt x) F" unfolding sqrt_def by (rule tendsto_real_root) lemma continuous_real_sqrt[continuous_intros]: diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Probability/Bochner_Integration.thy Wed Dec 30 11:21:54 2015 +0100 @@ -1524,11 +1524,11 @@ fixes s :: "real \ 'a \ 'b::{banach, second_countable_topology}" and w :: "'a \ real" and f :: "'a \ 'b" and M assumes "f \ borel_measurable M" "\t. s t \ borel_measurable M" "integrable M w" - assumes lim: "AE x in M. ((\i. s i x) ---> f x) at_top" + assumes lim: "AE x in M. ((\i. s i x) \ f x) at_top" assumes bound: "\\<^sub>F i in at_top. AE x in M. norm (s i x) \ w x" begin -lemma integral_dominated_convergence_at_top: "((\t. integral\<^sup>L M (s t)) ---> integral\<^sup>L M f) at_top" +lemma integral_dominated_convergence_at_top: "((\t. integral\<^sup>L M (s t)) \ integral\<^sup>L M f) at_top" proof (rule tendsto_at_topI_sequentially) fix X :: "nat \ real" assume X: "filterlim X at_top sequentially" from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound] @@ -1542,7 +1542,7 @@ show "AE x in M. (\n. s (X (n + N)) x) \ f x" using lim proof eventually_elim - fix x assume "((\i. s i x) ---> f x) at_top" + fix x assume "((\i. s i x) \ f x) at_top" then show "(\n. s (X (n + N)) x) \ f x" by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X]) qed @@ -1560,7 +1560,7 @@ show "AE x in M. (\i. s (N + real i) x) \ f x" using lim proof eventually_elim - fix x assume "((\i. s i x) ---> f x) at_top" + fix x assume "((\i. s i x) \ f x) at_top" then show "(\n. s (N + n) x) \ f x" by (rule filterlim_compose) (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially) @@ -2459,7 +2459,7 @@ lemma tendsto_integral_at_top: fixes f :: "real \ 'a::{banach, second_countable_topology}" assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f" - shows "((\y. \ x. indicator {.. y} x *\<^sub>R f x \M) ---> \ x. f x \M) at_top" + shows "((\y. \ x. indicator {.. y} x *\<^sub>R f x \M) \ \ x. f x \M) at_top" proof (rule tendsto_at_topI_sequentially) fix X :: "nat \ real" assume "filterlim X at_top sequentially" show "(\n. \x. indicator {..X n} x *\<^sub>R f x \M) \ integral\<^sup>L M f" @@ -2486,7 +2486,7 @@ assumes nonneg: "AE x in M. 0 \ f x" assumes borel: "f \ borel_measurable borel" assumes int: "\y. integrable M (\x. f x * indicator {.. y} x)" - assumes conv: "((\y. \ x. f x * indicator {.. y} x \M) ---> x) at_top" + assumes conv: "((\y. \ x. f x * indicator {.. y} x \M) \ x) at_top" shows has_bochner_integral_monotone_convergence_at_top: "has_bochner_integral M f x" and integrable_monotone_convergence_at_top: "integrable M f" and integral_monotone_convergence_at_top:"integral\<^sup>L M f = x" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Distributions.thy --- a/src/HOL/Probability/Distributions.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Probability/Distributions.thy Wed Dec 30 11:21:54 2015 +0100 @@ -123,7 +123,7 @@ apply (metis nat_ceiling_le_eq) done - have "((\x::real. (1 - (\n\k. (x ^ n / exp x) / (fact n))) * fact k) ---> + have "((\x::real. (1 - (\n\k. (x ^ n / exp x) / (fact n))) * fact k) \ (1 - (\n\k. 0 / (fact n))) * fact k) at_top" by (intro tendsto_intros tendsto_power_div_exp_0) simp then show "?X \ real_of_nat (fact k)" @@ -865,20 +865,20 @@ proof (intro nn_integral_cong ereal_right_mult_cong) fix s :: real show "?pI (\x. ?ff x s) = ereal (1 / (2 * (1 + s\<^sup>2)))" proof (subst nn_integral_FTC_atLeast) - have "((\a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) ---> (- (0 / (2 + 2 * s\<^sup>2)))) at_top" + have "((\a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) \ (- (0 / (2 + 2 * s\<^sup>2)))) at_top" apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top]) apply (subst mult.commute) apply (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] simp: add_pos_nonneg power2_eq_square add_nonneg_eq_0_iff) done - then show "((\a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) ---> 0) at_top" + then show "((\a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) \ 0) at_top" by (simp add: field_simps) qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff) qed rule also have "... = ereal (pi / 4)" proof (subst nn_integral_FTC_atLeast) - show "((\a. arctan a / 2) ---> (pi / 2) / 2 ) at_top" + show "((\a. arctan a / 2) \ (pi / 2) / 2 ) at_top" by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top) qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square) finally have "?pI ?gauss^2 = pi / 4" @@ -904,12 +904,12 @@ (auto simp: ac_simps times_ereal.simps(1)[symmetric] ereal_indicator simp del: times_ereal.simps) also have "\ = ereal (0 - (- exp (- 0\<^sup>2) / 2))" proof (rule nn_integral_FTC_atLeast) - have "((\x::real. - exp (- x\<^sup>2) / 2) ---> - 0 / 2) at_top" + have "((\x::real. - exp (- x\<^sup>2) / 2) \ - 0 / 2) at_top" by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top] filterlim_pow_at_top filterlim_ident) auto - then show "((\a::real. - exp (- a\<^sup>2) / 2) ---> 0) at_top" + then show "((\a::real. - exp (- a\<^sup>2) / 2) \ 0) at_top" by simp qed (auto intro!: derivative_eq_intros) also have "\ = ereal (1 / 2)" @@ -934,13 +934,13 @@ have "2 \ (0::real)" by linarith let ?f = "\b. \x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \lborel" - have "((\b. (k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \lborel) - ?M (k + 1) b / 2) ---> + have "((\b. (k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \lborel) - ?M (k + 1) b / 2) \ (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel) - 0 / 2) at_top" (is ?tendsto) proof (intro tendsto_intros \2 \ 0\ tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros]) - show "(?M (k + 1) ---> 0) at_top" + show "(?M (k + 1) \ 0) at_top" proof cases assume "even k" - have "((\x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top" + have "((\x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) \ 0 * 0) at_top" by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident) auto @@ -949,7 +949,7 @@ finally show ?thesis by simp next assume "odd k" - have "((\x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top" + have "((\x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) \ 0) at_top" by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top) auto @@ -958,7 +958,7 @@ finally show ?thesis by simp qed qed - also have "?tendsto \ ((?f ---> (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel) - 0 / 2) at_top)" + also have "?tendsto \ ((?f \ (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel) - 0 / 2) at_top)" proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI) fix b :: real assume b: "0 \ b" have "Suc k * (\x. indicator {0..b} x *\<^sub>R ?M k x \lborel) = (\x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \lborel)" @@ -977,7 +977,7 @@ then show "(k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b" by (simp add: field_simps atLeastAtMost_def indicator_inter_arith) qed - finally have int_M_at_top: "((?f ---> (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel)) at_top)" + finally have int_M_at_top: "((?f \ (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel)) at_top)" by simp have "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R ?M (k + 2) x) ((k + 1) / 2 * I)" @@ -988,7 +988,7 @@ by rule (simp split: split_indicator) show "integrable lborel (\x. indicator {0..} x *\<^sub>R (?M (k + 2) x) * indicator {..y} x::real)" unfolding * by (rule borel_integrable_compact) (auto intro!: continuous_intros) - show "((?f ---> (k + 1) / 2 * I) at_top)" + show "((?f \ (k + 1) / 2 * I) at_top)" using int_M_at_top has_bochner_integral_integral_eq[OF Mk] by simp qed (auto split: split_indicator) } note step = this diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Fin_Map.thy --- a/src/HOL/Probability/Fin_Map.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Probability/Fin_Map.thy Wed Dec 30 11:21:54 2015 +0100 @@ -187,7 +187,7 @@ using open_restricted_space[of "\x. \ P x"] unfolding closed_def by (rule back_subst) auto -lemma tendsto_proj: "((\x. x) ---> a) F \ ((\x. (x)\<^sub>F i) ---> (a)\<^sub>F i) F" +lemma tendsto_proj: "((\x. x) \ a) F \ ((\x. (x)\<^sub>F i) \ (a)\<^sub>F i) F" unfolding tendsto_def proof safe fix S::"'b set" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Interval_Integral.thy --- a/src/HOL/Probability/Interval_Integral.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Probability/Interval_Integral.thy Wed Dec 30 11:21:54 2015 +0100 @@ -622,8 +622,8 @@ assumes F: "\x. a < ereal x \ ereal x < b \ DERIV F x :> f x" assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" assumes f_nonneg: "AE x in lborel. a < ereal x \ ereal x < b \ 0 \ f x" - assumes A: "((F \ real_of_ereal) ---> A) (at_right a)" - assumes B: "((F \ real_of_ereal) ---> B) (at_left b)" + assumes A: "((F \ real_of_ereal) \ A) (at_right a)" + assumes B: "((F \ real_of_ereal) \ B) (at_left b)" shows "set_integrable lborel (einterval a b) f" "(LBINT x=a..b. f x) = B - A" @@ -669,8 +669,8 @@ assumes F: "\x. a < ereal x \ ereal x < b \ (F has_vector_derivative f x) (at x)" assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" assumes f_integrable: "set_integrable lborel (einterval a b) f" - assumes A: "((F \ real_of_ereal) ---> A) (at_right a)" - assumes B: "((F \ real_of_ereal) ---> B) (at_left b)" + assumes A: "((F \ real_of_ereal) \ A) (at_right a)" + assumes B: "((F \ real_of_ereal) \ B) (at_left b)" shows "(LBINT x=a..b. f x) = B - A" proof - from einterval_Icc_approximation[OF \a < b\] guess u l . note approx = this @@ -834,8 +834,8 @@ and contf: "\x. a < ereal x \ ereal x < b \ isCont f (g x)" and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" and g'_nonneg: "\x. a \ ereal x \ ereal x \ b \ 0 \ g' x" - and A: "((ereal \ g \ real_of_ereal) ---> A) (at_right a)" - and B: "((ereal \ g \ real_of_ereal) ---> B) (at_left b)" + and A: "((ereal \ g \ real_of_ereal) \ A) (at_right a)" + and B: "((ereal \ g \ real_of_ereal) \ B) (at_left b)" and integrable: "set_integrable lborel (einterval a b) (\x. g' x *\<^sub>R f (g x))" and integrable2: "set_integrable lborel (einterval A B) (\x. f x)" shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" @@ -935,8 +935,8 @@ and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" and f_nonneg: "\x. a < ereal x \ ereal x < b \ 0 \ f (g x)" (* TODO: make this AE? *) and g'_nonneg: "\x. a \ ereal x \ ereal x \ b \ 0 \ g' x" - and A: "((ereal \ g \ real_of_ereal) ---> A) (at_right a)" - and B: "((ereal \ g \ real_of_ereal) ---> B) (at_left b)" + and A: "((ereal \ g \ real_of_ereal) \ A) (at_right a)" + and B: "((ereal \ g \ real_of_ereal) \ B) (at_left b)" and integrable_fg: "set_integrable lborel (einterval a b) (\x. f (g x) * g' x)" shows "set_integrable lborel (einterval A B) f" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Lebesgue_Integral_Substitution.thy --- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy Wed Dec 30 11:21:54 2015 +0100 @@ -148,7 +148,7 @@ shows "D \ 0" proof (rule tendsto_le_const) let ?A' = "(\y. y - x) ` interior A" - from deriv show "((\h. (f (x + h) - f x) / h) ---> D) (at 0)" + from deriv show "((\h. (f (x + h) - f x) / h) \ D) (at 0)" by (simp add: field_has_derivative_at has_field_derivative_def) from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset) diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Dec 30 11:21:54 2015 +0100 @@ -322,7 +322,7 @@ note * = this let ?F = "interval_measure F" - show "((\a. F b - F a) ---> emeasure ?F {a..b}) (at_left a)" + show "((\a. F b - F a) \ emeasure ?F {a..b}) (at_left a)" proof (rule tendsto_at_left_sequentially) show "a - 1 < a" by simp fix X assume "\n. X n < a" "incseq X" "X \ a" @@ -344,7 +344,7 @@ using \\n. X n < a\ \a \ b\ by (subst *) (auto intro: less_imp_le less_le_trans) finally show "(\n. F b - F (X n)) \ emeasure ?F {a..b}" . qed - show "((\a. ereal (F b - F a)) ---> F b - F a) (at_left a)" + show "((\a. ereal (F b - F a)) \ F b - F a) (at_left a)" using cont_F by (intro lim_ereal[THEN iffD2] tendsto_intros ) (auto simp: continuous_on_def intro: tendsto_within_subset) @@ -1244,7 +1244,7 @@ assumes f_borel: "f \ borel_measurable borel" assumes f: "\x. a \ x \ DERIV F x :> f x" assumes nonneg: "\x. a \ x \ 0 \ f x" - assumes lim: "(F ---> T) at_top" + assumes lim: "(F \ T) at_top" shows "(\\<^sup>+x. ereal (f x) * indicator {a ..} x \lborel) = T - F a" proof - let ?f = "\(i::nat) (x::real). ereal (f x) * indicator {a..a + real i} x" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Probability/Projective_Limit.thy --- a/src/HOL/Probability/Projective_Limit.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Probability/Projective_Limit.thy Wed Dec 30 11:21:54 2015 +0100 @@ -48,7 +48,7 @@ lemma compactE': fixes S :: "'a :: metric_space set" assumes "compact S" "\n\m. f n \ S" - obtains l r where "l \ S" "subseq r" "((f \ r) ---> l) sequentially" + obtains l r where "l \ S" "subseq r" "((f \ r) \ l) sequentially" proof atomize_elim have "subseq (op + m)" by (simp add: subseq_def) have "\n. (f o (\i. m + i)) n \ S" using assms by auto diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Dec 30 11:21:54 2015 +0100 @@ -1651,13 +1651,13 @@ qed (auto intro!: exI[of _ "{y. dist x y < e}" for e] open_ball simp: dist_commute) lemma (in metric_space) tendsto_iff: - "(f ---> l) F \ (\e>0. eventually (\x. dist (f x) l < e) F)" + "(f \ l) F \ (\e>0. eventually (\x. dist (f x) l < e) F)" unfolding nhds_metric filterlim_INF filterlim_principal by auto -lemma (in metric_space) tendstoI: "(\e. 0 < e \ eventually (\x. dist (f x) l < e) F) \ (f ---> l) F" +lemma (in metric_space) tendstoI: "(\e. 0 < e \ eventually (\x. dist (f x) l < e) F) \ (f \ l) F" by (auto simp: tendsto_iff) -lemma (in metric_space) tendstoD: "(f ---> l) F \ 0 < e \ eventually (\x. dist (f x) l < e) F" +lemma (in metric_space) tendstoD: "(f \ l) F \ 0 < e \ eventually (\x. dist (f x) l < e) F" by (auto simp: tendsto_iff) lemma (in metric_space) eventually_nhds_metric: @@ -1688,9 +1688,9 @@ lemma metric_tendsto_imp_tendsto: fixes a :: "'a :: metric_space" and b :: "'b :: metric_space" - assumes f: "(f ---> a) F" + assumes f: "(f \ a) F" assumes le: "eventually (\x. dist (g x) b \ dist (f x) a) F" - shows "(g ---> b) F" + shows "(g \ b) F" proof (rule tendstoI) fix e :: real assume "0 < e" with f have "eventually (\x. dist (f x) a < e) F" by (rule tendstoD) @@ -1977,7 +1977,7 @@ lemma tendsto_at_topI_sequentially: fixes f :: "real \ 'b::first_countable_topology" assumes *: "\X. filterlim X at_top sequentially \ (\n. f (X n)) \ y" - shows "(f ---> y) at_top" + shows "(f \ y) at_top" proof - from nhds_countable[of y] guess A . note A = this @@ -2009,7 +2009,7 @@ fixes f :: "real \ real" assumes mono: "mono f" assumes limseq: "(\n. f (real n)) \ y" - shows "(f ---> y) at_top" + shows "(f \ y) at_top" proof (rule tendstoI) fix e :: real assume "0 < e" with limseq obtain N :: nat where N: "\n. N \ n \ \f (real n) - y\ < e" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Topological_Spaces.thy Wed Dec 30 11:21:54 2015 +0100 @@ -480,13 +480,13 @@ subsubsection \Tendsto\ abbreviation (in topological_space) - tendsto :: "('b \ 'a) \ 'a \ 'b filter \ bool" (infixr "--->" 55) where - "(f ---> l) F \ filterlim f (nhds l) F" + tendsto :: "('b \ 'a) \ 'a \ 'b filter \ bool" (infixr "\" 55) where + "(f \ l) F \ filterlim f (nhds l) F" definition (in t2_space) Lim :: "'f filter \ ('f \ 'a) \ 'a" where - "Lim A f = (THE l. (f ---> l) A)" + "Lim A f = (THE l. (f \ l) A)" -lemma tendsto_eq_rhs: "(f ---> x) F \ x = y \ (f ---> y) F" +lemma tendsto_eq_rhs: "(f \ x) F \ x = y \ (f \ y) F" by simp named_theorems tendsto_intros "introduction rules for tendsto" @@ -498,55 +498,55 @@ \ lemma (in topological_space) tendsto_def: - "(f ---> l) F \ (\S. open S \ l \ S \ eventually (\x. f x \ S) F)" + "(f \ l) F \ (\S. open S \ l \ S \ eventually (\x. f x \ S) F)" unfolding nhds_def filterlim_INF filterlim_principal by auto lemma tendsto_cong: assumes "eventually (\x. f x = g x) F" - shows "(f ---> c) F \ (g ---> c) F" + shows "(f \ c) F \ (g \ c) F" by (rule filterlim_cong[OF refl refl assms]) -lemma tendsto_mono: "F \ F' \ (f ---> l) F' \ (f ---> l) F" +lemma tendsto_mono: "F \ F' \ (f \ l) F' \ (f \ l) F" unfolding tendsto_def le_filter_def by fast -lemma tendsto_within_subset: "(f ---> l) (at x within S) \ T \ S \ (f ---> l) (at x within T)" +lemma tendsto_within_subset: "(f \ l) (at x within S) \ T \ S \ (f \ l) (at x within T)" by (blast intro: tendsto_mono at_le) lemma filterlim_at: - "(LIM x F. f x :> at b within s) \ (eventually (\x. f x \ s \ f x \ b) F \ (f ---> b) F)" + "(LIM x F. f x :> at b within s) \ (eventually (\x. f x \ s \ f x \ b) F \ (f \ b) F)" by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute) lemma (in topological_space) topological_tendstoI: - "(\S. open S \ l \ S \ eventually (\x. f x \ S) F) \ (f ---> l) F" + "(\S. open S \ l \ S \ eventually (\x. f x \ S) F) \ (f \ l) F" unfolding tendsto_def by auto lemma (in topological_space) topological_tendstoD: - "(f ---> l) F \ open S \ l \ S \ eventually (\x. f x \ S) F" + "(f \ l) F \ open S \ l \ S \ eventually (\x. f x \ S) F" unfolding tendsto_def by auto lemma (in order_topology) order_tendsto_iff: - "(f ---> x) F \ (\lx. l < f x) F) \ (\u>x. eventually (\x. f x < u) F)" + "(f \ x) F \ (\lx. l < f x) F) \ (\u>x. eventually (\x. f x < u) F)" unfolding nhds_order filterlim_inf filterlim_INF filterlim_principal by auto lemma (in order_topology) order_tendstoI: "(\a. a < y \ eventually (\x. a < f x) F) \ (\a. y < a \ eventually (\x. f x < a) F) \ - (f ---> y) F" + (f \ y) F" unfolding order_tendsto_iff by auto lemma (in order_topology) order_tendstoD: - assumes "(f ---> y) F" + assumes "(f \ y) F" shows "a < y \ eventually (\x. a < f x) F" and "y < a \ eventually (\x. f x < a) F" using assms unfolding order_tendsto_iff by auto -lemma tendsto_bot [simp]: "(f ---> a) bot" +lemma tendsto_bot [simp]: "(f \ a) bot" unfolding tendsto_def by simp lemma (in linorder_topology) tendsto_max: - assumes X: "(X ---> x) net" - assumes Y: "(Y ---> y) net" - shows "((\x. max (X x) (Y x)) ---> max x y) net" + assumes X: "(X \ x) net" + assumes Y: "(Y \ y) net" + shows "((\x. max (X x) (Y x)) \ max x y) net" proof (rule order_tendstoI) fix a assume "a < max x y" then show "eventually (\x. a < max (X x) (Y x)) net" @@ -560,9 +560,9 @@ qed lemma (in linorder_topology) tendsto_min: - assumes X: "(X ---> x) net" - assumes Y: "(Y ---> y) net" - shows "((\x. min (X x) (Y x)) ---> min x y) net" + assumes X: "(X \ x) net" + assumes Y: "(Y \ y) net" + shows "((\x. min (X x) (Y x)) \ min x y) net" proof (rule order_tendstoI) fix a assume "a < min x y" then show "eventually (\x. a < min (X x) (Y x)) net" @@ -575,24 +575,24 @@ by (auto simp: min_less_iff_disj elim: eventually_mono) qed -lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\x. x) ---> a) (at a within s)" +lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\x. x) \ a) (at a within s)" unfolding tendsto_def eventually_at_topological by auto -lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\x. k) ---> k) F" +lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\x. k) \ k) F" by (simp add: tendsto_def) lemma (in t2_space) tendsto_unique: - assumes "F \ bot" and "(f ---> a) F" and "(f ---> b) F" + assumes "F \ bot" and "(f \ a) F" and "(f \ b) F" shows "a = b" proof (rule ccontr) assume "a \ b" obtain U V where "open U" "open V" "a \ U" "b \ V" "U \ V = {}" using hausdorff [OF \a \ b\] by fast have "eventually (\x. f x \ U) F" - using \(f ---> a) F\ \open U\ \a \ U\ by (rule topological_tendstoD) + using \(f \ a) F\ \open U\ \a \ U\ by (rule topological_tendstoD) moreover have "eventually (\x. f x \ V) F" - using \(f ---> b) F\ \open V\ \b \ V\ by (rule topological_tendstoD) + using \(f \ b) F\ \open V\ \b \ V\ by (rule topological_tendstoD) ultimately have "eventually (\x. False) F" proof eventually_elim @@ -605,28 +605,28 @@ qed lemma (in t2_space) tendsto_const_iff: - assumes "\ trivial_limit F" shows "((\x. a :: 'a) ---> b) F \ a = b" + assumes "\ trivial_limit F" shows "((\x. a :: 'a) \ b) F \ a = b" by (auto intro!: tendsto_unique [OF assms tendsto_const]) lemma increasing_tendsto: fixes f :: "_ \ 'a::order_topology" assumes bdd: "eventually (\n. f n \ l) F" and en: "\x. x < l \ eventually (\n. x < f n) F" - shows "(f ---> l) F" + shows "(f \ l) F" using assms by (intro order_tendstoI) (auto elim!: eventually_mono) lemma decreasing_tendsto: fixes f :: "_ \ 'a::order_topology" assumes bdd: "eventually (\n. l \ f n) F" and en: "\x. l < x \ eventually (\n. f n < x) F" - shows "(f ---> l) F" + shows "(f \ l) F" using assms by (intro order_tendstoI) (auto elim!: eventually_mono) lemma tendsto_sandwich: fixes f g h :: "'a \ 'b::order_topology" assumes ev: "eventually (\n. f n \ g n) net" "eventually (\n. g n \ h n) net" - assumes lim: "(f ---> c) net" "(h ---> c) net" - shows "(g ---> c) net" + assumes lim: "(f \ c) net" "(h \ c) net" + shows "(g \ c) net" proof (rule order_tendstoI) fix a show "a < c \ eventually (\x. a < g x) net" using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2) @@ -638,7 +638,7 @@ lemma limit_frequently_eq: assumes "F \ bot" assumes "frequently (\x. f x = c) F" - assumes "(f ---> d) F" + assumes "(f \ d) F" shows "d = (c :: 'a :: t1_space)" proof (rule ccontr) assume "d \ c" @@ -649,7 +649,7 @@ qed lemma tendsto_imp_eventually_ne: - assumes "F \ bot" "(f ---> c) F" "c \ (c' :: 'a :: t1_space)" + assumes "F \ bot" "(f \ c) F" "c \ (c' :: 'a :: t1_space)" shows "eventually (\z. f z \ c') F" proof (rule ccontr) assume "\eventually (\z. f z \ c') F" @@ -660,7 +660,7 @@ lemma tendsto_le: fixes f g :: "'a \ 'b::linorder_topology" assumes F: "\ trivial_limit F" - assumes x: "(f ---> x) F" and y: "(g ---> y) F" + assumes x: "(f \ x) F" and y: "(g \ y) F" assumes ev: "eventually (\x. g x \ f x) F" shows "y \ x" proof (rule ccontr) @@ -678,14 +678,14 @@ lemma tendsto_le_const: fixes f :: "'a \ 'b::linorder_topology" assumes F: "\ trivial_limit F" - assumes x: "(f ---> x) F" and a: "eventually (\i. a \ f i) F" + assumes x: "(f \ x) F" and a: "eventually (\i. a \ f i) F" shows "a \ x" using F x tendsto_const a by (rule tendsto_le) lemma tendsto_ge_const: fixes f :: "'a \ 'b::linorder_topology" assumes F: "\ trivial_limit F" - assumes x: "(f ---> x) F" and a: "eventually (\i. a \ f i) F" + assumes x: "(f \ x) F" and a: "eventually (\i. a \ f i) F" shows "a \ x" by (rule tendsto_le [OF F tendsto_const x a]) @@ -695,7 +695,7 @@ subsubsection \Rules about @{const Lim}\ lemma tendsto_Lim: - "\(trivial_limit net) \ (f ---> l) net \ Lim net f = l" + "\(trivial_limit net) \ (f \ l) net \ Lim net f = l" unfolding Lim_def using tendsto_unique[of net f] by auto lemma Lim_ident_at: "\ trivial_limit (at x within s) \ Lim (at x within s) (\x. x) = x" @@ -771,7 +771,7 @@ qed lemma tendsto_at_within_iff_tendsto_nhds: - "(g ---> g l) (at l within S) \ (g ---> g l) (inf (nhds l) (principal S))" + "(g \ g l) (at l within S) \ (g \ g l) (inf (nhds l) (principal S))" unfolding tendsto_def eventually_at_filter eventually_inf_principal by (intro ext all_cong imp_cong) (auto elim!: eventually_mono) @@ -780,7 +780,7 @@ abbreviation (in topological_space) LIMSEQ :: "[nat \ 'a, 'a] \ bool" ("((_)/ \ (_))" [60, 60] 60) where - "X \ L \ (X ---> L) sequentially" + "X \ L \ (X \ L) sequentially" abbreviation (in t2_space) lim :: "(nat \ 'a) \ 'a" where "lim X \ Lim sequentially X" @@ -1196,7 +1196,7 @@ lemma tendsto_at_iff_sequentially: fixes f :: "'a :: first_countable_topology \ _" - shows "(f ---> a) (at x within s) \ (\X. (\i. X i \ s - {x}) \ X \ x \ ((f \ X) \ a))" + shows "(f \ a) (at x within s) \ (\X. (\i. X i \ s - {x}) \ X \ x \ ((f \ X) \ a))" unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap at_within_def eventually_nhds_within_iff_sequentially comp_def by metis @@ -1205,9 +1205,9 @@ abbreviation LIM :: "('a::topological_space \ 'b::topological_space) \ 'a \ 'b \ bool" ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where - "f -- a --> L \ (f ---> L) (at a)" + "f -- a --> L \ (f \ L) (at a)" -lemma tendsto_within_open: "a \ S \ open S \ (f ---> l) (at a within S) \ (f -- a --> l)" +lemma tendsto_within_open: "a \ S \ open S \ (f \ l) (at a within S) \ (f -- a --> l)" unfolding tendsto_def by (simp add: at_within_open[where S=S]) lemma LIM_const_not_eq[tendsto_intros]: @@ -1241,19 +1241,19 @@ by simp lemma tendsto_at_iff_tendsto_nhds: - "g -- l --> g l \ (g ---> g l) (nhds l)" + "g -- l --> g l \ (g \ g l) (nhds l)" unfolding tendsto_def eventually_at_filter by (intro ext all_cong imp_cong) (auto elim!: eventually_mono) lemma tendsto_compose: - "g -- l --> g l \ (f ---> l) F \ ((\x. g (f x)) ---> g l) F" + "g -- l --> g l \ (f \ l) F \ ((\x. g (f x)) \ g l) F" unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g]) lemma LIM_o: "\g -- l --> g l; f -- a --> l\ \ (g \ f) -- a --> g l" unfolding o_def by (rule tendsto_compose) lemma tendsto_compose_eventually: - "g -- l --> m \ (f ---> l) F \ eventually (\x. f x \ l) F \ ((\x. g (f x)) ---> m) F" + "g -- l --> m \ (f \ l) F \ eventually (\x. f x \ l) F \ ((\x. g (f x)) \ m) F" by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at) lemma LIM_compose_eventually: @@ -1263,7 +1263,7 @@ shows "(\x. g (f x)) -- a --> c" using g f inj by (rule tendsto_compose_eventually) -lemma tendsto_compose_filtermap: "((g \ f) ---> T) F \ (g ---> T) (filtermap f F)" +lemma tendsto_compose_filtermap: "((g \ f) \ T) F \ (g \ T) (filtermap f F)" by (simp add: filterlim_def filtermap_filtermap comp_def) subsubsection \Relation of LIM and LIMSEQ\ @@ -1329,7 +1329,7 @@ fixes a :: "_ :: {linorder_topology, first_countable_topology}" assumes "b < a" assumes *: "\S. (\n. S n < a) \ (\n. b < S n) \ incseq S \ S \ a \ (\n. X (S n)) \ L" - shows "(X ---> L) (at_left a)" + shows "(X \ L) (at_left a)" using assms unfolding tendsto_def [where l=L] by (simp add: sequentially_imp_eventually_at_left) @@ -1367,7 +1367,7 @@ fixes a :: "_ :: {linorder_topology, first_countable_topology}" assumes "a < b" assumes *: "\S. (\n. a < S n) \ (\n. S n < b) \ decseq S \ S \ a \ (\n. X (S n)) \ L" - shows "(X ---> L) (at_right a)" + shows "(X \ L) (at_right a)" using assms unfolding tendsto_def [where l=L] by (simp add: sequentially_imp_eventually_at_right) @@ -1376,7 +1376,7 @@ subsubsection \Continuity on a set\ definition continuous_on :: "'a set \ ('a :: topological_space \ 'b :: topological_space) \ bool" where - "continuous_on s f \ (\x\s. (f ---> f x) (at x within s))" + "continuous_on s f \ (\x\s. (f \ f x) (at x within s))" lemma continuous_on_cong [cong]: "s = t \ (\x. x \ t \ f x = g x) \ continuous_on s f \ continuous_on t g" @@ -1559,7 +1559,7 @@ subsubsection \Continuity at a point\ definition continuous :: "'a::t2_space filter \ ('a \ 'b::topological_space) \ bool" where - "continuous F f \ (f ---> f (Lim F (\x. x))) F" + "continuous F f \ (f \ f (Lim F (\x. x))) F" lemma continuous_bot[continuous_intros, simp]: "continuous bot f" unfolding continuous_def by auto @@ -1567,7 +1567,7 @@ lemma continuous_trivial_limit: "trivial_limit net \ continuous net f" by simp -lemma continuous_within: "continuous (at x within s) f \ (f ---> f x) (at x within s)" +lemma continuous_within: "continuous (at x within s) f \ (f \ f x) (at x within s)" by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at continuous_def) lemma continuous_within_topological: @@ -1619,7 +1619,7 @@ lemma isCont_o[continuous_intros]: "isCont f a \ isCont g (f a) \ isCont (g \ f) a" unfolding o_def by (rule isCont_o2) -lemma isCont_tendsto_compose: "isCont g l \ (f ---> l) F \ ((\x. g (f x)) ---> g l) F" +lemma isCont_tendsto_compose: "isCont g l \ (f \ l) F \ ((\x. g (f x)) \ g l) F" unfolding isCont_def by (rule tendsto_compose) lemma continuous_within_compose3: @@ -2271,7 +2271,7 @@ assumes S: "S \ {}" "bdd_above S" shows "f (Sup S) = (SUP s:S. f s)" proof (rule antisym) - have f: "(f ---> f (Sup S)) (at_left (Sup S))" + have f: "(f \ f (Sup S)) (at_left (Sup S))" using cont unfolding continuous_within . show "f (Sup S) \ (SUP s:S. f s)" @@ -2308,7 +2308,7 @@ assumes S: "S \ {}" "bdd_above S" shows "f (Sup S) = (INF s:S. f s)" proof (rule antisym) - have f: "(f ---> f (Sup S)) (at_left (Sup S))" + have f: "(f \ f (Sup S)) (at_left (Sup S))" using cont unfolding continuous_within . show "(INF s:S. f s) \ f (Sup S)" @@ -2345,7 +2345,7 @@ assumes S: "S \ {}" "bdd_below S" shows "f (Inf S) = (INF s:S. f s)" proof (rule antisym) - have f: "(f ---> f (Inf S)) (at_right (Inf S))" + have f: "(f \ f (Inf S)) (at_right (Inf S))" using cont unfolding continuous_within . show "(INF s:S. f s) \ f (Inf S)" @@ -2382,7 +2382,7 @@ assumes S: "S \ {}" "bdd_below S" shows "f (Inf S) = (SUP s:S. f s)" proof (rule antisym) - have f: "(f ---> f (Inf S)) (at_right (Inf S))" + have f: "(f \ f (Inf S)) (at_right (Inf S))" using cont unfolding continuous_within . show "f (Inf S) \ (SUP s:S. f s)" diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Dec 29 23:50:44 2015 +0100 +++ b/src/HOL/Transcendental.thy Wed Dec 30 11:21:54 2015 +0100 @@ -181,7 +181,7 @@ corollary lim_n_over_pown: fixes x :: "'a::{real_normed_field,banach}" - shows "1 < norm x \ ((\n. of_nat n / x^n) ---> 0) sequentially" + shows "1 < norm x \ ((\n. of_nat n / x^n) \ 0) sequentially" using powser_times_n_limit_0 [of "inverse x"] by (simp add: norm_divide divide_simps) @@ -811,7 +811,7 @@ fixes a :: "nat \ 'a::{real_normed_field,banach}" assumes s: "0 < s" and sm: "\x. norm x < s \ (\n. a n * x ^ n) sums (f x)" - shows "(f ---> a 0) (at 0)" + shows "(f \ a 0) (at 0)" proof - have "summable (\n. a n * (of_real s / 2) ^ n)" apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm]) @@ -825,7 +825,7 @@ done then have "isCont (\x. \n. a n * x ^ n) 0" by (blast intro: DERIV_continuous) - then have "((\x. \n. a n * x ^ n) ---> a 0) (at 0)" + then have "((\x. \n. a n * x ^ n) \ a 0) (at 0)" by (simp add: continuous_within powser_zero) then show ?thesis apply (rule Lim_transform) @@ -840,9 +840,9 @@ fixes a :: "nat \ 'a::{real_normed_field,banach}" assumes s: "0 < s" and sm: "\x. x \ 0 \ norm x < s \ (\n. a n * x ^ n) sums (f x)" - shows "(f ---> a 0) (at 0)" + shows "(f \ a 0) (at 0)" proof - - have *: "((\x. if x = 0 then a 0 else f x) ---> a 0) (at 0)" + have *: "((\x. if x = 0 then a 0 else f x) \ a 0) (at 0)" apply (rule powser_limit_0 [OF s]) apply (case_tac "x=0") apply (auto simp add: powser_sums_zero sm) @@ -1208,7 +1208,7 @@ lemma tendsto_exp [tendsto_intros]: fixes f:: "_ \'a::{real_normed_field,banach}" - shows "(f ---> a) F \ ((\x. exp (f x)) ---> exp a) F" + shows "(f \ a) F \ ((\x. exp (f x)) \ exp a) F" by (rule isCont_tendsto_compose [OF isCont_exp]) lemma continuous_exp [continuous_intros]: @@ -1597,7 +1597,7 @@ lemma tendsto_ln [tendsto_intros]: fixes a::real shows - "(f ---> a) F \ a \ 0 \ ((\x. ln (f x)) ---> ln a) F" + "(f \ a) F \ a \ 0 \ ((\x. ln (f x)) \ ln a) F" by (rule isCont_tendsto_compose [OF isCont_ln]) lemma continuous_ln: @@ -2015,7 +2015,7 @@ qed qed -lemma exp_at_bot: "(exp ---> (0::real)) at_bot" +lemma exp_at_bot: "(exp \ (0::real)) at_bot" unfolding tendsto_Zfun_iff proof (rule ZfunI, simp add: eventually_at_bot_dense) fix r :: real assume "0 < r" @@ -2036,7 +2036,7 @@ lemma lim_exp_minus_1: fixes x :: "'a::{real_normed_field,banach}" - shows "((\z::'a. (exp(z) - 1) / z) ---> 1) (at 0)" + shows "((\z::'a. (exp(z) - 1) / z) \ 1) (at 0)" proof - have "((\z::'a. exp(z) - 1) has_field_derivative 1) (at 0)" by (intro derivative_eq_intros | simp)+ @@ -2059,10 +2059,10 @@ by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top) (auto simp: eventually_at_top_dense) -lemma tendsto_power_div_exp_0: "((\x. x ^ k / exp x) ---> (0::real)) at_top" +lemma tendsto_power_div_exp_0: "((\x. x ^ k / exp x) \ (0::real)) at_top" proof (induct k) case 0 - show "((\x. x ^ 0 / exp x) ---> (0::real)) at_top" + show "((\x. x ^ 0 / exp x) \ (0::real)) at_top" by (simp add: inverse_eq_divide[symmetric]) (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono at_top_le_at_infinity order_refl) @@ -2077,7 +2077,7 @@ show "eventually (\x. exp x \ 0) at_top" by auto from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"] - show "((\x. real (Suc k) * x ^ k / exp x) ---> 0) at_top" + show "((\x. real (Suc k) * x ^ k / exp x) \ 0) at_top" by simp qed (rule exp_at_top) qed @@ -2089,7 +2089,7 @@ lemma tendsto_log [tendsto_intros]: - "\(f ---> a) F; (g ---> b) F; 0 < a; a \ 1; 0 < b\ \ ((\x. log (f x) (g x)) ---> log a b) F" + "\(f \ a) F; (g \ b) F; 0 < a; a \ 1; 0 < b\ \ ((\x. log (f x) (g x)) \ log a b) F" unfolding log_def by (intro tendsto_intros) auto lemma continuous_log: @@ -2505,11 +2505,11 @@ lemma tendsto_powr [tendsto_intros]: fixes a::real - assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \ 0" - shows "((\x. f x powr g x) ---> a powr b) F" + assumes f: "(f \ a) F" and g: "(g \ b) F" and a: "a \ 0" + shows "((\x. f x powr g x) \ a powr b) F" unfolding powr_def proof (rule filterlim_If) - from f show "((\x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" + from f show "((\x. 0) \ (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds) qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1) @@ -2539,22 +2539,22 @@ lemma tendsto_powr2: fixes a::real - assumes f: "(f ---> a) F" and g: "(g ---> b) F" and f_nonneg: "\\<^sub>F x in F. 0 \ f x" and b: "0 < b" - shows "((\x. f x powr g x) ---> a powr b) F" + assumes f: "(f \ a) F" and g: "(g \ b) F" and f_nonneg: "\\<^sub>F x in F. 0 \ f x" and b: "0 < b" + shows "((\x. f x powr g x) \ a powr b) F" unfolding powr_def proof (rule filterlim_If) - from f show "((\x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" + from f show "((\x. 0) \ (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds) next { assume "a = 0" with f f_nonneg have "LIM x inf F (principal {x. f x \ 0}). f x :> at_right 0" by (auto simp add: filterlim_at eventually_inf_principal le_less elim: eventually_mono intro: tendsto_mono inf_le1) - then have "((\x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \ 0}))" + then have "((\x. exp (g x * ln (f x))) \ 0) (inf F (principal {x. f x \ 0}))" by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0] filterlim_tendsto_pos_mult_at_bot[OF _ \0 < b\] intro: tendsto_mono inf_le1 g) } - then show "((\x. exp (g x * ln (f x))) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \ 0}))" + then show "((\x. exp (g x * ln (f x))) \ (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \ 0}))" using f g by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1) qed @@ -2596,19 +2596,19 @@ declare has_real_derivative_powr[THEN DERIV_chain2, derivative_intros] lemma tendsto_zero_powrI: - assumes "(f ---> (0::real)) F" "(g ---> b) F" "\\<^sub>F x in F. 0 \ f x" "0 < b" - shows "((\x. f x powr g x) ---> 0) F" + assumes "(f \ (0::real)) F" "(g \ b) F" "\\<^sub>F x in F. 0 \ f x" "0 < b" + shows "((\x. f x powr g x) \ 0) F" using tendsto_powr2[OF assms] by simp lemma tendsto_neg_powr: assumes "s < 0" and f: "LIM x F. f x :> at_top" - shows "((\x. f x powr s) ---> (0::real)) F" + shows "((\x. f x powr s) \ (0::real)) F" proof - - have "((\x. exp (s * ln (f x))) ---> (0::real)) F" (is "?X") + have "((\x. exp (s * ln (f x))) \ (0::real)) F" (is "?X") by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_top] filterlim_tendsto_neg_mult_at_bot assms) - also have "?X \ ((\x. f x powr s) ---> (0::real)) F" + also have "?X \ ((\x. f x powr s) \ (0::real)) F" using f filterlim_at_top_dense[of f F] by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_mono) finally show ?thesis . @@ -2616,14 +2616,14 @@ lemma tendsto_exp_limit_at_right: fixes x :: real - shows "((\y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)" + shows "((\y. (1 + x * y) powr (1 / y)) \ exp x) (at_right 0)" proof cases assume "x \ 0" have "((\y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)" by (auto intro!: derivative_eq_intros) - then have "((\y. ln (1 + x * y) / y) ---> x) (at 0)" + then have "((\y. ln (1 + x * y) / y) \ x) (at 0)" by (auto simp add: has_field_derivative_def field_has_derivative_at) - then have *: "((\y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)" + then have *: "((\y. exp (ln (1 + x * y) / y)) \ exp x) (at 0)" by (rule tendsto_intros) then show ?thesis proof (rule filterlim_mono_eventually) @@ -2638,7 +2638,7 @@ lemma tendsto_exp_limit_at_top: fixes x :: real - shows "((\y. (1 + x / y) powr y) ---> exp x) at_top" + shows "((\y. (1 + x / y) powr y) \ exp x) at_top" apply (subst filterlim_at_top_to_right) apply (simp add: inverse_eq_divide) apply (rule tendsto_exp_limit_at_right) @@ -2819,12 +2819,12 @@ lemma tendsto_sin [tendsto_intros]: fixes f:: "_ \ 'a::{real_normed_field,banach}" - shows "(f ---> a) F \ ((\x. sin (f x)) ---> sin a) F" + shows "(f \ a) F \ ((\x. sin (f x)) \ sin a) F" by (rule isCont_tendsto_compose [OF isCont_sin]) lemma tendsto_cos [tendsto_intros]: fixes f:: "_ \ 'a::{real_normed_field,banach}" - shows "(f ---> a) F \ ((\x. cos (f x)) ---> cos a) F" + shows "(f \ a) F \ ((\x. cos (f x)) \ cos a) F" by (rule isCont_tendsto_compose [OF isCont_cos]) lemma continuous_sin [continuous_intros]: @@ -4049,7 +4049,7 @@ lemma tendsto_tan [tendsto_intros]: fixes f :: "'a \ 'a::{real_normed_field,banach}" - shows "\(f ---> a) F; cos a \ 0\ \ ((\x. tan (f x)) ---> tan a) F" + shows "\(f \ a) F; cos a \ 0\ \ ((\x. tan (f x)) \ tan a) F" by (rule isCont_tendsto_compose [OF isCont_tan]) lemma continuous_tan: @@ -4318,7 +4318,7 @@ lemma tendsto_cot [tendsto_intros]: fixes f :: "'a \ 'a::{real_normed_field,banach}" - shows "\(f ---> a) F; sin a \ 0\ \ ((\x. cot (f x)) ---> cot a) F" + shows "\(f \ a) F; sin a \ 0\ \ ((\x. cot (f x)) \ cot a) F" by (rule isCont_tendsto_compose [OF isCont_cot]) lemma continuous_cot: @@ -4631,7 +4631,7 @@ apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le) done -lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \ ((\x. arctan (f x)) ---> arctan x) F" +lemma tendsto_arctan [tendsto_intros]: "(f \ x) F \ ((\x. arctan (f x)) \ arctan x) F" by (rule isCont_tendsto_compose [OF isCont_arctan]) lemma continuous_arctan [continuous_intros]: "continuous F f \ continuous F (\x. arctan (f x))" @@ -4690,7 +4690,7 @@ (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 intro!: tan_monotone exI[of _ "pi/2"]) -lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top" +lemma tendsto_arctan_at_top: "(arctan \ (pi/2)) at_top" proof (rule tendstoI) fix e :: real assume "0 < e" @@ -4712,7 +4712,7 @@ qed qed -lemma tendsto_arctan_at_bot: "(arctan ---> - (pi/2)) at_bot" +lemma tendsto_arctan_at_bot: "(arctan \ - (pi/2)) at_bot" unfolding filterlim_at_bot_mirror arctan_minus by (intro tendsto_minus tendsto_arctan_at_top)