--- 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)
--- 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 \<Longrightarrow> (g ---> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
+ "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
by (auto intro!: tendsto_intros)
lemma tendsto_complex_iff:
- "(f ---> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
+ "(f \<longlongrightarrow> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) \<longlongrightarrow> Re x) F \<and> ((\<lambda>x. Im (f x)) \<longlongrightarrow> Im x) F)"
proof safe
- assume "((\<lambda>x. Re (f x)) ---> Re x) F" "((\<lambda>x. Im (f x)) ---> Im x) F"
- from tendsto_Complex[OF this] show "(f ---> x) F"
+ assume "((\<lambda>x. Re (f x)) \<longlongrightarrow> Re x) F" "((\<lambda>x. Im (f x)) \<longlongrightarrow> Im x) F"
+ from tendsto_Complex[OF this] show "(f \<longlongrightarrow> 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: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
+lemma lim_cnj: "((\<lambda>x. cnj(f x)) \<longlongrightarrow> cnj l) F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff)
lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
--- 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 \<longleftrightarrow>
(bounded_linear f' \<and>
- ((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) ---> 0) F)"
+ ((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) \<longlongrightarrow> 0) F)"
text \<open>
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 (\<lambda>x. x)"
let ?D = "\<lambda>f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)"
- have "((\<lambda>x. ?D f f' x + ?D g g' x) ---> (0 + 0)) F"
+ have "((\<lambda>x. ?D f f' x + ?D g g' x) \<longlongrightarrow> (0 + 0)) F"
using f g by (intro tendsto_add) (auto simp: has_derivative_def)
- then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) ---> 0) F"
+ then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) \<longlongrightarrow> 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) \<longleftrightarrow>
- (bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s))"
+ (bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 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) \<longleftrightarrow>
- (bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) ---> 0) (at x within s))"
+ (bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) \<longlongrightarrow> 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' \<Longrightarrow> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s) \<Longrightarrow>
+ "bounded_linear f' \<Longrightarrow> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s) \<Longrightarrow>
(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: "(\<And>y. y \<in> s \<Longrightarrow> y \<noteq> x \<Longrightarrow> dist y x < e \<Longrightarrow> norm ((f y - f x) - f' (y - x)) / norm (y - x) \<le> H y)"
- and "(H ---> 0) (at x within s)"
+ and "(H \<longlongrightarrow> 0) (at x within s)"
shows "(f has_derivative f') (at x within s)"
unfolding has_derivative_iff_norm
proof safe
- show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) ---> 0) (at x within s)"
+ show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)"
proof (rule tendsto_sandwich[where f="\<lambda>x. 0"])
- show "(H ---> 0) (at x within s)" by fact
+ show "(H \<longlongrightarrow> 0) (at x within s)" by fact
show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> 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 = "\<lambda>f. (f ---> 0) (at x within s)"
+ let ?L = "\<lambda>f. (f \<longlongrightarrow> 0) (at x within s)"
have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x))"
using f unfolding has_derivative_iff_norm by blast
then have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m)
@@ -216,7 +216,7 @@
subsection \<open>Composition\<close>
-lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \<Longrightarrow> (f ---> y) (at x within s) \<longleftrightarrow> (f ---> y) (inf (nhds x) (principal s))"
+lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \<Longrightarrow> (f \<longlongrightarrow> y) (at x within s) \<longleftrightarrow> (f \<longlongrightarrow> 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: "\<And>x. norm (g' x) \<le> norm x * kG" by fast
note G.tendsto[tendsto_intros]
- let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
+ let ?L = "\<lambda>f. (f \<longlongrightarrow> 0) (at x within s)"
let ?D = "\<lambda>f f' x y. (f y - f x) - f' (y - x)"
let ?N = "\<lambda>f f' x y. norm (?D f f' x y) / norm (y - x)"
let ?gf = "\<lambda>x. g (f x)" and ?gf' = "\<lambda>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 \<longlongrightarrow> 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)) \<longlongrightarrow> 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)) \<longlongrightarrow> 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 "((\<lambda>y. Nf y * kG + Ng y * (Nf y + kF)) ---> 0) (at x within s)"
+ show "((\<lambda>y. Nf y * kG + Ng y * (Nf y + kF)) \<longlongrightarrow> 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 \<longlongrightarrow> 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 \<longlongrightarrow> 0) ?F" "(Ng \<longlongrightarrow> 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 \<longlongrightarrow> 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 \<longlongrightarrow> 0) ?F"
by simp
next
fix y::'d assume "y \<noteq> x"
@@ -377,7 +377,7 @@
next
show "0 < norm x" using x by simp
next
- show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) ---> 0) (at x within s)"
+ show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) \<longlongrightarrow> 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 "\<And>x. x \<le> b \<Longrightarrow> (EX y. DERIV f x :> y & y > 0)"
- and lim: "(f ---> flim) at_bot"
+ and lim: "(f \<longlongrightarrow> flim) at_bot"
shows "flim < f b"
proof -
have "flim \<le> f (b - 1)"
@@ -1455,7 +1455,7 @@
lemma DERIV_neg_imp_decreasing_at_top:
fixes f :: "real => real"
assumes der: "\<And>x. x \<ge> b \<Longrightarrow> (EX y. DERIV f x :> y & y < 0)"
- and lim: "(f ---> flim) at_top"
+ and lim: "(f \<longlongrightarrow> flim) at_top"
shows "flim < f b"
apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>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 \<Longrightarrow> (f ---> g a) (at_right a) \<Longrightarrow> isCont (\<lambda>x. if x \<le> a then g x else f x) a"
+ shows "continuous (at_left a) g \<Longrightarrow> (f \<longlongrightarrow> g a) (at_right a) \<Longrightarrow> isCont (\<lambda>x. if x \<le> 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 \<Rightarrow> real"
- assumes f_0: "(f0 ---> 0) (at_right 0)"
- assumes g_0: "(g0 ---> 0) (at_right 0)"
+ assumes f_0: "(f0 \<longlongrightarrow> 0) (at_right 0)"
+ assumes g_0: "(g0 \<longlongrightarrow> 0) (at_right 0)"
assumes ev:
"eventually (\<lambda>x. g0 x \<noteq> 0) (at_right 0)"
"eventually (\<lambda>x. g' x \<noteq> 0) (at_right 0)"
"eventually (\<lambda>x. DERIV f0 x :> f' x) (at_right 0)"
"eventually (\<lambda>x. DERIV g0 x :> g' x) (at_right 0)"
- assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) (at_right 0)"
- shows "((\<lambda> x. f0 x / g0 x) ---> x) (at_right 0)"
+ assumes lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) (at_right 0)"
+ shows "((\<lambda> x. f0 x / g0 x) \<longlongrightarrow> x) (at_right 0)"
proof -
def f \<equiv> "\<lambda>x. if x \<le> 0 then 0 else f0 x"
then have "f 0 = 0" by simp
@@ -1674,15 +1674,15 @@
moreover
from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
by eventually_elim auto
- then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
+ then have "((\<lambda>x. norm (\<zeta> x)) \<longlongrightarrow> 0) (at_right 0)"
by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"]) auto
- then have "(\<zeta> ---> 0) (at_right 0)"
+ then have "(\<zeta> \<longlongrightarrow> 0) (at_right 0)"
by (rule tendsto_norm_zero_cancel)
with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
by (auto elim!: eventually_mono simp: filterlim_at)
- from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
+ from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) \<longlongrightarrow> x) (at_right 0)"
by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
- ultimately have "((\<lambda>t. f t / g t) ---> x) (at_right 0)" (is ?P)
+ ultimately have "((\<lambda>t. f t / g t) \<longlongrightarrow> x) (at_right 0)" (is ?P)
by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
(auto elim: eventually_mono)
also have "?P \<longleftrightarrow> ?thesis"
@@ -1691,35 +1691,35 @@
qed
lemma lhopital_right:
- "((f::real \<Rightarrow> real) ---> 0) (at_right x) \<Longrightarrow> (g ---> 0) (at_right x) \<Longrightarrow>
+ "((f::real \<Rightarrow> real) \<longlongrightarrow> 0) (at_right x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at_right x) \<Longrightarrow>
eventually (\<lambda>x. g x \<noteq> 0) (at_right x) \<Longrightarrow>
eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow>
eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow>
eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow>
- ((\<lambda> x. (f' x / g' x)) ---> y) (at_right x) \<Longrightarrow>
- ((\<lambda> x. f x / g x) ---> y) (at_right x)"
+ ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_right x) \<Longrightarrow>
+ ((\<lambda> x. f x / g x) \<longlongrightarrow> 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 \<Rightarrow> real) ---> 0) (at_left x) \<Longrightarrow> (g ---> 0) (at_left x) \<Longrightarrow>
+ "((f::real \<Rightarrow> real) \<longlongrightarrow> 0) (at_left x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at_left x) \<Longrightarrow>
eventually (\<lambda>x. g x \<noteq> 0) (at_left x) \<Longrightarrow>
eventually (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow>
eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow>
eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow>
- ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
- ((\<lambda> x. f x / g x) ---> y) (at_left x)"
+ ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_left x) \<Longrightarrow>
+ ((\<lambda> x. f x / g x) \<longlongrightarrow> y) (at_left x)"
unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
lemma lhopital:
- "((f::real \<Rightarrow> real) ---> 0) (at x) \<Longrightarrow> (g ---> 0) (at x) \<Longrightarrow>
+ "((f::real \<Rightarrow> real) \<longlongrightarrow> 0) (at x) \<Longrightarrow> (g \<longlongrightarrow> 0) (at x) \<Longrightarrow>
eventually (\<lambda>x. g x \<noteq> 0) (at x) \<Longrightarrow>
eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow>
eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow>
eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow>
- ((\<lambda> x. (f' x / g' x)) ---> y) (at x) \<Longrightarrow>
- ((\<lambda> x. f x / g x) ---> y) (at x)"
+ ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at x) \<Longrightarrow>
+ ((\<lambda> x. f x / g x) \<longlongrightarrow> 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 (\<lambda>x. g' x \<noteq> 0) (at_right 0)"
"eventually (\<lambda>x. DERIV f x :> f' x) (at_right 0)"
"eventually (\<lambda>x. DERIV g x :> g' x) (at_right 0)"
- assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) (at_right 0)"
- shows "((\<lambda> x. f x / g x) ---> x) (at_right 0)"
+ assumes lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) (at_right 0)"
+ shows "((\<lambda> x. f x / g x) \<longlongrightarrow> 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: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"
+ have inv_g: "((\<lambda>x. inverse (g x)) \<longlongrightarrow> 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 "((\<lambda>x. norm (1 - g a * inverse (g x))) ---> norm (1 - g a * 0)) (at_right 0)"
+ then have "((\<lambda>x. norm (1 - g a * inverse (g x))) \<longlongrightarrow> norm (1 - g a * 0)) (at_right 0)"
by (intro tendsto_intros)
- then have "((\<lambda>x. norm (1 - g a / g x)) ---> 1) (at_right 0)"
+ then have "((\<lambda>x. norm (1 - g a / g x)) \<longlongrightarrow> 1) (at_right 0)"
by (simp add: inverse_eq_divide)
from this[unfolded tendsto_iff, rule_format, of 1]
have "eventually (\<lambda>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 "((\<lambda>t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)"
+ from inv_g have "((\<lambda>t. norm ((f a - x * g a) * inverse (g t))) \<longlongrightarrow> norm ((f a - x * g a) * 0)) (at_right 0)"
by (intro tendsto_intros)
- then have "((\<lambda>t. norm (f a - x * g a) / norm (g t)) ---> 0) (at_right 0)"
+ then have "((\<lambda>t. norm (f a - x * g a) / norm (g t)) \<longlongrightarrow> 0) (at_right 0)"
by (simp add: inverse_eq_divide)
from this[unfolded tendsto_iff, rule_format, of "e / 2"] \<open>0 < e\<close>
have "eventually (\<lambda>t. norm (f a - x * g a) / norm (g t) < e / 2) (at_right 0)"
@@ -1808,8 +1808,8 @@
eventually (\<lambda>x. g' x \<noteq> 0) (at_right x) \<Longrightarrow>
eventually (\<lambda>x. DERIV f x :> f' x) (at_right x) \<Longrightarrow>
eventually (\<lambda>x. DERIV g x :> g' x) (at_right x) \<Longrightarrow>
- ((\<lambda> x. (f' x / g' x)) ---> y) (at_right x) \<Longrightarrow>
- ((\<lambda> x. f x / g x) ---> y) (at_right x)"
+ ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_right x) \<Longrightarrow>
+ ((\<lambda> x. f x / g x) \<longlongrightarrow> 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 (\<lambda>x. g' x \<noteq> 0) (at_left x) \<Longrightarrow>
eventually (\<lambda>x. DERIV f x :> f' x) (at_left x) \<Longrightarrow>
eventually (\<lambda>x. DERIV g x :> g' x) (at_left x) \<Longrightarrow>
- ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
- ((\<lambda> x. f x / g x) ---> y) (at_left x)"
+ ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at_left x) \<Longrightarrow>
+ ((\<lambda> x. f x / g x) \<longlongrightarrow> 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'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
@@ -1828,8 +1828,8 @@
eventually (\<lambda>x. g' x \<noteq> 0) (at x) \<Longrightarrow>
eventually (\<lambda>x. DERIV f x :> f' x) (at x) \<Longrightarrow>
eventually (\<lambda>x. DERIV g x :> g' x) (at x) \<Longrightarrow>
- ((\<lambda> x. (f' x / g' x)) ---> y) (at x) \<Longrightarrow>
- ((\<lambda> x. f x / g x) ---> y) (at x)"
+ ((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> y) (at x) \<Longrightarrow>
+ ((\<lambda> x. f x / g x) \<longlongrightarrow> 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 (\<lambda>x. g' x \<noteq> 0) at_top"
assumes Df: "eventually (\<lambda>x. DERIV f x :> f' x) at_top"
assumes Dg: "eventually (\<lambda>x. DERIV g x :> g' x) at_top"
- assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) at_top"
- shows "((\<lambda> x. f x / g x) ---> x) at_top"
+ assumes lim: "((\<lambda> x. (f' x / g' x)) \<longlongrightarrow> x) at_top"
+ shows "((\<lambda> x. f x / g x) \<longlongrightarrow> x) at_top"
unfolding filterlim_at_top_to_right
proof (rule lhopital_right_0_at_top)
let ?F = "\<lambda>x. f (inverse x)"
@@ -1874,7 +1874,7 @@
using g' eventually_ge_at_top[where c="1::real"]
by eventually_elim auto
- show "((\<lambda>x. ?D f' x / ?D g' x) ---> x) ?R"
+ show "((\<lambda>x. ?D f' x / ?D g' x) \<longlongrightarrow> 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"]
--- 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 (\<lambda>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 \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
+lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) \<longlongrightarrow> ereal x) F"
using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"]
by (simp add: continuous_on_eq_continuous_at)
-lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) ---> - x) F"
+lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) \<longlongrightarrow> - 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 \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
+lemma ereal_Lim_uminus: "(f \<longlongrightarrow> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) \<longlongrightarrow> - f0) net"
using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>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: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+ assumes c: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> c * x) F"
proof -
{ fix c :: ereal assume "0 < c" "c < \<infinity>"
- then have "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+ then have "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> 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 "- \<infinity> < c" "c < 0"
then have "0 < - c" "- c < \<infinity>"
by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
- then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F"
+ then have "((\<lambda>x. (- c) * f x) \<longlongrightarrow> (- 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 \<noteq> 0" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+ assumes "x \<noteq> 0" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. c * f x::ereal) \<longlongrightarrow> c * x) F"
proof cases
assume "\<bar>c\<bar> = \<infinity>"
show ?thesis
@@ -1828,7 +1828,7 @@
qed (rule tendsto_cmult_ereal[OF _ f])
lemma tendsto_cadd_ereal[tendsto_intros, simp, intro]:
- assumes c: "y \<noteq> - \<infinity>" "x \<noteq> - \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
+ assumes c: "y \<noteq> - \<infinity>" "x \<noteq> - \<infinity>" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. f x + y::ereal) \<longlongrightarrow> 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: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
+ assumes c: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f \<longlongrightarrow> x) F" shows "((\<lambda>x. f x + y::ereal) \<longlongrightarrow> 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 "\<bar>x\<bar> \<noteq> \<infinity>" "(f ---> x) F"
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>" "(f \<longlongrightarrow> x) F"
shows "eventually (\<lambda>x. \<bar>f x\<bar> \<noteq> \<infinity>) F"
proof -
- have "(f ---> ereal (real_of_ereal x)) F"
+ have "(f \<longlongrightarrow> ereal (real_of_ereal x)) F"
using assms by (cases x) auto
then have "eventually (\<lambda>x. f x \<in> ereal ` UNIV) F"
by (rule topological_tendstoD) (auto intro: open_ereal)
@@ -2436,8 +2436,8 @@
subsubsection \<open>Convergent sequences\<close>
lemma lim_real_of_ereal[simp]:
- assumes lim: "(f ---> ereal x) net"
- shows "((\<lambda>x. real_of_ereal (f x)) ---> x) net"
+ assumes lim: "(f \<longlongrightarrow> ereal x) net"
+ shows "((\<lambda>x. real_of_ereal (f x)) \<longlongrightarrow> x) net"
proof (intro topological_tendstoI)
fix S
assume "open S" and "x \<in> 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]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
+lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) \<longlongrightarrow> ereal x) net \<longleftrightarrow> (f \<longlongrightarrow> x) net"
by (auto dest!: lim_real_of_ereal)
lemma convergent_real_imp_convergent_ereal:
@@ -2460,7 +2460,7 @@
thus "lim (\<lambda>n. ereal (a n)) = ereal (lim a)" using lim L limI by metis
qed
-lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
+lemma tendsto_PInfty: "(f \<longlongrightarrow> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
proof -
{
fix l :: ereal
@@ -2473,10 +2473,10 @@
qed
lemma tendsto_PInfty_eq_at_top:
- "((\<lambda>z. ereal (f z)) ---> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
+ "((\<lambda>z. ereal (f z)) \<longlongrightarrow> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
unfolding tendsto_PInfty filterlim_at_top_dense by simp
-lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
+lemma tendsto_MInfty: "(f \<longlongrightarrow> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>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 \<Rightarrow> ereal"
assumes "x \<noteq> 0"
- and tendsto: "((\<lambda>x. ereal (real_of_ereal (f x))) ---> x) net"
- shows "(f ---> x) net"
+ and tendsto: "((\<lambda>x. ereal (real_of_ereal (f x))) \<longlongrightarrow> x) net"
+ shows "(f \<longlongrightarrow> x) net"
proof (intro topological_tendstoI)
fix S
assume S: "open S" "x \<in> S"
@@ -2572,8 +2572,8 @@
lemma tendsto_ereal_realI:
fixes f :: "'a \<Rightarrow> ereal"
- assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and tendsto: "(f ---> x) net"
- shows "((\<lambda>x. ereal (real_of_ereal (f x))) ---> x) net"
+ assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and tendsto: "(f \<longlongrightarrow> x) net"
+ shows "((\<lambda>x. ereal (real_of_ereal (f x))) \<longlongrightarrow> x) net"
proof (intro topological_tendstoI)
fix S
assume "open S" and "x \<in> S"
@@ -2592,15 +2592,15 @@
lemma tendsto_add_ereal:
fixes x y :: ereal
assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and y: "\<bar>y\<bar> \<noteq> \<infinity>"
- assumes f: "(f ---> x) F" and g: "(g ---> y) F"
- shows "((\<lambda>x. f x + g x) ---> x + y) F"
+ assumes f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
+ shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
proof -
from x obtain r where x': "x = ereal r" by (cases x) auto
- with f have "((\<lambda>i. real_of_ereal (f i)) ---> r) F" by simp
+ with f have "((\<lambda>i. real_of_ereal (f i)) \<longlongrightarrow> r) F" by simp
moreover
from y obtain p where y': "y = ereal p" by (cases y) auto
- with g have "((\<lambda>i. real_of_ereal (g i)) ---> p) F" by simp
- ultimately have "((\<lambda>i. real_of_ereal (f i) + real_of_ereal (g i)) ---> r + p) F"
+ with g have "((\<lambda>i. real_of_ereal (g i)) \<longlongrightarrow> p) F" by simp
+ ultimately have "((\<lambda>i. real_of_ereal (f i) + real_of_ereal (g i)) \<longlongrightarrow> 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 \<Rightarrow> ereal"
assumes "\<not> trivial_limit net"
- shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
+ shows "(f \<longlongrightarrow> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
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 \<Rightarrow> ereal"
assumes "\<not> trivial_limit net"
- shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
+ shows "(f \<longlongrightarrow> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
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 \<circ> real_of_ereal) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
- "((f \<circ> real_of_ereal) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
- "((f \<circ> real_of_ereal) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
- "((f \<circ> real_of_ereal) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
+ "((f \<circ> real_of_ereal) \<longlongrightarrow> y) (at_left (ereal x)) \<longleftrightarrow> (f \<longlongrightarrow> y) (at_left x)"
+ "((f \<circ> real_of_ereal) \<longlongrightarrow> y) (at_right (ereal x)) \<longleftrightarrow> (f \<longlongrightarrow> y) (at_right x)"
+ "((f \<circ> real_of_ereal) \<longlongrightarrow> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f \<longlongrightarrow> y) at_top"
+ "((f \<circ> real_of_ereal) \<longlongrightarrow> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f \<longlongrightarrow> 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 \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
- "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
- "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
+ "((ereal \<circ> f) \<longlongrightarrow> ereal a) F \<longleftrightarrow> (f \<longlongrightarrow> a) F"
+ "((ereal \<circ> f) \<longlongrightarrow> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
+ "((ereal \<circ> f) \<longlongrightarrow> -\<infinity>) F \<longleftrightarrow> (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 -- \<infinity> --> (0::ereal)"
proof -
- have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity"
+ have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> 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 \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)
-lemma inverse_ereal_tendsto_at_right_0: "(inverse ---> \<infinity>) (at_right (0::ereal))"
+lemma inverse_ereal_tendsto_at_right_0: "(inverse \<longlongrightarrow> \<infinity>) (at_right (0::ereal))"
unfolding tendsto_compose_filtermap[symmetric] at_right_ereal zero_ereal_def
by (subst filterlim_cong[OF refl refl, where g="\<lambda>x. ereal (inverse x)"])
(auto simp: eventually_at_filter tendsto_PInfty_eq_at_top filterlim_inverse_at_top_right)
--- 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 \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
assumes ntriv: "\<not> trivial_limit F"
- assumes lim: "(f ---> f0) F"
+ assumes lim: "(f \<longlongrightarrow> 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 \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
assumes ntriv: "\<not> trivial_limit F"
- assumes lim: "(f ---> f0) F"
+ assumes lim: "(f \<longlongrightarrow> 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: "\<not> trivial_limit F"
and lim: "Liminf F f = f0" "Limsup F f = f0"
- shows "(f ---> f0) F"
+ shows "(f \<longlongrightarrow> 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 "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
+ shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
lemma liminf_subseq_mono:
--- 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 \<open>Continuity of operations\<close>
lemma tendsto_fst [tendsto_intros]:
- assumes "(f ---> a) F"
- shows "((\<lambda>x. fst (f x)) ---> fst a) F"
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
proof (rule topological_tendstoI)
fix S assume "open S" and "fst a \<in> S"
then have "open (fst -` S)" and "a \<in> fst -` S"
@@ -165,8 +165,8 @@
qed
lemma tendsto_snd [tendsto_intros]:
- assumes "(f ---> a) F"
- shows "((\<lambda>x. snd (f x)) ---> snd a) F"
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
proof (rule topological_tendstoI)
fix S assume "open S" and "snd a \<in> S"
then have "open (snd -` S)" and "a \<in> snd -` S"
@@ -178,18 +178,18 @@
qed
lemma tendsto_Pair [tendsto_intros]:
- assumes "(f ---> a) F" and "(g ---> b) F"
- shows "((\<lambda>x. (f x, g x)) ---> (a, b)) F"
+ assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
+ shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
proof (rule topological_tendstoI)
fix S assume "open S" and "(a, b) \<in> S"
then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
unfolding open_prod_def by fast
have "eventually (\<lambda>x. f x \<in> A) F"
- using \<open>(f ---> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
+ using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
by (rule topological_tendstoD)
moreover
have "eventually (\<lambda>x. g x \<in> B) F"
- using \<open>(g ---> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
+ using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
by (rule topological_tendstoD)
ultimately
show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
@@ -491,7 +491,7 @@
let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
- show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)"
+ show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)"
using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm)
fix y :: 'a assume "y \<noteq> x"
--- 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 \<Longrightarrow> ((\<lambda>n. f(n)) ---> l) sequentially"
+ "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> 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 (\<lambda>x. f x - a) F"
+lemma tendsto_Zfun_iff: "(f \<longlongrightarrow> a) F = Zfun (\<lambda>x. f x - a) F"
by (simp only: tendsto_iff Zfun_def dist_norm)
-lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk>
- \<Longrightarrow> (g ---> 0) F"
+lemma tendsto_0_le: "\<lbrakk>(f \<longlongrightarrow> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk>
+ \<Longrightarrow> (g \<longlongrightarrow> 0) F"
by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)
subsubsection \<open>Distance and norms\<close>
lemma tendsto_dist [tendsto_intros]:
fixes l m :: "'a :: metric_space"
- assumes f: "(f ---> l) F" and g: "(g ---> m) F"
- shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F"
+ assumes f: "(f \<longlongrightarrow> l) F" and g: "(g \<longlongrightarrow> m) F"
+ shows "((\<lambda>x. dist (f x) (g x)) \<longlongrightarrow> 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 \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
+ "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> 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 \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) F"
+ "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F"
by (drule tendsto_norm, simp)
lemma tendsto_norm_zero_cancel:
- "((\<lambda>x. norm (f x)) ---> 0) F \<Longrightarrow> (f ---> 0) F"
+ "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F"
unfolding tendsto_iff dist_norm by simp
lemma tendsto_norm_zero_iff:
- "((\<lambda>x. norm (f x)) ---> 0) F \<longleftrightarrow> (f ---> 0) F"
+ "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F"
unfolding tendsto_iff dist_norm by simp
lemma tendsto_rabs [tendsto_intros]:
- "(f ---> (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) F"
+ "(f \<longlongrightarrow> (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> \<bar>l\<bar>) 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 \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) F"
+ "(f \<longlongrightarrow> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> 0) F"
by (fold real_norm_def, rule tendsto_norm_zero)
lemma tendsto_rabs_zero_cancel:
- "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) F \<Longrightarrow> (f ---> 0) F"
+ "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<Longrightarrow> (f \<longlongrightarrow> 0) F"
by (fold real_norm_def, rule tendsto_norm_zero_cancel)
lemma tendsto_rabs_zero_iff:
- "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) F \<longleftrightarrow> (f ---> 0) F"
+ "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F"
by (fold real_norm_def, rule tendsto_norm_zero_iff)
subsubsection \<open>Addition and subtraction\<close>
lemma tendsto_add [tendsto_intros]:
fixes a b :: "'a::real_normed_vector"
- shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 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 :: "_ \<Rightarrow> 'b::real_normed_vector"
- shows "\<lbrakk>(f ---> 0) F; (g ---> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> 0) F; (g \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 0) F"
by (drule (1) tendsto_add, simp)
lemma tendsto_minus [tendsto_intros]:
fixes a :: "'a::real_normed_vector"
- shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) F"
+ shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. - f x) \<longlongrightarrow> - 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 "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
+ shows "((\<lambda>x. - f x) \<longlongrightarrow> - a) F \<Longrightarrow> (f \<longlongrightarrow> a) F"
by (drule tendsto_minus, simp)
lemma tendsto_minus_cancel_left:
- "(f ---> - (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x. - f x) ---> y) F"
+ "(f \<longlongrightarrow> - (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x. - f x) \<longlongrightarrow> 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 "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) \<longlongrightarrow> a - b) F"
using tendsto_add [of f a F "\<lambda>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 \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
- assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) F"
- shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) F"
+ assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
+ shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>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 \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
+ "(g \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) \<longlongrightarrow> 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 \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
+ "(g \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) \<longlongrightarrow> 0) F"
by (drule tendsto, simp only: zero)
lemma (in bounded_bilinear) tendsto:
- "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) F"
+ "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) \<longlongrightarrow> 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 "((\<lambda>x. f x ** g x) ---> 0) F"
+ assumes f: "(f \<longlongrightarrow> 0) F"
+ assumes g: "(g \<longlongrightarrow> 0) F"
+ shows "((\<lambda>x. f x ** g x) \<longlongrightarrow> 0) F"
using tendsto [OF f g] by (simp add: zero_left)
lemma (in bounded_bilinear) tendsto_left_zero:
- "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. f x ** c) ---> 0) F"
+ "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x ** c) \<longlongrightarrow> 0) F"
by (rule bounded_linear.tendsto_zero [OF bounded_linear_left])
lemma (in bounded_bilinear) tendsto_right_zero:
- "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) F"
+ "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) \<longlongrightarrow> 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 \<Longrightarrow> ((\<lambda>x. c * (f x)) ---> c * l) F"
+ shows "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) \<longlongrightarrow> c * l) F"
by (rule tendsto_mult [OF tendsto_const])
lemma tendsto_mult_right:
fixes c::"'a::real_normed_algebra"
- shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) ---> l * c) F"
+ shows "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) \<longlongrightarrow> 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 \<Rightarrow> 'b::{power,real_normed_algebra}"
- shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
+ shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 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 \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
- assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) F"
- shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) F"
+ assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F"
+ shows "((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>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:
- "((\<lambda>x. of_real (f x) :: 'a :: real_normed_div_algebra) ---> of_real c) F \<longleftrightarrow> (f ---> c) F"
+ "((\<lambda>x. of_real (f x) :: 'a :: real_normed_div_algebra) \<longlongrightarrow> of_real c) F \<longleftrightarrow> (f \<longlongrightarrow> c) F"
unfolding tendsto_iff by simp
lemma tendsto_add_const_iff:
- "((\<lambda>x. c + f x :: 'a :: real_normed_vector) ---> c + d) F \<longleftrightarrow> (f ---> d) F"
+ "((\<lambda>x. c + f x :: 'a :: real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
using tendsto_add[OF tendsto_const[of c], of f d]
tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>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 \<longlongrightarrow> a) F"
assumes a: "a \<noteq> 0"
shows "Bfun (\<lambda>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 \<longlongrightarrow> a) F"
assumes a: "a \<noteq> 0"
- shows "((\<lambda>x. inverse (f x)) ---> inverse a) F"
+ shows "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse a) F"
proof -
from a have "0 < norm a" by simp
with f have "eventually (\<lambda>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 "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F; b \<noteq> 0\<rbrakk>
+ \<Longrightarrow> ((\<lambda>x. f x / g x) \<longlongrightarrow> 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 "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> 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 \<noteq> bot"
- assumes "(f ---> (c :: 'a :: real_normed_vector)) F"
+ assumes "(f \<longlongrightarrow> (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 :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
- shows "(inverse ---> (0::'a)) at_infinity"
+ shows "(inverse \<longlongrightarrow> (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 \<longlongrightarrow> (c :: 'b :: real_normed_vector)) (F :: 'a filter)"
assumes "filterlim g at_infinity F"
shows "filterlim (\<lambda>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 "((\<lambda>x. norm (f x)) ---> norm c) F" by (rule tendsto_norm)
+ from assms(1) have "((\<lambda>x. norm (f x)) \<longlongrightarrow> norm c) F" by (rule tendsto_norm)
hence "eventually (\<lambda>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 (\<lambda>x. norm (g x) \<ge> 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 \<longlongrightarrow> (c :: 'b :: real_normed_vector)) (F :: 'a filter)"
shows "filterlim (\<lambda>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 \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
+ "(f \<longlongrightarrow> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> 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 \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
+ "(f \<longlongrightarrow> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> 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 \<noteq> bot" "(f ---> (c :: 'a :: real_normed_field)) F" "c \<noteq> 0"
+ assumes "F \<noteq> bot" "(f \<longlongrightarrow> (c :: 'a :: real_normed_field)) F" "c \<noteq> 0"
assumes "filterlim g at_infinity F"
shows "filterlim (\<lambda>x. f x * g x) at_infinity F"
proof -
- have "((\<lambda>x. inverse (f x) * inverse (g x)) ---> inverse c * 0) F"
+ have "((\<lambda>x. inverse (f x) * inverse (g x)) \<longlongrightarrow> inverse c * 0) F"
by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
hence "filterlim (\<lambda>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 \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
+lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 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 \<Longrightarrow> filterlim (\<lambda>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 \<longlongrightarrow> (0::'a)) at_infinity"
by (fact tendsto_inverse_0)
then show "filtermap inverse at_infinity \<le> 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 \<longleftrightarrow> ((f o inverse) ---> l) (at (0::'a))"
+ shows "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> ((f o inverse) \<longlongrightarrow> 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 "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (f ---> l) at_infinity"
+ shows "((\<lambda>x. f(1 / x)) \<longlongrightarrow> l) (at (0::'a)) \<Longrightarrow> (f \<longlongrightarrow> l) at_infinity"
by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
@@ -1316,7 +1316,7 @@
\<close>
lemma filterlim_tendsto_pos_mult_at_top:
- assumes f: "(f ---> c) F" and c: "0 < c"
+ assumes f: "(f \<longlongrightarrow> 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 \<longlongrightarrow> 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 "\<lambda>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 \<longlongrightarrow> 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 "\<lambda>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 "\<lambda>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 \<longlongrightarrow> 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 \<Rightarrow> real"
- assumes f: "(f ---> a) F" "0 < a"
- assumes g: "(g ---> 0) F" "eventually (\<lambda>x. 0 < g x) F"
+ assumes f: "(f \<longlongrightarrow> a) F" "0 < a"
+ assumes g: "(g \<longlongrightarrow> 0) F" "eventually (\<lambda>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 :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}"
- assumes f: "(f ---> c) F"
+ assumes f: "(f \<longlongrightarrow> c) F"
assumes g: "LIM x F. g x :> at_infinity"
- shows "((\<lambda>x. f x / g x) ---> 0) F"
+ shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 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 "\<lbrakk>(g ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (f ---> a) F"
+ shows "\<lbrakk>(g \<longlongrightarrow> a) F; ((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> (f \<longlongrightarrow> a) F"
using tendsto_add [of g a F "\<lambda>x. f x - g x" 0] by simp
lemma Lim_transform2:
fixes a b :: "'a::real_normed_vector"
- shows "\<lbrakk>(f ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (g ---> a) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> a) F; ((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> (g \<longlongrightarrow> a) F"
by (erule Lim_transform) (simp add: tendsto_minus_cancel)
lemma Lim_transform_eventually:
- "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
+ "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> (g \<longlongrightarrow> 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 "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f ---> l) (at x within S)"
- shows "(g ---> l) (at x within S)"
+ and "(f \<longlongrightarrow> l) (at x within S)"
+ shows "(g \<longlongrightarrow> l) (at x within S)"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>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 \<longlongrightarrow> l) (at x within S)" by fact
qed
lemma Lim_transform_at:
assumes "0 < d"
and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f ---> l) (at x)"
- shows "(g ---> l) (at x)"
+ and "(f \<longlongrightarrow> l) (at x)"
+ shows "(g \<longlongrightarrow> l) (at x)"
using _ assms(3)
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>x. f x = g x) (at x)"
@@ -1554,10 +1554,10 @@
fixes a b :: "'a::t1_space"
assumes "a \<noteq> b"
and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
- and "(f ---> l) (at a within S)"
- shows "(g ---> l) (at a within S)"
+ and "(f \<longlongrightarrow> l) (at a within S)"
+ shows "(g \<longlongrightarrow> l) (at a within S)"
proof (rule Lim_transform_eventually)
- show "(f ---> l) (at a within S)" by fact
+ show "(f \<longlongrightarrow> l) (at a within S)" by fact
show "eventually (\<lambda>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\<noteq>b"
and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
- and fl: "(f ---> l) (at a)"
- shows "(g ---> l) (at a)"
+ and fl: "(f \<longlongrightarrow> l) (at a)"
+ shows "(g \<longlongrightarrow> l) (at a)"
using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
text\<open>Alternatively, within an open set.\<close>
@@ -1576,13 +1576,13 @@
lemma Lim_transform_within_open:
assumes "open S" and "a \<in> S"
and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
- and "(f ---> l) (at a)"
- shows "(g ---> l) (at a)"
+ and "(f \<longlongrightarrow> l) (at a)"
+ shows "(g \<longlongrightarrow> l) (at a)"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>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 \<longlongrightarrow> l) (at a)" by fact
qed
text\<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
@@ -1594,14 +1594,14 @@
and "x = y"
and "S = T"
and "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
- shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
+ shows "(f \<longlongrightarrow> x) (at a within S) \<longleftrightarrow> (g \<longlongrightarrow> 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 "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
- shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
+ shows "((\<lambda>x. f x) \<longlongrightarrow> x) (at a) \<longleftrightarrow> ((g \<longlongrightarrow> y) (at a))"
unfolding tendsto_def eventually_at_topological
using assms by simp
text\<open>An unbounded sequence's inverse tends to 0\<close>
@@ -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: "((\<lambda>n. 1 / of_nat n) ---> (0::'a::real_normed_field)) sequentially"
+lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (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 \<ge> nat \<lceil>inverse e + 1\<rceil>"
@@ -1646,7 +1646,7 @@
by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
qed
-lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially"
+lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
using lim_1_over_n by (simp add: inverse_eq_divide)
lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
@@ -1979,17 +1979,17 @@
lemma LIM_zero:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
+ shows "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F"
unfolding tendsto_iff dist_norm by simp
lemma LIM_zero_cancel:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
+ shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F"
unfolding tendsto_iff dist_norm by simp
lemma LIM_zero_iff:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
+ shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F"
unfolding tendsto_iff dist_norm by simp
lemma LIM_imp_LIM:
@@ -2152,7 +2152,7 @@
assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
shows "0 \<le> f x"
proof (rule tendsto_le_const)
- show "(f ---> f x) (at_left x)"
+ show "(f \<longlongrightarrow> f x) (at_left x)"
using \<open>isCont f x\<close> by (simp add: filterlim_at_split isCont_def)
show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"])
--- 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 \<Rightarrow>\<^sub>L 'b::real_normed_vector"
and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
- assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) ---> a j) F)"
- shows "(b ---> a) F"
+ assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) \<longlongrightarrow> a j) F)"
+ shows "(b \<longlongrightarrow> a) F"
proof -
have "\<And>j. j \<in> Basis \<Longrightarrow> Zfun (\<lambda>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 "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) ---> a i j) F"
- shows "((\<lambda>n. blinfun_of_matrix (b n)) ---> blinfun_of_matrix a) F"
+ assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) \<longlongrightarrow> a i j) F"
+ shows "((\<lambda>n. blinfun_of_matrix (b n)) \<longlongrightarrow> blinfun_of_matrix a) F"
proof -
have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>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 \<Rightarrow>\<^sub>L 'b::euclidean_space"
and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
- shows "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j \<bullet> i) ---> a j \<bullet> i) F) \<Longrightarrow> (b ---> a) F"
+ shows "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j \<bullet> i) \<longlongrightarrow> a j \<bullet> i) F) \<Longrightarrow> (b \<longlongrightarrow> 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: "((\<lambda>i. f (r1 (r2 i)) k) ---> l2) sequentially"
+ and lr2: "((\<lambda>i. f (r1 (r2 i)) k) \<longlongrightarrow> l2) sequentially"
using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) k"]
by (auto simp: o_def)
def r \<equiv> "r1 \<circ> r2"
@@ -585,9 +585,9 @@
ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
using eventually_elim2 by force
}
- then have *: "((f \<circ> r) ---> l) sequentially"
+ then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
by auto
qed
--- 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 (\<lambda>i. f (r1 i) $ k))"
by (metis (lifting) bounded_subset image_subsetI f' s')
then obtain l2 r2 where r2: "subseq r2"
- and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially"
+ and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) \<longlongrightarrow> l2) sequentially"
using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"] by (auto simp: o_def)
def r \<equiv> "r1 \<circ> r2"
have r: "subseq r"
@@ -888,8 +888,8 @@
ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
by (rule eventually_mono)
}
- hence "((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
+ hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp
+ with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
qed
lemma interval_cart:
@@ -1014,19 +1014,19 @@
lemma Lim_component_le_cart:
fixes f :: "'a \<Rightarrow> real^'n"
- assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f x $i \<le> b) net"
+ assumes "(f \<longlongrightarrow> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f x $i \<le> b) net"
shows "l$i \<le> 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 \<Rightarrow> real^'n"
- assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. b \<le> (f x)$i) net"
+ assumes "(f \<longlongrightarrow> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. b \<le> (f x)$i) net"
shows "b \<le> 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 \<Rightarrow> real^'n"
- assumes net: "(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$i = b) net"
+ assumes net: "(f \<longlongrightarrow> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>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
--- 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 "\<exists>d>0. \<forall>y\<in>s. y \<noteq> x \<and> cmod (y-x) < d \<longrightarrow> cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
using d1 by blast
}
- then have *: "((\<lambda>y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) ---> 0) (at x within s)"
+ then have *: "((\<lambda>y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) \<longlongrightarrow> 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: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
and \<gamma>: "valid_path \<gamma>"
and [simp]: "~ (trivial_limit F)"
- shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
+ shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
proof -
have "0 \<le> 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 "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
+ then show "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
by (rule tendstoI)
qed
@@ -5300,7 +5300,7 @@
assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on (circlepath z r)) F"
and ev_no: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> 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)" "((\<lambda>n. contour_integral (circlepath z r) (f n)) ---> contour_integral (circlepath z r) l) F"
+ shows "l contour_integrable_on (circlepath z r)" "((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> 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\<open> These weak Liouville versions don't even need the derivative formula.\<close>
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 \<longlongrightarrow> 0) at_infinity"
shows "f z = 0"
proof (rule ccontr)
assume fz: "f z \<noteq> 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 \<longlongrightarrow> l) at_infinity"
shows "f z = l"
using Liouville_weak_0 [of "\<lambda>z. f z - l"]
by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero)
@@ -6195,7 +6195,7 @@
{ assume f: "\<And>z. f z \<noteq> 0"
have 1: "(\<lambda>x. 1 / f x) holomorphic_on UNIV"
by (simp add: holomorphic_on_divide holomorphic_on_const assms f)
- have 2: "((\<lambda>x. 1 / f x) ---> 0) at_infinity"
+ have 2: "((\<lambda>x. 1 / f x) \<longlongrightarrow> 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: "(\<lambda>u. g u/(u - w)) contour_integrable_on circlepath z r"
by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
- have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) ---> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
+ have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) \<longlongrightarrow> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
- have f_tends_cig: "((\<lambda>n. 2 * of_real pi * ii * f n w) ---> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
+ have f_tends_cig: "((\<lambda>n. 2 * of_real pi * ii * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>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 "((\<lambda>n. 2 * of_real pi * \<i> * f n w) ---> 2 * of_real pi * \<i> * g w) F"
+ have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> 2 * of_real pi * \<i> * 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"
- "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) ---> g' w) F"
+ "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> 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: "\<And>x. x \<in> ball z r \<Longrightarrow> deriv g x = g' x"
by (simp add: DERIV_imp_deriv)
- have tends_f'n_g': "((\<lambda>n. f' n w) ---> g' w) F" if w: "w \<in> ball z r" for w
+ have tends_f'n_g': "((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F" if w: "w \<in> ball z r" for w
proof -
have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)"
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 "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2))
- ---> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
+ \<longlongrightarrow> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \<open>0 < r\<close>])
- then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) ---> 0) F"
+ then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) \<longlongrightarrow> 0) F"
using Lim_null by (force intro!: tendsto_mult_right_zero)
- have "((\<lambda>n. f' n w - g' w) ---> 0) F"
+ have "((\<lambda>n. f' n w - g' w) \<longlongrightarrow> 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 "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) ---> g' w) F"
+ obtain g' where "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F"
by (blast intro: tends_f'n_g' g' )
then show ?thesis using g
using that by blast
--- 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 \<longlongrightarrow> l) F"
"eventually (\<lambda>x. Re(f x) \<le> b) F"
shows "Re(l) \<le> b"
by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Re)
lemma tendsto_Re_lower:
assumes "~ (trivial_limit F)"
- "(f ---> l) F"
+ "(f \<longlongrightarrow> l) F"
"eventually (\<lambda>x. b \<le> Re(f x)) F"
shows "b \<le> Re(l)"
by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Re)
lemma tendsto_Im_upper:
assumes "~ (trivial_limit F)"
- "(f ---> l) F"
+ "(f \<longlongrightarrow> l) F"
"eventually (\<lambda>x. Im(f x) \<le> b) F"
shows "Im(l) \<le> b"
by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Im)
lemma tendsto_Im_lower:
assumes "~ (trivial_limit F)"
- "(f ---> l) F"
+ "(f \<longlongrightarrow> l) F"
"eventually (\<lambda>x. b \<le> Im(f x)) F"
shows "b \<le> 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 "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
+ assumes "(f \<longlongrightarrow> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
shows "l \<in> \<real>"
proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
show "eventually (\<lambda>x. f x \<in> \<real>) F"
@@ -246,7 +246,7 @@
lemma real_lim_sequentially:
fixes l::complex
- shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
+ shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
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 (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g ---> 0) F" shows "(f ---> 0) F"
+ assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
subsection\<open>Holomorphic functions\<close>
@@ -812,11 +812,11 @@
assumes cvs: "convex s"
and df: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s \<longrightarrow> norm (f' n x - g' x) \<le> e"
- and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) ---> l) sequentially"
- shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) ---> g x) sequentially \<and>
+ and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially"
+ shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and>
(g has_field_derivative (g' x)) (at x within s)"
proof -
- from assms obtain x l where x: "x \<in> s" and tf: "((\<lambda>n. f n x) ---> l) sequentially"
+ from assms obtain x l where x: "x \<in> s" and tf: "((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially"
by blast
{ fix e::real assume e: "e > 0"
then obtain N where N: "\<forall>n\<ge>N. \<forall>x. x \<in> s \<longrightarrow> cmod (f' n x - g' x) \<le> e"
--- 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 "((\<lambda>n. Ln n / (n powr s)) ---> 0) sequentially"
+ shows "((\<lambda>n. Ln n / (n powr s)) \<longlongrightarrow> 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: "((\<lambda>n. Ln(of_nat n) / of_nat n) ---> 0) sequentially"
+lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 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 "((\<lambda>n. ln n / (n powr s)) ---> 0) sequentially"
+ shows "((\<lambda>n. ln n / (n powr s)) \<longlongrightarrow> 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: "((\<lambda>n. ln(real_of_nat n) / of_nat n) ---> 0) sequentially"
+lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 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 "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
+ shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 0) sequentially"
proof -
have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> 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 "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
+ shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 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: "((\<lambda>n. 1 / Ln(of_nat n)) ---> 0) sequentially"
+lemma lim_1_over_Ln: "((\<lambda>n. 1 / Ln(of_nat n)) \<longlongrightarrow> 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: "((\<lambda>n. 1 / ln(real_of_nat n)) ---> 0) sequentially"
+lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) \<longlongrightarrow> 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)
--- 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 \<open>These are the only cases we'll care about, probably.\<close>
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
- bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
+ bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 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) \<longleftrightarrow>
- bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
+ bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
using has_derivative_within [of f f' x UNIV]
by simp
@@ -111,14 +111,14 @@
fixes f :: "real \<Rightarrow> real"
and y :: "real"
shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
- ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x <..} \<inter> I))"
+ ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
proof -
- have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
- ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
+ have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
+ ((\<lambda>t. (f t - f x) / (t - x) - y) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I))"
by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
- also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> I))"
by (simp add: Lim_null[symmetric])
- also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x<..} \<inter> 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 \<open>Caratheodory characterization\<close>
lemma DERIV_within_iff:
- "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
+ "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) \<longlongrightarrow> D) (at a within s)"
proof -
have 1: "\<And>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 \<open>a < x2\<close>
by (auto simp: trivial_limit_within islimpt_in_closure)
moreover
- have "((\<lambda>x1. (\<phi> x1 - \<phi> a) + e * (x1 - a) + e) ---> (\<phi> x2 - \<phi> a) + e * (x2 - a) + e) (at x2 within {a <..<x2})"
- "((\<lambda>x1. norm (f x1 - f a)) ---> norm (f x2 - f a)) (at x2 within {a <..<x2})"
+ have "((\<lambda>x1. (\<phi> x1 - \<phi> a) + e * (x1 - a) + e) \<longlongrightarrow> (\<phi> x2 - \<phi> a) + e * (x2 - a) + e) (at x2 within {a <..<x2})"
+ "((\<lambda>x1. norm (f x1 - f a)) \<longlongrightarrow> norm (f x2 - f a)) (at x2 within {a <..<x2})"
using a
by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
intro: tendsto_within_subset[where S="{a .. b}"])
@@ -1899,13 +1899,13 @@
and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
and "x0 \<in> s"
- and "((\<lambda>n. f n x0) ---> l) sequentially"
- shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially \<and> (g has_derivative g'(x)) (at x within s)"
+ and "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
+ shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g'(x)) (at x within s)"
proof -
have lem1: "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
using assms(1,2,3) by (rule has_derivative_sequence_lipschitz)
- have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially"
+ have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
apply (rule bchoice)
unfolding convergent_eq_cauchy
proof
@@ -1970,7 +1970,7 @@
proof rule+
fix n x y
assume as: "N \<le> n" "x \<in> s" "y \<in> s"
- have "((\<lambda>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 "((\<lambda>m. norm (f n x - f n y - (f m x - f m y))) \<longlongrightarrow> norm (f n x - f n y - (g x - g y))) sequentially"
by (intro tendsto_intros g[rule_format] as)
moreover have "eventually (\<lambda>m. norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)) sequentially"
unfolding eventually_sequentially
@@ -1988,14 +1988,14 @@
by (rule tendsto_ge_const[OF trivial_limit_sequentially])
qed
qed
- have "\<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
+ have "\<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
unfolding has_derivative_within_alt2
proof (intro ballI conjI)
fix x
assume "x \<in> s"
- then show "((\<lambda>n. f n x) ---> g x) sequentially"
+ then show "((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
by (simp add: g)
- have lem3: "\<forall>u. ((\<lambda>n. f' n x u) ---> g' x u) sequentially"
+ have lem3: "\<forall>u. ((\<lambda>n. f' n x u) \<longlongrightarrow> 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 \<in> interior A \<inter> closure {c<..}" by auto
also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_inter_closure_subset) auto
finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
- moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
+ moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> 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 (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
@@ -2576,7 +2576,7 @@
from c have "c \<in> interior A \<inter> closure {..<c}" by auto
also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_inter_closure_subset) auto
finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
- moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
+ moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> 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 (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
--- 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 \<Longrightarrow> at x within {0 ..} = at x"
using at_within_interior[of x "{0 ..}"] by (simp add: interior_Ici[of "- \<infinity>"])
- ultimately show "(inverse ---> inverse x) (at x within {0..})"
+ ultimately show "(inverse \<longlongrightarrow> inverse x) (at x within {0..})"
by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos)
qed
--- 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 "((\<lambda>x. f x) ---> a) net"
- shows "((\<lambda>x. f x $ i) ---> a $ i) net"
+ assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net"
+ shows "((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
proof (rule topological_tendstoI)
fix S assume "open S" "a $ i \<in> S"
then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
@@ -212,8 +212,8 @@
unfolding isCont_def by (rule tendsto_vec_nth)
lemma vec_tendstoI:
- assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net"
- shows "((\<lambda>x. f x) ---> a) net"
+ assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
+ shows "((\<lambda>x. f x) \<longlongrightarrow> a) net"
proof (rule topological_tendstoI)
fix S assume "open S" and "a \<in> S"
then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i"
@@ -228,8 +228,8 @@
qed
lemma tendsto_vec_lambda [tendsto_intros]:
- assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net"
- shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net"
+ assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net"
+ shows "((\<lambda>x. \<chi> i. f x i) \<longlongrightarrow> (\<chi> i. a i)) net"
using assms by (simp add: vec_tendstoI)
lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
--- 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 \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on cbox a b"
and "\<forall>k. \<forall>x\<in>cbox a b.(f k x) \<le> f (Suc k) x"
- and "\<forall>x\<in>cbox a b. ((\<lambda>k. f k x) ---> g x) sequentially"
+ and "\<forall>x\<in>cbox a b. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
and "bounded {integral (cbox a b) (f k) | k . k \<in> UNIV}"
- shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) ---> integral (cbox a b) g) sequentially"
+ shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> 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 "\<exists>i. ((\<lambda>k. integral (cbox a b) (f k)) ---> i) sequentially"
+ have "\<exists>i. ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> i) sequentially"
apply (rule bounded_increasing_convergent)
defer
apply rule
@@ -9935,15 +9935,15 @@
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on s"
and "\<forall>k. \<forall>x\<in>s. (f k x) \<le> (f (Suc k) x)"
- and "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially"
+ and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
and "bounded {integral s (f k)| k. True}"
- shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
-proof -
- have lem: "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+ shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+proof -
+ have lem: "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
if "\<forall>k. \<forall>x\<in>s. 0 \<le> f k x"
and "\<forall>k. (f k) integrable_on s"
and "\<forall>k. \<forall>x\<in>s. f k x \<le> f (Suc k) x"
- and "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially"
+ and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
and "bounded {integral s (f k)| k. True}"
for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g s
proof -
@@ -9962,7 +9962,7 @@
done
note fg=this[rule_format]
- have "\<exists>i. ((\<lambda>k. integral s (f k)) ---> i) sequentially"
+ have "\<exists>i. ((\<lambda>k. integral s (f k)) \<longlongrightarrow> i) sequentially"
apply (rule bounded_increasing_convergent)
apply (rule that(5))
apply rule
@@ -10004,7 +10004,7 @@
apply (rule int)
done
have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
- ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) --->
+ ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) \<longlongrightarrow>
integral (cbox a b) (\<lambda>x. if x \<in> 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 "(\<lambda>x. g x - f 0 x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) --->
+ have "(\<lambda>x. g x - f 0 x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
integral s (\<lambda>x. g x - f 0 x)) sequentially"
apply (rule lem)
apply safe
@@ -10225,9 +10225,9 @@
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on s"
and "\<forall>k. \<forall>x\<in>s. f (Suc k) x \<le> f k x"
- and "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially"
+ and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
and "bounded {integral s (f k)| k. True}"
- shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+ shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
proof -
note assm = assms[rule_format]
have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}"
@@ -10240,7 +10240,7 @@
apply auto
done
have "(\<lambda>x. - g x) integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. - f k x)) ---> integral s (\<lambda>x. - g x)) sequentially"
+ ((\<lambda>k. integral s (\<lambda>x. - f k x)) \<longlongrightarrow> integral s (\<lambda>x. - g x)) sequentially"
apply (rule monotone_convergence_increasing)
apply safe
apply (rule integrable_neg)
@@ -11842,7 +11842,7 @@
obtains I J where
"\<And>n. (f n has_integral I n) (cbox a b)"
"(g has_integral J) (cbox a b)"
- "(I ---> J) F"
+ "(I \<longlongrightarrow> 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 \<longlongrightarrow> J) F"
proof cases
assume "content (cbox a b) = 0"
hence "I = (\<lambda>_. 0)" "J = 0"
@@ -11906,9 +11906,9 @@
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
- and "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
+ and "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
shows "g integrable_on s"
- and "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+ and "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
proof -
have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
proof (safe intro!: bdd_belowI)
@@ -11922,7 +11922,7 @@
qed
have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
+ ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
proof (rule monotone_convergence_decreasing, safe)
fix m :: nat
@@ -11962,7 +11962,7 @@
show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
by (rule cInf_superset_mono) auto
let ?S = "{f j x| j. m \<le> j}"
- show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
+ show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Inf ?S) sequentially"
proof (rule LIMSEQ_I, goal_cases)
case r: (1 r)
@@ -11993,7 +11993,7 @@
note dec1 = conjunctD2[OF this]
have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) --->
+ ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
proof (rule monotone_convergence_increasing,safe)
fix m :: nat
@@ -12033,7 +12033,7 @@
show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
by (rule cSup_subset_mono) auto
let ?S = "{f j x| j. m \<le> j}"
- show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
+ show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Sup ?S) sequentially"
proof (rule LIMSEQ_I, goal_cases)
case r: (1 r)
have "\<exists>y\<in>?S. Sup ?S - r < y"
@@ -12062,7 +12062,7 @@
note inc1 = conjunctD2[OF this]
have "g integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+ ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<longlongrightarrow> 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 \<and>
- ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+ ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
apply (rule monotone_convergence_decreasing,safe)
apply fact
proof -
@@ -12135,7 +12135,7 @@
show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
- show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
+ show "((\<lambda>k. Sup {f j x |j. k \<le> j}) \<longlongrightarrow> g x) sequentially"
proof (rule LIMSEQ_I, goal_cases)
case r: (1 r)
then have "0<r/2"
@@ -12157,7 +12157,7 @@
note dec2 = conjunctD2[OF this]
show "g integrable_on s" by fact
- show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+ show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> 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]
--- 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 "((\<lambda>x. infnorm (f x)) ---> infnorm a) F"
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. infnorm (f x)) \<longlongrightarrow> infnorm a) F"
proof (rule tendsto_compose [OF LIM_I assms])
fix r :: real
assume "r > 0"
--- 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 \<Rightarrow> 'b::topological_space"
- shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
+ shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
by (fact tendsto_within_open)
lemma continuous_on_union:
@@ -2293,48 +2293,48 @@
subsection \<open>Limits\<close>
lemma Lim:
- "(f ---> l) net \<longleftrightarrow>
+ "(f \<longlongrightarrow> l) net \<longleftrightarrow>
trivial_limit net \<or>
(\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
unfolding tendsto_iff trivial_limit_eq by auto
text\<open>Show that they yield usual definitions in the various cases.\<close>
-lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
+lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> 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) \<longleftrightarrow>
+lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp add: tendsto_iff eventually_at dist_nz)
-lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
+lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp add: tendsto_iff eventually_at2)
lemma Lim_at_infinity:
- "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
+ "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
by (auto simp add: tendsto_iff eventually_at_infinity)
-lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
+lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
by (rule topological_tendstoI, auto elim: eventually_mono)
text\<open>The expected monotonicity property.\<close>
lemma Lim_Un:
- assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
- shows "(f ---> l) (at x within (S \<union> T))"
+ assumes "(f \<longlongrightarrow> l) (at x within S)" "(f \<longlongrightarrow> l) (at x within T)"
+ shows "(f \<longlongrightarrow> l) (at x within (S \<union> T))"
using assms unfolding at_within_union by (rule filterlim_sup)
lemma Lim_Un_univ:
- "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>
- S \<union> T = UNIV \<Longrightarrow> (f ---> l) (at x)"
+ "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T) \<Longrightarrow>
+ S \<union> T = UNIV \<Longrightarrow> (f \<longlongrightarrow> l) (at x)"
by (metis Lim_Un)
text\<open>Interrelations between restricted and unrestricted limits.\<close>
lemma Lim_at_imp_Lim_at_within:
- "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
+ "(f \<longlongrightarrow> l) (at x) \<Longrightarrow> (f \<longlongrightarrow> 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 "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L"
- shows "(X ---> L) (at a within T)"
+ shows "(X \<longlongrightarrow> 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: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
- shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
+ shows "(f \<longlongrightarrow> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
proof (cases "{x<..} \<inter> 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 \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f ---> x) sequentially)"
+ shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -2456,13 +2456,13 @@
lemma Lim_null:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net"
+ shows "(f \<longlongrightarrow> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) \<longlongrightarrow> 0) net"
by (simp add: Lim dist_norm)
lemma Lim_null_comparison:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net"
- shows "(f ---> 0) net"
+ assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g \<longlongrightarrow> 0) net"
+ shows "(f \<longlongrightarrow> 0) net"
using assms(2)
proof (rule metric_tendsto_imp_tendsto)
show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
@@ -2473,8 +2473,8 @@
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
and g :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) net"
- and "(g ---> 0) net"
- shows "(f ---> 0) net"
+ and "(g \<longlongrightarrow> 0) net"
+ shows "(f \<longlongrightarrow> 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 (\<lambda>x. f(x) \<in> S) net"
- and "\<not> trivial_limit net" "(f ---> l) net"
+ and "\<not> trivial_limit net" "(f \<longlongrightarrow> l) net"
shows "l \<in> S"
proof (rule ccontr)
assume "l \<notin> S"
@@ -2501,21 +2501,21 @@
lemma Lim_dist_ubound:
assumes "\<not>(trivial_limit net)"
- and "(f ---> l) net"
+ and "(f \<longlongrightarrow> l) net"
and "eventually (\<lambda>x. dist a (f x) \<le> e) net"
shows "dist a l \<le> e"
using assms by (fast intro: tendsto_le tendsto_intros)
lemma Lim_norm_ubound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net"
+ assumes "\<not>(trivial_limit net)" "(f \<longlongrightarrow> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net"
shows "norm(l) \<le> e"
using assms by (fast intro: tendsto_le tendsto_intros)
lemma Lim_norm_lbound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "\<not> trivial_limit net"
- and "(f ---> l) net"
+ and "(f \<longlongrightarrow> l) net"
and "eventually (\<lambda>x. e \<le> norm (f x)) net"
shows "e \<le> norm l"
using assms by (fast intro: tendsto_le tendsto_intros)
@@ -2523,25 +2523,25 @@
text\<open>Limit under bilinear function\<close>
lemma Lim_bilinear:
- assumes "(f ---> l) net"
- and "(g ---> m) net"
+ assumes "(f \<longlongrightarrow> l) net"
+ and "(g \<longlongrightarrow> m) net"
and "bounded_bilinear h"
- shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
- using \<open>bounded_bilinear h\<close> \<open>(f ---> l) net\<close> \<open>(g ---> m) net\<close>
+ shows "((\<lambda>x. h (f x) (g x)) \<longlongrightarrow> (h l m)) net"
+ using \<open>bounded_bilinear h\<close> \<open>(f \<longlongrightarrow> l) net\<close> \<open>(g \<longlongrightarrow> m) net\<close>
by (rule bounded_bilinear.tendsto)
text\<open>These are special for limits out of the same vector space.\<close>
-lemma Lim_within_id: "(id ---> a) (at a within s)"
+lemma Lim_within_id: "(id \<longlongrightarrow> 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 \<longlongrightarrow> 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) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)"
+ shows "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) \<longlongrightarrow> l) (at 0)"
using LIM_offset_zero LIM_offset_zero_cancel ..
text\<open>It's also sometimes useful to extract the limit point from the filter.\<close>
@@ -2558,7 +2558,7 @@
using netlimit_within [of a UNIV] by simp
lemma lim_within_interior:
- "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
+ "x \<in> interior S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S) \<longleftrightarrow> (f \<longlongrightarrow> 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 \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)"
+ shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x \<longlongrightarrow> 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 \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
+ shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x \<longlongrightarrow> l) sequentially \<longrightarrow> l \<in> 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 "((\<lambda>x. infdist (f x) A) ---> infdist l A) F"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> 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 \<Longrightarrow> ((\<lambda>i. f(i - k)) ---> l) sequentially"
+ "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) \<longlongrightarrow> l) sequentially"
apply (erule filterlim_compose)
apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially)
apply arith
done
-lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
+lemma seq_harmonic: "((\<lambda>n. inverse (real n)) \<longlongrightarrow> 0) sequentially"
using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) (* TODO: move to Limits.thy *)
subsection \<open>More properties of closed balls\<close>
@@ -3224,7 +3224,7 @@
{
fix y
assume "y \<in> closure S"
- then obtain f where f: "\<forall>n. f n \<in> S" "(f ---> y) sequentially"
+ then obtain f where f: "\<forall>n. f n \<in> S" "(f \<longlongrightarrow> y) sequentially"
unfolding closure_sequential by auto
have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
@@ -3567,7 +3567,7 @@
lemma sequence_infinite_lemma:
fixes f :: "nat \<Rightarrow> 'a::t1_space"
assumes "\<forall>n. f n \<noteq> l"
- and "(f ---> l) sequentially"
+ and "(f \<longlongrightarrow> l) sequentially"
shows "infinite (range f)"
proof
assume "finite (range f)"
@@ -3664,7 +3664,7 @@
lemma sequence_unique_limpt:
fixes f :: "nat \<Rightarrow> 'a::t2_space"
- assumes "(f ---> l) sequentially"
+ assumes "(f \<longlongrightarrow> l) sequentially"
and "l' islimpt (range f)"
shows "l' = l"
proof (rule ccontr)
@@ -3701,7 +3701,7 @@
proof -
{
fix x l
- assume as: "\<forall>n::nat. x n \<in> s" "(x ---> l) sequentially"
+ assume as: "\<forall>n::nat. x n \<in> s" "(x \<longlongrightarrow> l) sequentially"
then have "l \<in> s"
proof (cases "\<forall>n. x n \<noteq> l")
case False
@@ -3974,16 +3974,16 @@
definition seq_compact :: "'a::topological_space set \<Rightarrow> bool"
where "seq_compact S \<longleftrightarrow>
- (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially))"
+ (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
lemma seq_compactI:
- assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
shows "seq_compact S"
unfolding seq_compact_def using assms by fast
lemma seq_compactE:
assumes "seq_compact S" "\<forall>n. f n \<in> S"
- obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
+ obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
using assms unfolding seq_compact_def by fast
lemma closed_sequentially: (* TODO: move upwards *)
@@ -4184,7 +4184,7 @@
{
fix f :: "nat \<Rightarrow> 'a"
assume f: "\<forall>n. f n \<in> s"
- have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> 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 "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)"
by auto
then obtain l where "l \<in> s" "\<forall>U. l\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" ..
- from this(2) have "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ from this(2) have "\<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
using acc_point_range_imp_convergent_subsequence[of l f] by auto
- with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" ..
+ with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
qed
}
then show ?thesis
@@ -4261,7 +4261,7 @@
qed simp
then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
by blast
- then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
+ then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
using assms by (metis seq_compact_def)
from this(3) have "Cauchy (x \<circ> r)"
using LIMSEQ_imp_Cauchy by auto
@@ -4358,7 +4358,7 @@
class heine_borel = metric_space +
assumes bounded_imp_convergent_subsequence:
- "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
lemma bounded_closed_imp_seq_compact:
fixes s::"'a::heine_borel set"
@@ -4370,13 +4370,13 @@
assume f: "\<forall>n. f n \<in> s"
with \<open>bounded s\<close> have "bounded (range f)"
by (auto intro: bounded_subset)
- obtain l r where r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
+ obtain l r where r: "subseq r" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"
by simp
have "l \<in> s" using \<open>closed s\<close> fr l
by (rule closed_sequentially)
- show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
using \<open>l \<in> s\<close> r l by blast
qed
@@ -4451,7 +4451,7 @@
by simp
have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))"
by (metis (lifting) bounded_subset f' image_subsetI s')
- then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
+ then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) \<longlongrightarrow> l2) sequentially"
using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"]
by (auto simp: o_def)
def r \<equiv> "r1 \<circ> r2"
@@ -4509,9 +4509,9 @@
ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
by (rule eventually_mono)
}
- then have *: "((f \<circ> r) ---> l) sequentially"
+ then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> 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 \<circ> f \<circ> r1))"
by (auto simp add: image_comp intro: bounded_snd bounded_subset)
- obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially"
+ obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
using bounded_imp_convergent_subsequence [OF s2]
unfolding o_def by fast
- have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
+ have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially"
using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
- have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially"
+ have l: "((f \<circ> (r1 \<circ> r2)) \<longlongrightarrow> (l1, l2)) sequentially"
using tendsto_Pair [OF l1' l2] unfolding o_def by simp
have r: "subseq (r1 \<circ> r2)"
using r1 r2 unfolding subseq_def by simp
- show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
using l r by fast
qed
@@ -4601,7 +4601,7 @@
}
then have "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
}
- then have "\<exists>l\<in>s. (f ---> l) sequentially" using \<open>l\<in>s\<close>
+ then have "\<exists>l\<in>s. (f \<longlongrightarrow> l) sequentially" using \<open>l\<in>s\<close>
unfolding lim_sequentially by auto
}
then show ?thesis unfolding complete_def by auto
@@ -4777,7 +4777,7 @@
by (rule compact_imp_complete)
moreover have "\<forall>n. f n \<in> closure (range f)"
using closure_subset [of "range f"] by auto
- ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
+ ultimately have "\<exists>l\<in>closure (range f). (f \<longlongrightarrow> l) sequentially"
using \<open>Cauchy f\<close> 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 \<Rightarrow> 'a::complete_space"
- shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s"
+ shows "(\<exists>l. (s \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy s"
unfolding Cauchy_convergent_iff convergent_def ..
lemma convergent_imp_bounded:
fixes s :: "nat \<Rightarrow> 'a::metric_space"
- shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
+ shows "(s \<longlongrightarrow> l) sequentially \<Longrightarrow> 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 \<longlongrightarrow> 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: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l x) sequentially"
+ then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l x) sequentially"
unfolding convergent_eq_cauchy[symmetric]
- using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l) sequentially"]
+ using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l) sequentially"]
by auto
{
fix e :: real
@@ -5230,7 +5230,7 @@
"continuous (at x) f \<Longrightarrow> 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 \<Longrightarrow> (f ---> l) net"
+lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f \<longlongrightarrow> l) net"
by simp
lemmas continuous_on = continuous_on_def \<comment> "legacy theorem name"
@@ -5253,8 +5253,8 @@
lemma continuous_within_sequentially:
fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a within s) f \<longleftrightarrow>
- (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
- \<longrightarrow> ((f \<circ> x) ---> f a) sequentially)"
+ (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x \<longlongrightarrow> a) sequentially
+ \<longrightarrow> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -5286,14 +5286,14 @@
lemma continuous_at_sequentially:
fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a) f \<longleftrightarrow>
- (\<forall>x. (x ---> a) sequentially --> ((f \<circ> x) ---> f a) sequentially)"
+ (\<forall>x. (x \<longlongrightarrow> a) sequentially --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
using continuous_within_sequentially[of a UNIV f] by simp
lemma continuous_on_sequentially:
fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous_on s f \<longleftrightarrow>
- (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
- --> ((f \<circ> x) ---> f a) sequentially)"
+ (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x \<longlongrightarrow> a) sequentially
+ --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
(is "?lhs = ?rhs")
proof
assume ?rhs
@@ -5311,15 +5311,15 @@
lemma uniformly_continuous_on_sequentially:
"uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
- ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially
- \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs")
+ ((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially
+ \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 0) sequentially)" (is "?lhs = ?rhs")
proof
assume ?lhs
{
fix x y
assume x: "\<forall>n. x n \<in> s"
and y: "\<forall>n. y n \<in> s"
- and xy: "((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially"
+ and xy: "((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially"
{
fix e :: real
assume "e > 0"
@@ -5340,7 +5340,7 @@
then have "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"
by auto
}
- then have "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially"
+ then have "((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 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 \<longlongrightarrow> l) F"
assumes l: "l \<in> s"
assumes ev: "\<forall>\<^sub>F x in F. g x \<in> s"
- shows "((\<lambda>x. f (g x)) ---> f l) F"
+ shows "((\<lambda>x. f (g x)) \<longlongrightarrow> f l) F"
proof -
- from f_cont have f: "(f ---> f l) (at l within s)"
+ from f_cont have f: "(f \<longlongrightarrow> f l) (at l within s)"
by (auto simp: l continuous_on)
- have i: "((\<lambda>x. if g x = l then f l else f (g x)) ---> f l) F"
+ have i: "((\<lambda>x. if g x = l then f l else f (g x)) \<longlongrightarrow> 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 \<longlongrightarrow> 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 \<in> U" and "a \<notin> U"
using t1_space [OF \<open>f x \<noteq> a\<close>] by fast
- have "(f ---> f x) (at x within s)"
+ have "(f \<longlongrightarrow> f x) (at x within s)"
using assms(1) by (simp add: continuous_within)
then have "eventually (\<lambda>y. f y \<in> U) (at x within s)"
using \<open>open U\<close> and \<open>f x \<in> U\<close>
@@ -6015,10 +6015,10 @@
lemma linear_lim_0:
assumes "bounded_linear f"
- shows "(f ---> 0) (at (0))"
+ shows "(f \<longlongrightarrow> 0) (at (0))"
proof -
interpret f: bounded_linear f by fact
- have "(f ---> f 0) (at 0)"
+ have "(f \<longlongrightarrow> 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\<in>s"
- have "(dist a ---> dist a x) (at x within s)"
+ have "(dist a \<longlongrightarrow> 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 \<in> s \<and> y \<in> t}"
{
fix x l
- assume as: "\<forall>n. x n \<in> ?S" "(x ---> l) sequentially"
+ assume as: "\<forall>n. x n \<in> ?S" "(x \<longlongrightarrow> l) sequentially"
from as(1) obtain f where f: "\<forall>n. x n = fst (f n) + snd (f n)" "\<forall>n. fst (f n) \<in> s" "\<forall>n. snd (f n) \<in> t"
using choice[of "\<lambda>n y. x n = (fst y) + (snd y) \<and> fst y \<in> s \<and> snd y \<in> t"] by auto
- obtain l' r where "l'\<in>s" and r: "subseq r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially"
+ obtain l' r where "l'\<in>s" and r: "subseq r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially"
using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
- have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially"
+ have "((\<lambda>n. snd (f (r n))) \<longlongrightarrow> 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 \<Rightarrow> 'b::euclidean_space"
- assumes "(f ---> l) net"
+ assumes "(f \<longlongrightarrow> l) net"
and "\<not> (trivial_limit net)"
and "eventually (\<lambda>x. f(x)\<bullet>i \<le> b) net"
shows "l\<bullet>i \<le> b"
@@ -6914,7 +6914,7 @@
lemma Lim_component_ge:
fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
- assumes "(f ---> l) net"
+ assumes "(f \<longlongrightarrow> l) net"
and "\<not> (trivial_limit net)"
and "eventually (\<lambda>x. b \<le> (f x)\<bullet>i) net"
shows "b \<le> l\<bullet>i"
@@ -6922,7 +6922,7 @@
lemma Lim_component_eq:
fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
- assumes net: "(f ---> l) net" "\<not> trivial_limit net"
+ assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net"
and ev:"eventually (\<lambda>x. f(x)\<bullet>i = b) net"
shows "l\<bullet>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 \<union> t)) \<longleftrightarrow>
- (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
+ "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow>
+ (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
unfolding tendsto_def
by (auto simp add: eventually_within_Un)
lemma Lim_topological:
- "(f ---> l) net \<longleftrightarrow>
+ "(f \<longlongrightarrow> l) net \<longleftrightarrow>
trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
unfolding tendsto_def trivial_limit_eq by auto
@@ -7266,7 +7266,7 @@
}
moreover
{
- assume "\<not> (f ---> x) sequentially"
+ assume "\<not> (f \<longlongrightarrow> x) sequentially"
{
fix e :: real
assume "e > 0"
@@ -7281,9 +7281,9 @@
by (auto intro!: that le_less_trans [OF _ N])
then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
}
- then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
+ then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially"
unfolding lim_sequentially by(auto simp add: dist_norm)
- then have "(f ---> x) sequentially"
+ then have "(f \<longlongrightarrow> x) sequentially"
unfolding f_def
using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
@@ -7815,11 +7815,11 @@
then have "f \<circ> x = g"
unfolding fun_eq_iff
by auto
- then obtain l where "l\<in>s" and l:"(x ---> l) sequentially"
+ then obtain l where "l\<in>s" and l:"(x \<longlongrightarrow> l) sequentially"
using cs[unfolded complete_def, THEN spec[where x="x"]]
using cauchy_isometric[OF \<open>0 < e\<close> s f normf] and cfg and x(1)
by auto
- then have "\<exists>l\<in>f ` s. (g ---> l) sequentially"
+ then have "\<exists>l\<in>f ` s. (g \<longlongrightarrow> l) sequentially"
using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
unfolding \<open>f \<circ> x = g\<close>
by auto
@@ -8186,7 +8186,7 @@
}
then have "Cauchy z"
unfolding cauchy_def by auto
- then obtain x where "x\<in>s" and x:"(z ---> x) sequentially"
+ then obtain x where "x\<in>s" and x:"(z \<longlongrightarrow> x) sequentially"
using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
def e \<equiv> "dist (f x) x"
--- 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: "\<forall>\<^sub>F n in F. (f n ---> g n) (at x within S)"
- assumes g: "(g ---> l) F"
+ assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
+ assumes g: "(g \<longlongrightarrow> l) F"
assumes uc: "uniform_limit S f h F"
assumes "\<not>trivial_limit F"
- shows "(h ---> l) (at x within S)"
+ shows "(h \<longlongrightarrow> l) (at x within S)"
proof (rule tendstoI)
fix e :: real
def e' \<equiv> "e/3"
@@ -101,7 +101,7 @@
tendsto_uniform_limitI:
assumes "uniform_limit S f l F"
assumes "x \<in> S"
- shows "((\<lambda>y. f y x) ---> l x) F"
+ shows "((\<lambda>y. f y x) \<longlongrightarrow> 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 \<in> A"
- then have "\<forall>\<^sub>F n in F. (f n ---> f n x) (at x within A)" "((\<lambda>n. f n x) ---> l x) F"
+ then have "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> f n x) (at x within A)" "((\<lambda>n. f n x) \<longlongrightarrow> 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 \<longlongrightarrow> l x) (at x within A)"
by (rule swap_uniform_limit) fact+
qed
--- 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 \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
+ "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) \<longlongrightarrow> 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 \<Longrightarrow> ((\<lambda>x. sqrt (f x)) ---> sqrt x) F"
+ "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) \<longlongrightarrow> sqrt x) F"
unfolding sqrt_def by (rule tendsto_real_root)
lemma continuous_real_sqrt[continuous_intros]:
--- 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 \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
and f :: "'a \<Rightarrow> 'b" and M
assumes "f \<in> borel_measurable M" "\<And>t. s t \<in> borel_measurable M" "integrable M w"
- assumes lim: "AE x in M. ((\<lambda>i. s i x) ---> f x) at_top"
+ assumes lim: "AE x in M. ((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
assumes bound: "\<forall>\<^sub>F i in at_top. AE x in M. norm (s i x) \<le> w x"
begin
-lemma integral_dominated_convergence_at_top: "((\<lambda>t. integral\<^sup>L M (s t)) ---> integral\<^sup>L M f) at_top"
+lemma integral_dominated_convergence_at_top: "((\<lambda>t. integral\<^sup>L M (s t)) \<longlongrightarrow> integral\<^sup>L M f) at_top"
proof (rule tendsto_at_topI_sequentially)
fix X :: "nat \<Rightarrow> 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. (\<lambda>n. s (X (n + N)) x) \<longlonglongrightarrow> f x"
using lim
proof eventually_elim
- fix x assume "((\<lambda>i. s i x) ---> f x) at_top"
+ fix x assume "((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
then show "(\<lambda>n. s (X (n + N)) x) \<longlonglongrightarrow> f x"
by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
qed
@@ -1560,7 +1560,7 @@
show "AE x in M. (\<lambda>i. s (N + real i) x) \<longlonglongrightarrow> f x"
using lim
proof eventually_elim
- fix x assume "((\<lambda>i. s i x) ---> f x) at_top"
+ fix x assume "((\<lambda>i. s i x) \<longlongrightarrow> f x) at_top"
then show "(\<lambda>n. s (N + n) x) \<longlonglongrightarrow> 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 \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
- shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
+ shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) \<longlongrightarrow> \<integral> x. f x \<partial>M) at_top"
proof (rule tendsto_at_topI_sequentially)
fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) \<longlonglongrightarrow> integral\<^sup>L M f"
@@ -2486,7 +2486,7 @@
assumes nonneg: "AE x in M. 0 \<le> f x"
assumes borel: "f \<in> borel_measurable borel"
assumes int: "\<And>y. integrable M (\<lambda>x. f x * indicator {.. y} x)"
- assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> x) at_top"
+ assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) \<longlongrightarrow> 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"
--- 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 "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) --->
+ have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) \<longlongrightarrow>
(1 - (\<Sum>n\<le>k. 0 / (fact n))) * fact k) at_top"
by (intro tendsto_intros tendsto_power_div_exp_0) simp
then show "?X \<longlonglongrightarrow> real_of_nat (fact k)"
@@ -865,20 +865,20 @@
proof (intro nn_integral_cong ereal_right_mult_cong)
fix s :: real show "?pI (\<lambda>x. ?ff x s) = ereal (1 / (2 * (1 + s\<^sup>2)))"
proof (subst nn_integral_FTC_atLeast)
- have "((\<lambda>a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) ---> (- (0 / (2 + 2 * s\<^sup>2)))) at_top"
+ have "((\<lambda>a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) \<longlongrightarrow> (- (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 "((\<lambda>a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) ---> 0) at_top"
+ then show "((\<lambda>a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) \<longlongrightarrow> 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 "((\<lambda>a. arctan a / 2) ---> (pi / 2) / 2 ) at_top"
+ show "((\<lambda>a. arctan a / 2) \<longlongrightarrow> (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 "\<dots> = ereal (0 - (- exp (- 0\<^sup>2) / 2))"
proof (rule nn_integral_FTC_atLeast)
- have "((\<lambda>x::real. - exp (- x\<^sup>2) / 2) ---> - 0 / 2) at_top"
+ have "((\<lambda>x::real. - exp (- x\<^sup>2) / 2) \<longlongrightarrow> - 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 "((\<lambda>a::real. - exp (- a\<^sup>2) / 2) ---> 0) at_top"
+ then show "((\<lambda>a::real. - exp (- a\<^sup>2) / 2) \<longlongrightarrow> 0) at_top"
by simp
qed (auto intro!: derivative_eq_intros)
also have "\<dots> = ereal (1 / 2)"
@@ -934,13 +934,13 @@
have "2 \<noteq> (0::real)"
by linarith
let ?f = "\<lambda>b. \<integral>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \<partial>lborel"
- have "((\<lambda>b. (k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \<partial>lborel) - ?M (k + 1) b / 2) --->
+ have "((\<lambda>b. (k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \<partial>lborel) - ?M (k + 1) b / 2) \<longlongrightarrow>
(k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top" (is ?tendsto)
proof (intro tendsto_intros \<open>2 \<noteq> 0\<close> tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros])
- show "(?M (k + 1) ---> 0) at_top"
+ show "(?M (k + 1) \<longlongrightarrow> 0) at_top"
proof cases
assume "even k"
- have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top"
+ have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) \<longlongrightarrow> 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 "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top"
+ have "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) \<longlongrightarrow> 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 \<longleftrightarrow> ((?f ---> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top)"
+ also have "?tendsto \<longleftrightarrow> ((?f \<longlongrightarrow> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>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 \<le> b"
have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)"
@@ -977,7 +977,7 @@
then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>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 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel)) at_top)"
+ finally have int_M_at_top: "((?f \<longlongrightarrow> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel)) at_top)"
by simp
have "has_bochner_integral lborel (\<lambda>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 (\<lambda>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 \<longlongrightarrow> (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
--- 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 "\<lambda>x. \<not> P x"]
unfolding closed_def by (rule back_subst) auto
-lemma tendsto_proj: "((\<lambda>x. x) ---> a) F \<Longrightarrow> ((\<lambda>x. (x)\<^sub>F i) ---> (a)\<^sub>F i) F"
+lemma tendsto_proj: "((\<lambda>x. x) \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. (x)\<^sub>F i) \<longlongrightarrow> (a)\<^sub>F i) F"
unfolding tendsto_def
proof safe
fix S::"'b set"
--- 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: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
- assumes A: "((F \<circ> real_of_ereal) ---> A) (at_right a)"
- assumes B: "((F \<circ> real_of_ereal) ---> B) (at_left b)"
+ assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
+ assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> 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: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
assumes f_integrable: "set_integrable lborel (einterval a b) f"
- assumes A: "((F \<circ> real_of_ereal) ---> A) (at_right a)"
- assumes B: "((F \<circ> real_of_ereal) ---> B) (at_left b)"
+ assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
+ assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
shows "(LBINT x=a..b. f x) = B - A"
proof -
from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
@@ -834,8 +834,8 @@
and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
- and A: "((ereal \<circ> g \<circ> real_of_ereal) ---> A) (at_right a)"
- and B: "((ereal \<circ> g \<circ> real_of_ereal) ---> B) (at_left b)"
+ and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
+ and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
and integrable2: "set_integrable lborel (einterval A B) (\<lambda>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': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
and f_nonneg: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> 0 \<le> f (g x)" (* TODO: make this AE? *)
and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
- and A: "((ereal \<circ> g \<circ> real_of_ereal) ---> A) (at_right a)"
- and B: "((ereal \<circ> g \<circ> real_of_ereal) ---> B) (at_left b)"
+ and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
+ and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)"
shows
"set_integrable lborel (einterval A B) f"
--- 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 \<ge> 0"
proof (rule tendsto_le_const)
let ?A' = "(\<lambda>y. y - x) ` interior A"
- from deriv show "((\<lambda>h. (f (x + h) - f x) / h) ---> D) (at 0)"
+ from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> 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)
--- 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 "((\<lambda>a. F b - F a) ---> emeasure ?F {a..b}) (at_left a)"
+ show "((\<lambda>a. F b - F a) \<longlongrightarrow> emeasure ?F {a..b}) (at_left a)"
proof (rule tendsto_at_left_sequentially)
show "a - 1 < a" by simp
fix X assume "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a"
@@ -344,7 +344,7 @@
using \<open>\<And>n. X n < a\<close> \<open>a \<le> b\<close> by (subst *) (auto intro: less_imp_le less_le_trans)
finally show "(\<lambda>n. F b - F (X n)) \<longlonglongrightarrow> emeasure ?F {a..b}" .
qed
- show "((\<lambda>a. ereal (F b - F a)) ---> F b - F a) (at_left a)"
+ show "((\<lambda>a. ereal (F b - F a)) \<longlongrightarrow> 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 \<in> borel_measurable borel"
assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
- assumes lim: "(F ---> T) at_top"
+ assumes lim: "(F \<longlongrightarrow> T) at_top"
shows "(\<integral>\<^sup>+x. ereal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
proof -
let ?f = "\<lambda>(i::nat) (x::real). ereal (f x) * indicator {a..a + real i} x"
--- 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" "\<forall>n\<ge>m. f n \<in> S"
- obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
+ obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
proof atomize_elim
have "subseq (op + m)" by (simp add: subseq_def)
have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
--- 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 \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
+ "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
unfolding nhds_metric filterlim_INF filterlim_principal by auto
-lemma (in metric_space) tendstoI: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f ---> l) F"
+lemma (in metric_space) tendstoI: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
by (auto simp: tendsto_iff)
-lemma (in metric_space) tendstoD: "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
+lemma (in metric_space) tendstoD: "(f \<longlongrightarrow> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>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 \<longlongrightarrow> a) F"
assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"
- shows "(g ---> b) F"
+ shows "(g \<longlongrightarrow> b) F"
proof (rule tendstoI)
fix e :: real assume "0 < e"
with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD)
@@ -1977,7 +1977,7 @@
lemma tendsto_at_topI_sequentially:
fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) \<longlonglongrightarrow> y"
- shows "(f ---> y) at_top"
+ shows "(f \<longlongrightarrow> y) at_top"
proof -
from nhds_countable[of y] guess A . note A = this
@@ -2009,7 +2009,7 @@
fixes f :: "real \<Rightarrow> real"
assumes mono: "mono f"
assumes limseq: "(\<lambda>n. f (real n)) \<longlonglongrightarrow> y"
- shows "(f ---> y) at_top"
+ shows "(f \<longlongrightarrow> y) at_top"
proof (rule tendstoI)
fix e :: real assume "0 < e"
with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
--- 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 \<open>Tendsto\<close>
abbreviation (in topological_space)
- tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
- "(f ---> l) F \<equiv> filterlim f (nhds l) F"
+ tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "\<longlongrightarrow>" 55) where
+ "(f \<longlongrightarrow> l) F \<equiv> filterlim f (nhds l) F"
definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "Lim A f = (THE l. (f ---> l) A)"
+ "Lim A f = (THE l. (f \<longlongrightarrow> l) A)"
-lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
+lemma tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
by simp
named_theorems tendsto_intros "introduction rules for tendsto"
@@ -498,55 +498,55 @@
\<close>
lemma (in topological_space) tendsto_def:
- "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
+ "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
unfolding nhds_def filterlim_INF filterlim_principal by auto
lemma tendsto_cong:
assumes "eventually (\<lambda>x. f x = g x) F"
- shows "(f ---> c) F \<longleftrightarrow> (g ---> c) F"
+ shows "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
by (rule filterlim_cong[OF refl refl assms])
-lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
+lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f \<longlongrightarrow> l) F' \<Longrightarrow> (f \<longlongrightarrow> l) F"
unfolding tendsto_def le_filter_def by fast
-lemma tendsto_within_subset: "(f ---> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at x within T)"
+lemma tendsto_within_subset: "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
by (blast intro: tendsto_mono at_le)
lemma filterlim_at:
- "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f ---> b) F)"
+ "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f \<longlongrightarrow> b) F)"
by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
lemma (in topological_space) topological_tendstoI:
- "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f ---> l) F"
+ "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
unfolding tendsto_def by auto
lemma (in topological_space) topological_tendstoD:
- "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
+ "(f \<longlongrightarrow> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
unfolding tendsto_def by auto
lemma (in order_topology) order_tendsto_iff:
- "(f ---> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
+ "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
unfolding nhds_order filterlim_inf filterlim_INF filterlim_principal by auto
lemma (in order_topology) order_tendstoI:
"(\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F) \<Longrightarrow> (\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F) \<Longrightarrow>
- (f ---> y) F"
+ (f \<longlongrightarrow> y) F"
unfolding order_tendsto_iff by auto
lemma (in order_topology) order_tendstoD:
- assumes "(f ---> y) F"
+ assumes "(f \<longlongrightarrow> y) F"
shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
and "y < a \<Longrightarrow> eventually (\<lambda>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 \<longlongrightarrow> a) bot"
unfolding tendsto_def by simp
lemma (in linorder_topology) tendsto_max:
- assumes X: "(X ---> x) net"
- assumes Y: "(Y ---> y) net"
- shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
+ assumes X: "(X \<longlongrightarrow> x) net"
+ assumes Y: "(Y \<longlongrightarrow> y) net"
+ shows "((\<lambda>x. max (X x) (Y x)) \<longlongrightarrow> max x y) net"
proof (rule order_tendstoI)
fix a assume "a < max x y"
then show "eventually (\<lambda>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 "((\<lambda>x. min (X x) (Y x)) ---> min x y) net"
+ assumes X: "(X \<longlongrightarrow> x) net"
+ assumes Y: "(Y \<longlongrightarrow> y) net"
+ shows "((\<lambda>x. min (X x) (Y x)) \<longlongrightarrow> min x y) net"
proof (rule order_tendstoI)
fix a assume "a < min x y"
then show "eventually (\<lambda>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]: "((\<lambda>x. x) ---> a) (at a within s)"
+lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
unfolding tendsto_def eventually_at_topological by auto
-lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) ---> k) F"
+lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
by (simp add: tendsto_def)
lemma (in t2_space) tendsto_unique:
- assumes "F \<noteq> bot" and "(f ---> a) F" and "(f ---> b) F"
+ assumes "F \<noteq> bot" and "(f \<longlongrightarrow> a) F" and "(f \<longlongrightarrow> b) F"
shows "a = b"
proof (rule ccontr)
assume "a \<noteq> b"
obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
using hausdorff [OF \<open>a \<noteq> b\<close>] by fast
have "eventually (\<lambda>x. f x \<in> U) F"
- using \<open>(f ---> a) F\<close> \<open>open U\<close> \<open>a \<in> U\<close> by (rule topological_tendstoD)
+ using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open U\<close> \<open>a \<in> U\<close> by (rule topological_tendstoD)
moreover
have "eventually (\<lambda>x. f x \<in> V) F"
- using \<open>(f ---> b) F\<close> \<open>open V\<close> \<open>b \<in> V\<close> by (rule topological_tendstoD)
+ using \<open>(f \<longlongrightarrow> b) F\<close> \<open>open V\<close> \<open>b \<in> V\<close> by (rule topological_tendstoD)
ultimately
have "eventually (\<lambda>x. False) F"
proof eventually_elim
@@ -605,28 +605,28 @@
qed
lemma (in t2_space) tendsto_const_iff:
- assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
+ assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
by (auto intro!: tendsto_unique [OF assms tendsto_const])
lemma increasing_tendsto:
fixes f :: "_ \<Rightarrow> 'a::order_topology"
assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
- shows "(f ---> l) F"
+ shows "(f \<longlongrightarrow> l) F"
using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
lemma decreasing_tendsto:
fixes f :: "_ \<Rightarrow> 'a::order_topology"
assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
- shows "(f ---> l) F"
+ shows "(f \<longlongrightarrow> l) F"
using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
lemma tendsto_sandwich:
fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
- assumes lim: "(f ---> c) net" "(h ---> c) net"
- shows "(g ---> c) net"
+ assumes lim: "(f \<longlongrightarrow> c) net" "(h \<longlongrightarrow> c) net"
+ shows "(g \<longlongrightarrow> c) net"
proof (rule order_tendstoI)
fix a show "a < c \<Longrightarrow> eventually (\<lambda>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 \<noteq> bot"
assumes "frequently (\<lambda>x. f x = c) F"
- assumes "(f ---> d) F"
+ assumes "(f \<longlongrightarrow> d) F"
shows "d = (c :: 'a :: t1_space)"
proof (rule ccontr)
assume "d \<noteq> c"
@@ -649,7 +649,7 @@
qed
lemma tendsto_imp_eventually_ne:
- assumes "F \<noteq> bot" "(f ---> c) F" "c \<noteq> (c' :: 'a :: t1_space)"
+ assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> (c' :: 'a :: t1_space)"
shows "eventually (\<lambda>z. f z \<noteq> c') F"
proof (rule ccontr)
assume "\<not>eventually (\<lambda>z. f z \<noteq> c') F"
@@ -660,7 +660,7 @@
lemma tendsto_le:
fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
- assumes x: "(f ---> x) F" and y: "(g ---> y) F"
+ assumes x: "(f \<longlongrightarrow> x) F" and y: "(g \<longlongrightarrow> y) F"
assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
shows "y \<le> x"
proof (rule ccontr)
@@ -678,14 +678,14 @@
lemma tendsto_le_const:
fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
- assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<le> f i) F"
+ assumes x: "(f \<longlongrightarrow> x) F" and a: "eventually (\<lambda>i. a \<le> f i) F"
shows "a \<le> x"
using F x tendsto_const a by (rule tendsto_le)
lemma tendsto_ge_const:
fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
- assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F"
+ assumes x: "(f \<longlongrightarrow> x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F"
shows "a \<ge> x"
by (rule tendsto_le [OF F tendsto_const x a])
@@ -695,7 +695,7 @@
subsubsection \<open>Rules about @{const Lim}\<close>
lemma tendsto_Lim:
- "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
+ "\<not>(trivial_limit net) \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> Lim net f = l"
unfolding Lim_def using tendsto_unique[of net f] by auto
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
@@ -771,7 +771,7 @@
qed
lemma tendsto_at_within_iff_tendsto_nhds:
- "(g ---> g l) (at l within S) \<longleftrightarrow> (g ---> g l) (inf (nhds l) (principal S))"
+ "(g \<longlongrightarrow> g l) (at l within S) \<longleftrightarrow> (g \<longlongrightarrow> 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 \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
("((_)/ \<longlonglongrightarrow> (_))" [60, 60] 60) where
- "X \<longlonglongrightarrow> L \<equiv> (X ---> L) sequentially"
+ "X \<longlonglongrightarrow> L \<equiv> (X \<longlongrightarrow> L) sequentially"
abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
"lim X \<equiv> Lim sequentially X"
@@ -1196,7 +1196,7 @@
lemma tendsto_at_iff_sequentially:
fixes f :: "'a :: first_countable_topology \<Rightarrow> _"
- shows "(f ---> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X \<longlonglongrightarrow> x \<longrightarrow> ((f \<circ> X) \<longlonglongrightarrow> a))"
+ shows "(f \<longlongrightarrow> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X \<longlonglongrightarrow> x \<longrightarrow> ((f \<circ> X) \<longlonglongrightarrow> 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 \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
- "f -- a --> L \<equiv> (f ---> L) (at a)"
+ "f -- a --> L \<equiv> (f \<longlongrightarrow> L) (at a)"
-lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
+lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (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 \<longleftrightarrow> (g ---> g l) (nhds l)"
+ "g -- l --> g l \<longleftrightarrow> (g \<longlongrightarrow> 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 \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
+ "g -- l --> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
unfolding o_def by (rule tendsto_compose)
lemma tendsto_compose_eventually:
- "g -- l --> m \<Longrightarrow> (f ---> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> m) F"
+ "g -- l --> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
lemma LIM_compose_eventually:
@@ -1263,7 +1263,7 @@
shows "(\<lambda>x. g (f x)) -- a --> c"
using g f inj by (rule tendsto_compose_eventually)
-lemma tendsto_compose_filtermap: "((g \<circ> f) ---> T) F \<longleftrightarrow> (g ---> T) (filtermap f F)"
+lemma tendsto_compose_filtermap: "((g \<circ> f) \<longlongrightarrow> T) F \<longleftrightarrow> (g \<longlongrightarrow> T) (filtermap f F)"
by (simp add: filterlim_def filtermap_filtermap comp_def)
subsubsection \<open>Relation of LIM and LIMSEQ\<close>
@@ -1329,7 +1329,7 @@
fixes a :: "_ :: {linorder_topology, first_countable_topology}"
assumes "b < a"
assumes *: "\<And>S. (\<And>n. S n < a) \<Longrightarrow> (\<And>n. b < S n) \<Longrightarrow> incseq S \<Longrightarrow> S \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L"
- shows "(X ---> L) (at_left a)"
+ shows "(X \<longlongrightarrow> 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 *: "\<And>S. (\<And>n. a < S n) \<Longrightarrow> (\<And>n. S n < b) \<Longrightarrow> decseq S \<Longrightarrow> S \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L"
- shows "(X ---> L) (at_right a)"
+ shows "(X \<longlongrightarrow> 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 \<open>Continuity on a set\<close>
definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
- "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
+ "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f \<longlongrightarrow> f x) (at x within s))"
lemma continuous_on_cong [cong]:
"s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
@@ -1559,7 +1559,7 @@
subsubsection \<open>Continuity at a point\<close>
definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
- "continuous F f \<longleftrightarrow> (f ---> f (Lim F (\<lambda>x. x))) F"
+ "continuous F f \<longleftrightarrow> (f \<longlongrightarrow> f (Lim F (\<lambda>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 \<Longrightarrow> continuous net f"
by simp
-lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f x) (at x within s)"
+lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f \<longlongrightarrow> 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 \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a"
unfolding o_def by (rule isCont_o2)
-lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
+lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
unfolding isCont_def by (rule tendsto_compose)
lemma continuous_within_compose3:
@@ -2271,7 +2271,7 @@
assumes S: "S \<noteq> {}" "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 \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
using cont unfolding continuous_within .
show "f (Sup S) \<le> (SUP s:S. f s)"
@@ -2308,7 +2308,7 @@
assumes S: "S \<noteq> {}" "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 \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
using cont unfolding continuous_within .
show "(INF s:S. f s) \<le> f (Sup S)"
@@ -2345,7 +2345,7 @@
assumes S: "S \<noteq> {}" "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 \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
using cont unfolding continuous_within .
show "(INF s:S. f s) \<le> f (Inf S)"
@@ -2382,7 +2382,7 @@
assumes S: "S \<noteq> {}" "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 \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
using cont unfolding continuous_within .
show "f (Inf S) \<le> (SUP s:S. f s)"
--- 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 \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) ---> 0) sequentially"
+ shows "1 < norm x \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) \<longlongrightarrow> 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 \<Rightarrow> 'a::{real_normed_field,banach}"
assumes s: "0 < s"
and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
- shows "(f ---> a 0) (at 0)"
+ shows "(f \<longlongrightarrow> a 0) (at 0)"
proof -
have "summable (\<lambda>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 (\<lambda>x. \<Sum>n. a n * x ^ n) 0"
by (blast intro: DERIV_continuous)
- then have "((\<lambda>x. \<Sum>n. a n * x ^ n) ---> a 0) (at 0)"
+ then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> 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 \<Rightarrow> 'a::{real_normed_field,banach}"
assumes s: "0 < s"
and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
- shows "(f ---> a 0) (at 0)"
+ shows "(f \<longlongrightarrow> a 0) (at 0)"
proof -
- have *: "((\<lambda>x. if x = 0 then a 0 else f x) ---> a 0) (at 0)"
+ have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> 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:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
- shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
+ shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) \<longlongrightarrow> 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 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
+ "(f \<longlongrightarrow> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) \<longlongrightarrow> 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 \<longlongrightarrow> (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 "((\<lambda>z::'a. (exp(z) - 1) / z) ---> 1) (at 0)"
+ shows "((\<lambda>z::'a. (exp(z) - 1) / z) \<longlongrightarrow> 1) (at 0)"
proof -
have "((\<lambda>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: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
+lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) \<longlongrightarrow> (0::real)) at_top"
proof (induct k)
case 0
- show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
+ show "((\<lambda>x. x ^ 0 / exp x) \<longlongrightarrow> (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 (\<lambda>x. exp x \<noteq> 0) at_top"
by auto
from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
- show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
+ show "((\<lambda>x. real (Suc k) * x ^ k / exp x) \<longlongrightarrow> 0) at_top"
by simp
qed (rule exp_at_top)
qed
@@ -2089,7 +2089,7 @@
lemma tendsto_log [tendsto_intros]:
- "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>x. log (f x) (g x)) ---> log a b) F"
+ "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>x. log (f x) (g x)) \<longlongrightarrow> 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 \<noteq> 0"
- shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
+ assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F" and a: "a \<noteq> 0"
+ shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
unfolding powr_def
proof (rule filterlim_If)
- from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
+ from f show "((\<lambda>x. 0) \<longlongrightarrow> (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: "\<forall>\<^sub>F x in F. 0 \<le> f x" and b: "0 < b"
- shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
+ assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F" and f_nonneg: "\<forall>\<^sub>F x in F. 0 \<le> f x" and b: "0 < b"
+ shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
unfolding powr_def
proof (rule filterlim_If)
- from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
+ from f show "((\<lambda>x. 0) \<longlongrightarrow> (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 \<noteq> 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 "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))"
+ then have "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> 0) (inf F (principal {x. f x \<noteq> 0}))"
by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
filterlim_tendsto_pos_mult_at_bot[OF _ \<open>0 < b\<close>]
intro: tendsto_mono inf_le1 g) }
- then show "((\<lambda>x. exp (g x * ln (f x))) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \<noteq> 0}))"
+ then show "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \<noteq> 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" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
- shows "((\<lambda>x. f x powr g x) ---> 0) F"
+ assumes "(f \<longlongrightarrow> (0::real)) F" "(g \<longlongrightarrow> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
+ shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> 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 "((\<lambda>x. f x powr s) ---> (0::real)) F"
+ shows "((\<lambda>x. f x powr s) \<longlongrightarrow> (0::real)) F"
proof -
- have "((\<lambda>x. exp (s * ln (f x))) ---> (0::real)) F" (is "?X")
+ have "((\<lambda>x. exp (s * ln (f x))) \<longlongrightarrow> (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 \<longleftrightarrow> ((\<lambda>x. f x powr s) ---> (0::real)) F"
+ also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) \<longlongrightarrow> (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 "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
+ shows "((\<lambda>y. (1 + x * y) powr (1 / y)) \<longlongrightarrow> exp x) (at_right 0)"
proof cases
assume "x \<noteq> 0"
have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
by (auto intro!: derivative_eq_intros)
- then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
+ then have "((\<lambda>y. ln (1 + x * y) / y) \<longlongrightarrow> x) (at 0)"
by (auto simp add: has_field_derivative_def field_has_derivative_at)
- then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
+ then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) \<longlongrightarrow> 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 "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
+ shows "((\<lambda>y. (1 + x / y) powr y) \<longlongrightarrow> 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:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
- shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
+ shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) \<longlongrightarrow> sin a) F"
by (rule isCont_tendsto_compose [OF isCont_sin])
lemma tendsto_cos [tendsto_intros]:
fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
- shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
+ shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) \<longlongrightarrow> 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 \<Rightarrow> 'a::{real_normed_field,banach}"
- shows "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) \<longlongrightarrow> 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 \<Rightarrow> 'a::{real_normed_field,banach}"
- shows "\<lbrakk>(f ---> a) F; sin a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. cot (f x)) ---> cot a) F"
+ shows "\<lbrakk>(f \<longlongrightarrow> a) F; sin a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. cot (f x)) \<longlongrightarrow> 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 \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
+lemma tendsto_arctan [tendsto_intros]: "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) \<longlongrightarrow> arctan x) F"
by (rule isCont_tendsto_compose [OF isCont_arctan])
lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
@@ -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 \<longlongrightarrow> (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 \<longlongrightarrow> - (pi/2)) at_bot"
unfolding filterlim_at_bot_mirror arctan_minus
by (intro tendsto_minus tendsto_arctan_at_top)