--- a/NEWS Tue Dec 29 22:41:22 2015 +0100
+++ b/NEWS Tue Dec 29 23:04:53 2015 +0100
@@ -502,6 +502,8 @@
notation Preorder.equiv ("op ~~")
and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)
+ notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
+
* The alternative notation "\<Colon>" for type and sort constraints has been
removed: in LaTeX document output it looks the same as "::".
INCOMPATIBILITY, use plain "::" instead.
--- a/src/HOL/Complex.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Complex.thy Tue Dec 29 23:04:53 2015 +0100
@@ -415,7 +415,7 @@
proof
fix X :: "nat \<Rightarrow> complex"
assume X: "Cauchy X"
- then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
+ then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) \<longlonglongrightarrow> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)
then show "convergent X"
unfolding complex.collapse by (rule convergentI)
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Dec 29 23:04:53 2015 +0100
@@ -2103,7 +2103,7 @@
using ln_series[of "x + 1"] \<open>0 \<le> x\<close> \<open>x < 1\<close> by auto
have "norm x < 1" using assms by auto
- have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
+ have "?a \<longlonglongrightarrow> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF \<open>norm x < 1\<close>]]] by auto
have "0 \<le> ?a n" for n
by (rule mult_nonneg_nonneg) (auto simp: \<open>0 \<le> x\<close>)
@@ -2117,7 +2117,7 @@
by (rule mult_left_mono, fact less_imp_le[OF \<open>x < 1\<close>]) (auto simp: \<open>0 \<le> x\<close>)
thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
qed auto
- from summable_Leibniz'(2,4)[OF \<open>?a ----> 0\<close> \<open>\<And>n. 0 \<le> ?a n\<close>, OF \<open>\<And>n. ?a (Suc n) \<le> ?a n\<close>, unfolded ln_eq]
+ from summable_Leibniz'(2,4)[OF \<open>?a \<longlonglongrightarrow> 0\<close> \<open>\<And>n. 0 \<le> ?a n\<close>, OF \<open>\<And>n. ?a (Suc n) \<le> ?a n\<close>, unfolded ln_eq]
show ?lb and ?ub
unfolding atLeast0LessThan by auto
qed
--- a/src/HOL/Library/BigO.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/BigO.thy Tue Dec 29 23:04:53 2015 +0100
@@ -840,7 +840,7 @@
apply (auto split: split_max simp add: func_plus)
done
-lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)"
+lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g \<longlonglongrightarrow> 0 \<Longrightarrow> f \<longlonglongrightarrow> (0::real)"
apply (simp add: LIMSEQ_iff bigo_alt_def)
apply clarify
apply (drule_tac x = "r / c" in spec)
@@ -863,7 +863,7 @@
apply simp
done
-lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)"
+lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h \<longlonglongrightarrow> 0 \<Longrightarrow> f \<longlonglongrightarrow> a \<Longrightarrow> g \<longlonglongrightarrow> (a::real)"
apply (drule set_plus_imp_minus)
apply (drule bigo_LIMSEQ1)
apply assumption
--- a/src/HOL/Library/Extended_Real.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Dec 29 23:04:53 2015 +0100
@@ -40,10 +40,10 @@
show ?thesis
unfolding continuous_within
proof (intro tendsto_at_left_sequentially[of bot])
- fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S ----> x"
+ fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S \<longlonglongrightarrow> x"
from S_x have x_eq: "x = (SUP i. S i)"
by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S)
- show "(\<lambda>n. f (S n)) ----> f x"
+ show "(\<lambda>n. f (S n)) \<longlonglongrightarrow> f x"
unfolding x_eq sup_continuousD[OF f S]
using S sup_continuous_mono[OF f] by (intro LIMSEQ_SUP) (auto simp: mono_def)
qed (insert x, auto simp: bot_less)
@@ -77,10 +77,10 @@
show ?thesis
unfolding continuous_within
proof (intro tendsto_at_right_sequentially[of _ top])
- fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S ----> x"
+ fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S \<longlonglongrightarrow> x"
from S_x have x_eq: "x = (INF i. S i)"
by (rule LIMSEQ_unique) (intro LIMSEQ_INF S)
- show "(\<lambda>n. f (S n)) ----> f x"
+ show "(\<lambda>n. f (S n)) \<longlonglongrightarrow> f x"
unfolding x_eq inf_continuousD[OF f S]
using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def)
qed (insert x, auto simp: less_top)
@@ -2118,10 +2118,10 @@
lemma countable_approach:
fixes x :: ereal
assumes "x \<noteq> -\<infinity>"
- shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)"
+ shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f \<longlonglongrightarrow> x)"
proof (cases x)
case (real r)
- moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0"
+ moreover have "(\<lambda>n. r - inverse (real (Suc n))) \<longlonglongrightarrow> r - 0"
by (intro tendsto_intros LIMSEQ_inverse_real_of_nat)
ultimately show ?thesis
by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def)
@@ -2141,7 +2141,7 @@
by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
next
assume "Sup A \<noteq> -\<infinity>"
- then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l ----> Sup A"
+ then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A"
by (auto dest: countable_approach)
have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
@@ -2161,9 +2161,9 @@
moreover
have "(SUP i. f i) = Sup A"
proof (rule tendsto_unique)
- show "f ----> (SUP i. f i)"
+ show "f \<longlonglongrightarrow> (SUP i. f i)"
by (rule LIMSEQ_SUP \<open>incseq f\<close>)+
- show "f ----> Sup A"
+ show "f \<longlonglongrightarrow> Sup A"
using l f
by (intro tendsto_sandwich[OF _ _ l_Sup tendsto_const])
(auto simp: Sup_upper)
@@ -2454,8 +2454,8 @@
assumes "convergent a"
shows "convergent (\<lambda>n. ereal (a n))" and "lim (\<lambda>n. ereal (a n)) = ereal (lim a)"
proof -
- from assms obtain L where L: "a ----> L" unfolding convergent_def ..
- hence lim: "(\<lambda>n. ereal (a n)) ----> ereal L" using lim_ereal by auto
+ from assms obtain L where L: "a \<longlonglongrightarrow> L" unfolding convergent_def ..
+ hence lim: "(\<lambda>n. ereal (a n)) \<longlonglongrightarrow> ereal L" using lim_ereal by auto
thus "convergent (\<lambda>n. ereal (a n))" unfolding convergent_def ..
thus "lim (\<lambda>n. ereal (a n)) = ereal (lim a)" using lim L limI by metis
qed
@@ -2495,7 +2495,7 @@
by auto
qed
-lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
+lemma Lim_PInfty: "f \<longlonglongrightarrow> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
unfolding tendsto_PInfty eventually_sequentially
proof safe
fix r
@@ -2508,7 +2508,7 @@
by (blast intro: less_le_trans)
qed (blast intro: less_imp_le)
-lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
+lemma Lim_MInfty: "f \<longlonglongrightarrow> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
unfolding tendsto_MInfty eventually_sequentially
proof safe
fix r
@@ -2521,24 +2521,24 @@
by (blast intro: le_less_trans)
qed (blast intro: less_imp_le)
-lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
+lemma Lim_bounded_PInfty: "f \<longlonglongrightarrow> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
using LIMSEQ_le_const2[of f l "ereal B"] by auto
-lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
+lemma Lim_bounded_MInfty: "f \<longlonglongrightarrow> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
using LIMSEQ_le_const[of f l "ereal B"] by auto
lemma tendsto_explicit:
- "f ----> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
+ "f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
unfolding tendsto_def eventually_sequentially by auto
-lemma Lim_bounded_PInfty2: "f ----> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
+lemma Lim_bounded_PInfty2: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
-lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
+lemma Lim_bounded_ereal: "f \<longlonglongrightarrow> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
by (intro LIMSEQ_le_const2) auto
lemma Lim_bounded2_ereal:
- assumes lim:"f ----> (l :: 'a::linorder_topology)"
+ assumes lim:"f \<longlonglongrightarrow> (l :: 'a::linorder_topology)"
and ge: "\<forall>n\<ge>N. f n \<ge> C"
shows "l \<ge> C"
using ge
@@ -2696,7 +2696,7 @@
fixes x :: ereal
assumes "\<bar>x\<bar> \<noteq> \<infinity>"
and "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
- shows "u ----> x"
+ shows "u \<longlonglongrightarrow> x"
proof (rule topological_tendstoI, unfold eventually_sequentially)
obtain rx where rx: "x = ereal rx"
using assms by (cases x) auto
@@ -2732,7 +2732,7 @@
qed
lemma tendsto_obtains_N:
- assumes "f ----> f0"
+ assumes "f \<longlonglongrightarrow> f0"
assumes "open S"
and "f0 \<in> S"
obtains N where "\<forall>n\<ge>N. f n \<in> S"
@@ -2742,10 +2742,10 @@
lemma ereal_LimI_finite_iff:
fixes x :: ereal
assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- shows "u ----> x \<longleftrightarrow> (\<forall>r. 0 < r \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r))"
+ shows "u \<longlonglongrightarrow> x \<longleftrightarrow> (\<forall>r. 0 < r \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume lim: "u ----> x"
+ assume lim: "u \<longlonglongrightarrow> x"
{
fix r :: ereal
assume "r > 0"
@@ -2762,7 +2762,7 @@
by auto
next
assume ?rhs
- then show "u ----> x"
+ then show "u \<longlonglongrightarrow> x"
using ereal_LimI_finite[of x] assms by auto
qed
@@ -2924,7 +2924,7 @@
shows "suminf f \<le> x"
proof (rule Lim_bounded_ereal)
have "summable f" using pos[THEN summable_ereal_pos] .
- then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
+ then show "(\<lambda>N. \<Sum>n<N. f n) \<longlonglongrightarrow> suminf f"
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
using assms by auto
@@ -3195,11 +3195,11 @@
assumes f: "\<And>i. 0 \<le> f i"
shows "(\<Sum>i. f (i + k)) \<le> suminf f"
proof -
- have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
+ have "(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))"
using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
- moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
+ moreover have "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
- then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
+ then have "(\<lambda>n. \<Sum>i<n + k. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
by (rule LIMSEQ_ignore_initial_segment)
ultimately show ?thesis
proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
@@ -3430,7 +3430,7 @@
lemma limsup_le_liminf_real:
fixes X :: "nat \<Rightarrow> real" and L :: real
assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
- shows "X ----> L"
+ shows "X \<longlonglongrightarrow> L"
proof -
from 1 2 have "limsup X \<le> liminf X" by auto
hence 3: "limsup X = liminf X"
@@ -3442,7 +3442,7 @@
by (rule convergent_limsup_cl)
also from 1 2 3 have "limsup X = L" by auto
finally have "lim (\<lambda>n. ereal(X n)) = L" ..
- hence "(\<lambda>n. ereal (X n)) ----> L"
+ hence "(\<lambda>n. ereal (X n)) \<longlonglongrightarrow> L"
apply (elim subst)
by (subst convergent_LIMSEQ_iff [symmetric], rule 4)
thus ?thesis by simp
@@ -3450,33 +3450,33 @@
lemma liminf_PInfty:
fixes X :: "nat \<Rightarrow> ereal"
- shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
+ shows "X \<longlonglongrightarrow> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
by (metis Liminf_PInfty trivial_limit_sequentially)
lemma limsup_MInfty:
fixes X :: "nat \<Rightarrow> ereal"
- shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
+ shows "X \<longlonglongrightarrow> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
by (metis Limsup_MInfty trivial_limit_sequentially)
lemma ereal_lim_mono:
fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
- and "X ----> x"
- and "Y ----> y"
+ and "X \<longlonglongrightarrow> x"
+ and "Y \<longlonglongrightarrow> y"
shows "x \<le> y"
using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
lemma incseq_le_ereal:
fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
assumes inc: "incseq X"
- and lim: "X ----> L"
+ and lim: "X \<longlonglongrightarrow> L"
shows "X N \<le> L"
using inc
by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
lemma decseq_ge_ereal:
assumes dec: "decseq X"
- and lim: "X ----> (L::'a::linorder_topology)"
+ and lim: "X \<longlonglongrightarrow> (L::'a::linorder_topology)"
shows "X N \<ge> L"
using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
@@ -3491,21 +3491,21 @@
lemma ereal_Sup_lim:
fixes a :: "'a::{complete_linorder,linorder_topology}"
assumes "\<And>n. b n \<in> s"
- and "b ----> a"
+ and "b \<longlonglongrightarrow> a"
shows "a \<le> Sup s"
by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
lemma ereal_Inf_lim:
fixes a :: "'a::{complete_linorder,linorder_topology}"
assumes "\<And>n. b n \<in> s"
- and "b ----> a"
+ and "b \<longlonglongrightarrow> a"
shows "Inf s \<le> a"
by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
lemma SUP_Lim_ereal:
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
assumes inc: "incseq X"
- and l: "X ----> l"
+ and l: "X \<longlonglongrightarrow> l"
shows "(SUP n. X n) = l"
using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
by simp
@@ -3513,25 +3513,25 @@
lemma INF_Lim_ereal:
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
assumes dec: "decseq X"
- and l: "X ----> l"
+ and l: "X \<longlonglongrightarrow> l"
shows "(INF n. X n) = l"
using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
by simp
lemma SUP_eq_LIMSEQ:
assumes "mono f"
- shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
+ shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f \<longlonglongrightarrow> x"
proof
have inc: "incseq (\<lambda>i. ereal (f i))"
using \<open>mono f\<close> unfolding mono_def incseq_def by auto
{
- assume "f ----> x"
- then have "(\<lambda>i. ereal (f i)) ----> ereal x"
+ assume "f \<longlonglongrightarrow> x"
+ then have "(\<lambda>i. ereal (f i)) \<longlonglongrightarrow> ereal x"
by auto
from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
next
assume "(SUP n. ereal (f n)) = ereal x"
- with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
+ with LIMSEQ_SUP[OF inc] show "f \<longlonglongrightarrow> x" by auto
}
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Dec 29 23:04:53 2015 +0100
@@ -898,8 +898,8 @@
apply (simp add: setsum.delta')
done
-lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) ----> a"
- (is "?s ----> a")
+lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a"
+ (is "?s \<longlonglongrightarrow> a")
proof -
have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r
proof -
@@ -4413,11 +4413,11 @@
show "convergent X"
proof (rule convergentI)
- show "X ----> Abs_fps (\<lambda>i. X (M i) $ i)"
+ show "X \<longlonglongrightarrow> Abs_fps (\<lambda>i. X (M i) $ i)"
unfolding tendsto_iff
proof safe
fix e::real assume e: "0 < e"
- have "(\<lambda>n. inverse (2 ^ n) :: real) ----> 0" by (rule LIMSEQ_inverse_realpow_zero) simp_all
+ have "(\<lambda>n. inverse (2 ^ n) :: real) \<longlonglongrightarrow> 0" by (rule LIMSEQ_inverse_realpow_zero) simp_all
from this and e have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
by (rule order_tendstoD)
then obtain i where "inverse (2 ^ i) < e"
--- a/src/HOL/Library/Indicator_Function.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Tue Dec 29 23:04:53 2015 +0100
@@ -83,7 +83,7 @@
lemma LIMSEQ_indicator_incseq:
assumes "incseq A"
- shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
+ shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
proof cases
assume "\<exists>i. x \<in> A i"
then obtain i where "x \<in> A i"
@@ -97,9 +97,9 @@
qed (auto simp: indicator_def)
lemma LIMSEQ_indicator_UN:
- "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
+ "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
proof -
- have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union>i<k. A i) x"
+ have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x"
by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
by auto
@@ -108,7 +108,7 @@
lemma LIMSEQ_indicator_decseq:
assumes "decseq A"
- shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
+ shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
proof cases
assume "\<exists>i. x \<notin> A i"
then obtain i where "x \<notin> A i"
@@ -122,9 +122,9 @@
qed (auto simp: indicator_def)
lemma LIMSEQ_indicator_INT:
- "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
+ "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
proof -
- have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
+ have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x"
by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
by auto
--- a/src/HOL/Library/Liminf_Limsup.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Tue Dec 29 23:04:53 2015 +0100
@@ -365,9 +365,9 @@
lemma lim_increasing_cl:
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
- obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+ obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
proof
- show "f ----> (SUP n. f n)"
+ show "f \<longlonglongrightarrow> (SUP n. f n)"
using assms
by (intro increasing_tendsto)
(auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
@@ -375,9 +375,9 @@
lemma lim_decreasing_cl:
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
- obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+ obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
proof
- show "f ----> (INF n. f n)"
+ show "f \<longlonglongrightarrow> (INF n. f n)"
using assms
by (intro decreasing_tendsto)
(auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
@@ -385,7 +385,7 @@
lemma compact_complete_linorder:
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
+ shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
proof -
obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
using seq_monosub[of X]
@@ -393,7 +393,7 @@
by auto
then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
by (auto simp add: monoseq_def)
- then obtain l where "(X \<circ> r) ----> l"
+ then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
by auto
then show ?thesis
--- a/src/HOL/Library/Lub_Glb.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/Lub_Glb.thy Tue Dec 29 23:04:53 2015 +0100
@@ -223,9 +223,9 @@
fixes X :: "nat \<Rightarrow> real"
assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
- shows "X ----> u"
+ shows "X \<longlonglongrightarrow> u"
proof -
- have "X ----> (SUP i. X i)"
+ have "X \<longlonglongrightarrow> (SUP i. X i)"
using u[THEN isLubD1] X
by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
also have "(SUP i. X i) = u"
--- a/src/HOL/Library/Product_Vector.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/Product_Vector.thy Tue Dec 29 23:04:53 2015 +0100
@@ -383,13 +383,13 @@
instance prod :: (complete_space, complete_space) complete_space
proof
fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
- have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
+ have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
using Cauchy_fst [OF \<open>Cauchy X\<close>]
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
- have 2: "(\<lambda>n. snd (X n)) ----> lim (\<lambda>n. snd (X n))"
+ have 2: "(\<lambda>n. snd (X n)) \<longlonglongrightarrow> lim (\<lambda>n. snd (X n))"
using Cauchy_snd [OF \<open>Cauchy X\<close>]
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
- have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
+ have "X \<longlonglongrightarrow> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
using tendsto_Pair [OF 1 2] by simp
then show "convergent X"
by (rule convergentI)
--- a/src/HOL/Limits.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Limits.thy Tue Dec 29 23:04:53 2015 +0100
@@ -329,7 +329,7 @@
(* TODO: delete *)
(* FIXME: one use in NSA/HSEQ.thy *)
-lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
+lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X \<longlonglongrightarrow> L)"
apply (rule_tac x="X m" in exI)
apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
unfolding eventually_sequentially
@@ -1468,25 +1468,25 @@
subsection \<open>Limits of Sequences\<close>
-lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
+lemma [trans]: "X=Y ==> Y \<longlonglongrightarrow> z ==> X \<longlonglongrightarrow> z"
by simp
lemma LIMSEQ_iff:
fixes L :: "'a::real_normed_vector"
- shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
+ shows "(X \<longlonglongrightarrow> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
unfolding lim_sequentially dist_norm ..
lemma LIMSEQ_I:
fixes L :: "'a::real_normed_vector"
- shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
+ shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X \<longlonglongrightarrow> L"
by (simp add: LIMSEQ_iff)
lemma LIMSEQ_D:
fixes L :: "'a::real_normed_vector"
- shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
+ shows "\<lbrakk>X \<longlonglongrightarrow> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
by (simp add: LIMSEQ_iff)
-lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
+lemma LIMSEQ_linear: "\<lbrakk> X \<longlonglongrightarrow> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) \<longlonglongrightarrow> x"
unfolding tendsto_def eventually_sequentially
by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute)
@@ -1499,7 +1499,7 @@
lemma Bseq_inverse:
fixes a :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
+ shows "\<lbrakk>X \<longlonglongrightarrow> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
by (rule Bfun_inverse)
text\<open>Transformation of limit.\<close>
@@ -1607,7 +1607,7 @@
text\<open>An unbounded sequence's inverse tends to 0\<close>
lemma LIMSEQ_inverse_zero:
- "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
+ "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
apply (rule filterlim_compose[OF tendsto_inverse_0])
apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
@@ -1615,7 +1615,7 @@
text\<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity\<close>
-lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
+lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) \<longlonglongrightarrow> 0"
by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
@@ -1623,16 +1623,16 @@
infinity is now easily proved\<close>
lemma LIMSEQ_inverse_real_of_nat_add:
- "(%n. r + inverse(real(Suc n))) ----> r"
+ "(%n. r + inverse(real(Suc n))) \<longlonglongrightarrow> r"
using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
lemma LIMSEQ_inverse_real_of_nat_add_minus:
- "(%n. r + -inverse(real(Suc n))) ----> r"
+ "(%n. r + -inverse(real(Suc n))) \<longlonglongrightarrow> r"
using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
by auto
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
- "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
+ "(%n. r*( 1 + -inverse(real(Suc n)))) \<longlonglongrightarrow> r"
using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
by auto
@@ -1649,24 +1649,24 @@
lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially"
using lim_1_over_n by (simp add: inverse_eq_divide)
-lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) ----> 1"
+lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: field_simps)
- have "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1 + 0"
+ have "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) \<longlonglongrightarrow> 1 + 0"
by (intro tendsto_add tendsto_const lim_inverse_n)
- thus "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1" by simp
+ thus "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) \<longlonglongrightarrow> 1" by simp
qed
-lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) ----> 1"
+lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) =
of_nat n / of_nat (Suc n)) sequentially"
using eventually_gt_at_top[of "0::nat"]
by eventually_elim (simp add: field_simps del: of_nat_Suc)
- have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> inverse 1"
+ have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> inverse 1"
by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
- thus "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> 1" by simp
+ thus "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> 1" by simp
qed
subsection \<open>Convergence on sequences\<close>
@@ -1733,8 +1733,8 @@
assumes "convergent f"
shows "convergent (\<lambda>n. norm (f n))"
proof -
- from assms have "f ----> lim f" by (simp add: convergent_LIMSEQ_iff)
- hence "(\<lambda>n. norm (f n)) ----> norm (lim f)" by (rule tendsto_norm)
+ from assms have "f \<longlonglongrightarrow> lim f" by (simp add: convergent_LIMSEQ_iff)
+ hence "(\<lambda>n. norm (f n)) \<longlonglongrightarrow> norm (lim f)" by (rule tendsto_norm)
thus ?thesis by (auto simp: convergent_def)
qed
@@ -1794,7 +1794,7 @@
fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
assumes u: "bdd_above (range X)"
assumes X: "incseq X"
- shows "X ----> (SUP i. X i)"
+ shows "X \<longlonglongrightarrow> (SUP i. X i)"
by (rule order_tendstoI)
(auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])
@@ -1802,7 +1802,7 @@
fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
assumes u: "bdd_below (range X)"
assumes X: "decseq X"
- shows "X ----> (INF i. X i)"
+ shows "X \<longlonglongrightarrow> (INF i. X i)"
by (rule order_tendstoI)
(auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
@@ -1845,24 +1845,24 @@
lemma incseq_convergent:
fixes X :: "nat \<Rightarrow> real"
assumes "incseq X" and "\<forall>i. X i \<le> B"
- obtains L where "X ----> L" "\<forall>i. X i \<le> L"
+ obtains L where "X \<longlonglongrightarrow> L" "\<forall>i. X i \<le> L"
proof atomize_elim
from incseq_bounded[OF assms] \<open>incseq X\<close> Bseq_monoseq_convergent[of X]
- obtain L where "X ----> L"
+ obtain L where "X \<longlonglongrightarrow> L"
by (auto simp: convergent_def monoseq_def incseq_def)
- with \<open>incseq X\<close> show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
+ with \<open>incseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. X i \<le> L)"
by (auto intro!: exI[of _ L] incseq_le)
qed
lemma decseq_convergent:
fixes X :: "nat \<Rightarrow> real"
assumes "decseq X" and "\<forall>i. B \<le> X i"
- obtains L where "X ----> L" "\<forall>i. L \<le> X i"
+ obtains L where "X \<longlonglongrightarrow> L" "\<forall>i. L \<le> X i"
proof atomize_elim
from decseq_bounded[OF assms] \<open>decseq X\<close> Bseq_monoseq_convergent[of X]
- obtain L where "X ----> L"
+ obtain L where "X \<longlonglongrightarrow> L"
by (auto simp: convergent_def monoseq_def decseq_def)
- with \<open>decseq X\<close> show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
+ with \<open>decseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. L \<le> X i)"
by (auto intro!: exI[of _ L] decseq_le)
qed
@@ -1901,39 +1901,39 @@
"[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
-lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
+lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) \<longlonglongrightarrow> 0"
by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
lemma LIMSEQ_realpow_zero:
- "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
+ "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
proof cases
assume "0 \<le> x" and "x \<noteq> 0"
hence x0: "0 < x" by simp
assume x1: "x < 1"
from x0 x1 have "1 < inverse x"
by (rule one_less_inverse)
- hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
+ hence "(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_inverse_realpow_zero)
thus ?thesis by (simp add: power_inverse)
qed (rule LIMSEQ_imp_Suc, simp)
lemma LIMSEQ_power_zero:
fixes x :: "'a::{real_normed_algebra_1}"
- shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
+ shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
apply (simp add: power_abs norm_power_ineq)
done
-lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
+lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) \<longlonglongrightarrow> 0"
by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
text\<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}\<close>
-lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
+lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
-lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
+lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_power_zero) simp
@@ -2162,8 +2162,8 @@
subsection \<open>Nested Intervals and Bisection -- Needed for Compactness\<close>
lemma nested_sequence_unique:
- assumes "\<forall>n. f n \<le> f (Suc n)" "\<forall>n. g (Suc n) \<le> g n" "\<forall>n. f n \<le> g n" "(\<lambda>n. f n - g n) ----> 0"
- shows "\<exists>l::real. ((\<forall>n. f n \<le> l) \<and> f ----> l) \<and> ((\<forall>n. l \<le> g n) \<and> g ----> l)"
+ assumes "\<forall>n. f n \<le> f (Suc n)" "\<forall>n. g (Suc n) \<le> g n" "\<forall>n. f n \<le> g n" "(\<lambda>n. f n - g n) \<longlonglongrightarrow> 0"
+ shows "\<exists>l::real. ((\<forall>n. f n \<le> l) \<and> f \<longlonglongrightarrow> l) \<and> ((\<forall>n. l \<le> g n) \<and> g \<longlonglongrightarrow> l)"
proof -
have "incseq f" unfolding incseq_Suc_iff by fact
have "decseq g" unfolding decseq_Suc_iff by fact
@@ -2171,15 +2171,15 @@
{ fix n
from \<open>decseq g\<close> have "g n \<le> g 0" by (rule decseqD) simp
with \<open>\<forall>n. f n \<le> g n\<close>[THEN spec, of n] have "f n \<le> g 0" by auto }
- then obtain u where "f ----> u" "\<forall>i. f i \<le> u"
+ then obtain u where "f \<longlonglongrightarrow> u" "\<forall>i. f i \<le> u"
using incseq_convergent[OF \<open>incseq f\<close>] by auto
moreover
{ fix n
from \<open>incseq f\<close> have "f 0 \<le> f n" by (rule incseqD) simp
with \<open>\<forall>n. f n \<le> g n\<close>[THEN spec, of n] have "f 0 \<le> g n" by simp }
- then obtain l where "g ----> l" "\<forall>i. l \<le> g i"
+ then obtain l where "g \<longlonglongrightarrow> l" "\<forall>i. l \<le> g i"
using decseq_convergent[OF \<open>decseq g\<close>] by auto
- moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \<open>f ----> u\<close> \<open>g ----> l\<close>]]
+ moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \<open>f \<longlonglongrightarrow> u\<close> \<open>g \<longlonglongrightarrow> l\<close>]]
ultimately show ?thesis by auto
qed
@@ -2198,14 +2198,14 @@
{ fix n have "l n \<le> u n" by (induct n) auto } note this[simp]
- have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l ----> x) \<and> ((\<forall>n. x \<le> u n) \<and> u ----> x)"
+ have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l \<longlonglongrightarrow> x) \<and> ((\<forall>n. x \<le> u n) \<and> u \<longlonglongrightarrow> x)"
proof (safe intro!: nested_sequence_unique)
fix n show "l n \<le> l (Suc n)" "u (Suc n) \<le> u n" by (induct n) auto
next
{ fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) }
- then show "(\<lambda>n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero)
+ then show "(\<lambda>n. l n - u n) \<longlonglongrightarrow> 0" by (simp add: LIMSEQ_divide_realpow_zero)
qed fact
- then obtain x where x: "\<And>n. l n \<le> x" "\<And>n. x \<le> u n" and "l ----> x" "u ----> x" by auto
+ then obtain x where x: "\<And>n. l n \<le> x" "\<And>n. x \<le> u n" and "l \<longlonglongrightarrow> x" "u \<longlonglongrightarrow> x" by auto
obtain d where "0 < d" and d: "\<And>a b. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> b - a < d \<Longrightarrow> P a b"
using \<open>l 0 \<le> x\<close> \<open>x \<le> u 0\<close> local[of x] by auto
@@ -2218,9 +2218,9 @@
qed (simp add: \<open>\<not> P a b\<close>) }
moreover
{ have "eventually (\<lambda>n. x - d / 2 < l n) sequentially"
- using \<open>0 < d\<close> \<open>l ----> x\<close> by (intro order_tendstoD[of _ x]) auto
+ using \<open>0 < d\<close> \<open>l \<longlonglongrightarrow> x\<close> by (intro order_tendstoD[of _ x]) auto
moreover have "eventually (\<lambda>n. u n < x + d / 2) sequentially"
- using \<open>0 < d\<close> \<open>u ----> x\<close> by (intro order_tendstoD[of _ x]) auto
+ using \<open>0 < d\<close> \<open>u \<longlonglongrightarrow> x\<close> by (intro order_tendstoD[of _ x]) auto
ultimately have "eventually (\<lambda>n. P (l n) (u n)) sequentially"
proof eventually_elim
fix n assume "x - d / 2 < l n" "u n < x + d / 2"
--- a/src/HOL/Metis_Examples/Clausification.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Metis_Examples/Clausification.thy Tue Dec 29 23:04:53 2015 +0100
@@ -115,7 +115,7 @@
lemma
fixes x :: real
- assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
+ assumes fn_le: "!!n. f n \<le> x" and 1: "f \<longlonglongrightarrow> lim f"
shows "lim f \<le> x"
by (metis 1 LIMSEQ_le_const2 fn_le)
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Tue Dec 29 23:04:53 2015 +0100
@@ -138,7 +138,7 @@
unfolding closed_sequential_limits
proof safe
fix f l
- assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f ----> l"
+ assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l"
have lim_fun: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (Rep_bcontfun l x) < e"
using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
@@ -156,7 +156,7 @@
by (auto simp: Abs_bcontfun_inverse)
qed
moreover note sequentially_bot
- moreover have "(\<lambda>n. Rep_bcontfun (f n) x) ----> Rep_bcontfun l x"
+ moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x"
using lim_fun by (blast intro!: metric_LIMSEQ_I)
ultimately show "Rep_bcontfun l x \<in> X x"
by (rule Lim_in_closed_set)
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Dec 29 23:04:53 2015 +0100
@@ -249,7 +249,7 @@
by (subst xy) (simp add: blinfun.bilinear_simps)
finally have "convergent (\<lambda>n. X n x)" .
}
- then obtain v where v: "\<And>x. (\<lambda>n. X n x) ----> v x"
+ then obtain v where v: "\<And>x. (\<lambda>n. X n x) \<longlonglongrightarrow> v x"
unfolding convergent_def
by metis
@@ -269,7 +269,7 @@
finally show "norm (norm (X m) - norm (X n)) < e" .
qed
qed
- then obtain K where K: "(\<lambda>n. norm (X n)) ----> K"
+ then obtain K where K: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow> K"
unfolding Cauchy_convergent_iff convergent_def
by metis
@@ -290,10 +290,10 @@
by (simp add: ac_simps)
qed
qed
- hence Bv: "\<And>x. (\<lambda>n. X n x) ----> Blinfun v x"
+ hence Bv: "\<And>x. (\<lambda>n. X n x) \<longlonglongrightarrow> Blinfun v x"
by (auto simp: bounded_linear_Blinfun_apply v)
- have "X ----> Blinfun v"
+ have "X \<longlonglongrightarrow> Blinfun v"
proof (rule LIMSEQ_I)
fix r::real assume "r > 0"
def r' \<equiv> "r / 2"
@@ -320,7 +320,7 @@
using M[OF n elim] by (simp add: mult_right_mono)
finally show ?case .
qed
- have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) ----> norm (X n x - Blinfun v x)"
+ have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) \<longlonglongrightarrow> norm (X n x - Blinfun v x)"
by (auto intro!: tendsto_intros Bv)
show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Dec 29 23:04:53 2015 +0100
@@ -838,7 +838,7 @@
proof (rule has_derivative_sequence [OF cvs _ _ x])
show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (op * (f' n x))) (at x within s)"
by (metis has_field_derivative_def df)
- next show "(\<lambda>n. f n x) ----> l"
+ next show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
by (rule tf)
next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
by (blast intro: **)
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Dec 29 23:04:53 2015 +0100
@@ -1636,7 +1636,7 @@
have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
using ln3_gt_1
by (force intro: order_trans [of _ "ln 3"] ln3_gt_1)
- moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) ----> 0"
+ moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) \<longlonglongrightarrow> 0"
using lim_Ln_over_power [OF assms]
by (metis tendsto_norm_zero_iff)
ultimately show ?thesis
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Dec 29 23:04:53 2015 +0100
@@ -1957,7 +1957,7 @@
qed
qed
qed
- then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) ----> g x" ..
+ then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
proof (rule, rule)
fix e :: real
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Dec 29 23:04:53 2015 +0100
@@ -366,10 +366,10 @@
instance vec :: (complete_space, finite) complete_space
proof
fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"
- have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)"
+ have "\<And>i. (\<lambda>n. X n $ i) \<longlonglongrightarrow> lim (\<lambda>n. X n $ i)"
using Cauchy_vec_nth [OF \<open>Cauchy X\<close>]
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
- hence "X ----> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
+ hence "X \<longlonglongrightarrow> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
by (simp add: vec_tendstoI)
then show "convergent X"
by (rule convergentI)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 29 23:04:53 2015 +0100
@@ -4580,7 +4580,7 @@
by (auto intro!: triangle3)
qed
qed
- then obtain s where s: "i ----> s"
+ then obtain s where s: "i \<longlonglongrightarrow> s"
using convergent_eq_cauchy[symmetric] by blast
show ?thesis
unfolding integrable_on_def has_integral
@@ -10201,8 +10201,8 @@
fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow> real"
assumes f: "\<And>k. (f k has_integral x k) s"
assumes "\<And>k x. x \<in> s \<Longrightarrow> f k x \<le> f (Suc k) x"
- assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>k. f k x) ----> g x"
- assumes "x ----> x'"
+ assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+ assumes "x \<longlonglongrightarrow> x'"
shows "(g has_integral x') s"
proof -
have x_eq: "x = (\<lambda>i. integral s (f i))"
@@ -10210,13 +10210,13 @@
then have x: "{integral s (f k) |k. True} = range x"
by auto
- have "g integrable_on s \<and> (\<lambda>k. integral s (f k)) ----> integral s g"
+ have "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
proof (intro monotone_convergence_increasing allI ballI assms)
show "bounded {integral s (f k) |k. True}"
unfolding x by (rule convergent_imp_bounded) fact
qed (auto intro: f)
moreover then have "integral s g = x'"
- by (intro LIMSEQ_unique[OF _ \<open>x ----> x'\<close>]) (simp add: x_eq)
+ by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq)
ultimately show ?thesis
by (simp add: has_integral_integral)
qed
@@ -12087,7 +12087,7 @@
show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)
- show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
+ show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) \<longlonglongrightarrow> g x"
proof (rule LIMSEQ_I, goal_cases)
case r: (1 r)
then have "0<r/2"
@@ -12183,8 +12183,8 @@
lemma has_integral_dominated_convergence:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
- "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) ----> g x"
- and x: "y ----> x"
+ "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+ and x: "y \<longlonglongrightarrow> x"
shows "(g has_integral x) s"
proof -
have int_f: "\<And>k. (f k) integrable_on s"
@@ -12193,9 +12193,9 @@
by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
moreover have "integral s g = x"
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral s (f i)) ----> x"
+ show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
using integral_unique[OF assms(1)] x by simp
- show "(\<lambda>i. integral s (f i)) ----> integral s g"
+ show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
by (intro dominated_convergence[OF int_f assms(2)]) fact+
qed
ultimately show ?thesis
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Dec 29 23:04:53 2015 +0100
@@ -39,7 +39,7 @@
using dist_triangle[of y z x] by (simp add: dist_commute)
(* LEGACY *)
-lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l"
+lemma lim_subseq: "subseq r \<Longrightarrow> s \<longlonglongrightarrow> l \<Longrightarrow> (s \<circ> r) \<longlonglongrightarrow> l"
by (rule LIMSEQ_subseq_LIMSEQ)
lemma countable_PiE:
@@ -2365,7 +2365,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 ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
+ 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)"
using assms unfolding tendsto_def [where l=L]
by (simp add: sequentially_imp_eventually_within)
@@ -2430,7 +2430,7 @@
then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
}
then have "\<forall>n. f n \<in> S - {x}" by auto
- moreover have "(\<lambda>n. f n) ----> x"
+ moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
proof (rule topological_tendstoI)
fix S
assume "open S" "x \<in> S"
@@ -2441,7 +2441,7 @@
ultimately show ?rhs by fast
next
assume ?rhs
- then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x"
+ then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
by auto
show ?lhs
unfolding islimpt_def
@@ -3515,7 +3515,7 @@
lemma acc_point_range_imp_convergent_subsequence:
fixes l :: "'a :: first_countable_topology"
assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
- shows "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+ shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
proof -
from countable_basis_at_decseq[of l]
obtain A where A:
@@ -3542,7 +3542,7 @@
have "subseq r"
by (auto simp: r_def s subseq_Suc_iff)
moreover
- have "(\<lambda>n. f (r n)) ----> l"
+ have "(\<lambda>n. f (r n)) \<longlonglongrightarrow> l"
proof (rule topological_tendstoI)
fix S
assume "open S" "l \<in> S"
@@ -3560,7 +3560,7 @@
ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
by eventually_elim auto
qed
- ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+ ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
by (auto simp: convergent_def comp_def)
qed
@@ -3658,7 +3658,7 @@
lemma islimpt_range_imp_convergent_subsequence:
fixes l :: "'a :: {t1_space, first_countable_topology}"
assumes l: "l islimpt (range f)"
- shows "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+ shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
using l unfolding islimpt_eq_acc_point
by (rule acc_point_range_imp_convergent_subsequence)
@@ -3987,11 +3987,11 @@
using assms unfolding seq_compact_def by fast
lemma closed_sequentially: (* TODO: move upwards *)
- assumes "closed s" and "\<forall>n. f n \<in> s" and "f ----> l"
+ assumes "closed s" and "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> l"
shows "l \<in> s"
proof (rule ccontr)
assume "l \<notin> s"
- with \<open>closed s\<close> and \<open>f ----> l\<close> have "eventually (\<lambda>n. f n \<in> - s) sequentially"
+ with \<open>closed s\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "eventually (\<lambda>n. f n \<in> - s) sequentially"
by (fast intro: topological_tendstoD)
with \<open>\<forall>n. f n \<in> s\<close> show "False"
by simp
@@ -4005,13 +4005,13 @@
hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
by simp_all
from \<open>seq_compact s\<close> and \<open>\<forall>n. f n \<in> s\<close>
- obtain l r where "l \<in> s" and r: "subseq r" and l: "(f \<circ> r) ----> l"
+ obtain l r where "l \<in> s" and r: "subseq r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
by (rule seq_compactE)
from \<open>\<forall>n. f n \<in> t\<close> have "\<forall>n. (f \<circ> r) n \<in> t"
by simp
from \<open>closed t\<close> and this and l have "l \<in> t"
by (rule closed_sequentially)
- with \<open>l \<in> s\<close> and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+ with \<open>l \<in> s\<close> and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
by fast
qed
@@ -4027,7 +4027,7 @@
proof (safe intro!: countably_compactI)
fix A
assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
- have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) ----> x"
+ have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
using \<open>seq_compact U\<close> by (fastforce simp: seq_compact_def subset_eq)
show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
proof cases
@@ -4048,7 +4048,7 @@
using \<open>A \<noteq> {}\<close> unfolding X_def SUP_def by (intro T) (auto intro: from_nat_into)
then have "range X \<subseteq> U"
by auto
- with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) ----> x"
+ with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) \<longlonglongrightarrow> x"
by auto
from \<open>x\<in>U\<close> \<open>U \<subseteq> \<Union>A\<close> from_nat_into_surj[OF \<open>countable A\<close>]
obtain n where "x \<in> from_nat_into A n" by auto
@@ -4115,7 +4115,7 @@
have "subseq r"
by (auto simp: r_def s subseq_Suc_iff)
moreover
- have "(\<lambda>n. X (r n)) ----> x"
+ have "(\<lambda>n. X (r n)) \<longlonglongrightarrow> x"
proof (rule topological_tendstoI)
fix S
assume "open S" "x \<in> S"
@@ -4133,7 +4133,7 @@
ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
by eventually_elim auto
qed
- ultimately show "\<exists>x \<in> U. \<exists>r. subseq r \<and> (X \<circ> r) ----> x"
+ ultimately show "\<exists>x \<in> U. \<exists>r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
using \<open>x \<in> U\<close> by (auto simp: convergent_def comp_def)
qed
@@ -4191,9 +4191,9 @@
using pigeonhole_infinite[OF _ True] by auto
then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l"
using infinite_enumerate by blast
- then have "subseq r \<and> (f \<circ> r) ----> f l"
+ then have "subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
by (simp add: fr o_def)
- with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+ with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
by auto
next
case False
@@ -4326,7 +4326,7 @@
lemma compact_def:
"compact (S :: 'a::metric_space set) \<longleftrightarrow>
- (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f \<circ> r) ----> l))"
+ (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
unfolding compact_eq_seq_compact_metric seq_compact_def by auto
subsubsection \<open>Complete the chain of compactness variants\<close>
@@ -4405,7 +4405,7 @@
(* TODO: is this lemma necessary? *)
lemma bounded_increasing_convergent:
fixes s :: "nat \<Rightarrow> real"
- shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s (Suc n) \<Longrightarrow> \<exists>l. s ----> l"
+ shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s (Suc n) \<Longrightarrow> \<exists>l. s \<longlonglongrightarrow> l"
using Bseq_mono_convergent[of s] incseq_Suc_iff[of s]
by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
@@ -4417,7 +4417,7 @@
unfolding comp_def by (metis seq_monosub)
then have "Bseq (f \<circ> r)"
unfolding Bseq_eq_bounded using f by (force intro: bounded_subset)
- with r show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
+ with r show "\<exists>l r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
qed
@@ -4531,7 +4531,7 @@
by (rule bounded_fst)
then have s1: "bounded (range (fst \<circ> f))"
by (simp add: image_comp)
- obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1"
+ obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
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)
@@ -4551,16 +4551,16 @@
subsubsection \<open>Completeness\<close>
definition complete :: "'a::metric_space set \<Rightarrow> bool"
- where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
+ where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f \<longlonglongrightarrow> l))"
lemma completeI:
- assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f ----> l"
+ assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
shows "complete s"
using assms unfolding complete_def by fast
lemma completeE:
assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
- obtains l where "l \<in> s" and "f ----> l"
+ obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
using assms unfolding complete_def by fast
lemma compact_imp_complete:
@@ -4570,7 +4570,7 @@
{
fix f
assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
- from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) ----> l"
+ from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) \<longlonglongrightarrow> l"
using assms unfolding compact_def by blast
note lr' = seq_suble [OF lr(2)]
@@ -4706,7 +4706,7 @@
by (simp add: dist_commute)
qed
- ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+ ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
using assms unfolding complete_def by blast
qed
qed
@@ -4789,19 +4789,19 @@
proof (rule completeI)
fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
then have "convergent f" by (rule Cauchy_convergent)
- then show "\<exists>l\<in>UNIV. f ----> l" unfolding convergent_def by simp
+ then show "\<exists>l\<in>UNIV. f \<longlonglongrightarrow> l" unfolding convergent_def by simp
qed
lemma complete_imp_closed:
assumes "complete s"
shows "closed s"
proof (unfold closed_sequential_limits, clarify)
- fix f x assume "\<forall>n. f n \<in> s" and "f ----> x"
- from \<open>f ----> x\<close> have "Cauchy f"
+ fix f x assume "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> x"
+ from \<open>f \<longlonglongrightarrow> x\<close> have "Cauchy f"
by (rule LIMSEQ_imp_Cauchy)
- with \<open>complete s\<close> and \<open>\<forall>n. f n \<in> s\<close> obtain l where "l \<in> s" and "f ----> l"
+ with \<open>complete s\<close> and \<open>\<forall>n. f n \<in> s\<close> obtain l where "l \<in> s" and "f \<longlonglongrightarrow> l"
by (rule completeE)
- from \<open>f ----> x\<close> and \<open>f ----> l\<close> have "x = l"
+ from \<open>f \<longlonglongrightarrow> x\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "x = l"
by (rule LIMSEQ_unique)
with \<open>l \<in> s\<close> show "x \<in> s"
by simp
@@ -4814,11 +4814,11 @@
fix f assume "\<forall>n. f n \<in> s \<inter> t" and "Cauchy f"
then have "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
by simp_all
- from \<open>complete s\<close> obtain l where "l \<in> s" and "f ----> l"
+ from \<open>complete s\<close> obtain l where "l \<in> s" and "f \<longlonglongrightarrow> l"
using \<open>\<forall>n. f n \<in> s\<close> and \<open>Cauchy f\<close> by (rule completeE)
- from \<open>closed t\<close> and \<open>\<forall>n. f n \<in> t\<close> and \<open>f ----> l\<close> have "l \<in> t"
+ from \<open>closed t\<close> and \<open>\<forall>n. f n \<in> t\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "l \<in> t"
by (rule closed_sequentially)
- with \<open>l \<in> s\<close> and \<open>f ----> l\<close> show "\<exists>l\<in>s \<inter> t. f ----> l"
+ with \<open>l \<in> s\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>s \<inter> t. f \<longlonglongrightarrow> l"
by fast
qed
@@ -4887,7 +4887,7 @@
using choice[of "\<lambda>n x. x \<in> s n"] by auto
from assms(4,1) have "seq_compact (s 0)"
by (simp add: bounded_closed_imp_seq_compact)
- then obtain l r where lr: "l \<in> s 0" "subseq r" "(x \<circ> r) ----> l"
+ then obtain l r where lr: "l \<in> s 0" "subseq r" "(x \<circ> r) \<longlonglongrightarrow> l"
using x and assms(3) unfolding seq_compact_def by blast
have "\<forall>n. l \<in> s n"
proof
@@ -4898,7 +4898,7 @@
using x and assms(3) and lr(2) [THEN seq_suble] by auto
then have "\<forall>i. (x \<circ> r) (i + n) \<in> s n"
using assms(3) by (fast intro!: le_add2)
- moreover have "(\<lambda>i. (x \<circ> r) (i + n)) ----> l"
+ moreover have "(\<lambda>i. (x \<circ> r) (i + n)) \<longlonglongrightarrow> l"
using lr(3) by (rule LIMSEQ_ignore_initial_segment)
ultimately show "l \<in> s n"
by (rule closed_sequentially)
@@ -5497,9 +5497,9 @@
} note le = this
{
fix x y
- assume f: "(\<lambda>n. dist (f (x n)) (f (y n))) ----> 0"
- assume g: "(\<lambda>n. dist (g (x n)) (g (y n))) ----> 0"
- have "(\<lambda>n. \<bar>dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\<bar>) ----> 0"
+ assume f: "(\<lambda>n. dist (f (x n)) (f (y n))) \<longlonglongrightarrow> 0"
+ assume g: "(\<lambda>n. dist (g (x n)) (g (y n))) \<longlonglongrightarrow> 0"
+ have "(\<lambda>n. \<bar>dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\<bar>) \<longlonglongrightarrow> 0"
by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]],
simp add: le)
}
@@ -5589,8 +5589,8 @@
lemma continuous_imp_tendsto:
assumes "continuous (at x0) f"
- and "x ----> x0"
- shows "(f \<circ> x) ----> (f x0)"
+ and "x \<longlonglongrightarrow> x0"
+ shows "(f \<circ> x) \<longlonglongrightarrow> (f x0)"
proof (rule topological_tendstoI)
fix S
assume "open S" "f x0 \<in> S"
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Dec 29 23:04:53 2015 +0100
@@ -207,7 +207,7 @@
show "\<forall>x\<in>X. dist (f n x) (?f x) < e"
proof
fix x assume x: "x \<in> X"
- with assms have "(\<lambda>n. f n x) ----> ?f x"
+ with assms have "(\<lambda>n. f n x) \<longlonglongrightarrow> ?f x"
by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
with \<open>e/2 > 0\<close> have "eventually (\<lambda>m. m \<ge> N \<and> dist (f m x) (?f x) < e/2) sequentially"
by (intro tendstoD eventually_conj eventually_ge_at_top)
--- a/src/HOL/NSA/HSEQ.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/NSA/HSEQ.thy Tue Dec 29 23:04:53 2015 +0100
@@ -162,7 +162,7 @@
subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
lemma LIMSEQ_NSLIMSEQ:
- assumes X: "X ----> L" shows "X ----NS> L"
+ assumes X: "X \<longlonglongrightarrow> L" shows "X ----NS> L"
proof (rule NSLIMSEQ_I)
fix N assume N: "N \<in> HNatInfinite"
have "starfun X N - star_of L \<in> Infinitesimal"
@@ -180,7 +180,7 @@
qed
lemma NSLIMSEQ_LIMSEQ:
- assumes X: "X ----NS> L" shows "X ----> L"
+ assumes X: "X ----NS> L" shows "X \<longlonglongrightarrow> L"
proof (rule LIMSEQ_I)
fix r::real assume r: "0 < r"
have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
@@ -199,7 +199,7 @@
by transfer
qed
-theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
+theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f ----NS> L)"
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
--- a/src/HOL/NthRoot.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/NthRoot.thy Tue Dec 29 23:04:53 2015 +0100
@@ -649,12 +649,12 @@
apply auto
done
-lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
+lemma LIMSEQ_root: "(\<lambda>n. root n n) \<longlonglongrightarrow> 1"
proof -
def x \<equiv> "\<lambda>n. root n n - 1"
- have "x ----> sqrt 0"
+ have "x \<longlonglongrightarrow> sqrt 0"
proof (rule tendsto_sandwich[OF _ _ tendsto_const])
- show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
+ show "(\<lambda>x. sqrt (2 / x)) \<longlonglongrightarrow> sqrt 0"
by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
(simp_all add: at_infinity_eq_at_top_bot)
{ fix n :: nat assume "2 < n"
@@ -686,13 +686,13 @@
lemma LIMSEQ_root_const:
assumes "0 < c"
- shows "(\<lambda>n. root n c) ----> 1"
+ shows "(\<lambda>n. root n c) \<longlonglongrightarrow> 1"
proof -
{ fix c :: real assume "1 \<le> c"
def x \<equiv> "\<lambda>n. root n c - 1"
- have "x ----> 0"
+ have "x \<longlonglongrightarrow> 0"
proof (rule tendsto_sandwich[OF _ _ tendsto_const])
- show "(\<lambda>n. c / n) ----> 0"
+ show "(\<lambda>n. c / n) \<longlonglongrightarrow> 0"
by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
(simp_all add: at_infinity_eq_at_top_bot)
{ fix n :: nat assume "1 < n"
@@ -713,7 +713,7 @@
show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
using \<open>1 \<le> c\<close> by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
qed
- from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
+ from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) \<longlonglongrightarrow> 1"
by (simp add: x_def) }
note ge_1 = this
@@ -724,7 +724,7 @@
assume "\<not> 1 \<le> c"
with \<open>0 < c\<close> have "1 \<le> 1 / c"
by simp
- then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
+ then have "(\<lambda>n. 1 / root n (1 / c)) \<longlonglongrightarrow> 1 / 1"
by (intro tendsto_divide tendsto_const ge_1 \<open>1 \<le> 1 / c\<close> one_neq_zero)
then show ?thesis
by (rule filterlim_cong[THEN iffD1, rotated 3])
--- a/src/HOL/Probability/Bochner_Integration.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Tue Dec 29 23:04:53 2015 +0100
@@ -18,7 +18,7 @@
lemma borel_measurable_implies_sequence_metric:
fixes f :: "'a \<Rightarrow> 'b :: {metric_space, second_countable_topology}"
assumes [measurable]: "f \<in> borel_measurable M"
- shows "\<exists>F. (\<forall>i. simple_function M (F i)) \<and> (\<forall>x\<in>space M. (\<lambda>i. F i x) ----> f x) \<and>
+ shows "\<exists>F. (\<forall>i. simple_function M (F i)) \<and> (\<forall>x\<in>space M. (\<lambda>i. F i x) \<longlonglongrightarrow> f x) \<and>
(\<forall>i. \<forall>x\<in>space M. dist (F i x) z \<le> 2 * dist (f x) z)"
proof -
obtain D :: "'b set" where "countable D" and D: "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
@@ -101,7 +101,7 @@
note * = this
fix x assume "x \<in> space M"
- show "(\<lambda>i. F i x) ----> f x"
+ show "(\<lambda>i. F i x) \<longlonglongrightarrow> f x"
proof cases
assume "f x = z"
then have "\<And>i n. x \<notin> A i n"
@@ -173,7 +173,7 @@
assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
- assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. U i x) ----> u x) \<Longrightarrow> P u"
+ assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. U i x) \<longlonglongrightarrow> u x) \<Longrightarrow> P u"
shows "P u"
proof -
have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M" using u by auto
@@ -199,13 +199,13 @@
intro!: real_of_ereal_positive_mono)
next
fix x assume x: "x \<in> space M"
- have "(\<lambda>i. U i x) ----> (SUP i. U i x)"
+ have "(\<lambda>i. U i x) \<longlonglongrightarrow> (SUP i. U i x)"
using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def)
moreover have "(\<lambda>i. U i x) = (\<lambda>i. ereal (U' i x))"
using x nn U(3) by (auto simp: fun_eq_iff U'_def ereal_real image_iff eq_commute)
moreover have "(SUP i. U i x) = ereal (u x)"
using sup u(2) by (simp add: max_def)
- ultimately show "(\<lambda>i. U' i x) ----> u x"
+ ultimately show "(\<lambda>i. U' i x) \<longlonglongrightarrow> u x"
by simp
next
fix i
@@ -516,8 +516,8 @@
for M f x where
"f \<in> borel_measurable M \<Longrightarrow>
(\<And>i. simple_bochner_integrable M (s i)) \<Longrightarrow>
- (\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) ----> 0 \<Longrightarrow>
- (\<lambda>i. simple_bochner_integral M (s i)) ----> x \<Longrightarrow>
+ (\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0 \<Longrightarrow>
+ (\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x \<Longrightarrow>
has_bochner_integral M f x"
lemma has_bochner_integral_cong:
@@ -530,7 +530,7 @@
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
unfolding has_bochner_integral.simps
- by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x ----> 0"]
+ by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x \<longlonglongrightarrow> 0"]
nn_integral_cong_AE)
auto
@@ -572,8 +572,8 @@
has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
fix sf sg
- assume f_sf: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - sf i x) \<partial>M) ----> 0"
- assume g_sg: "(\<lambda>i. \<integral>\<^sup>+ x. norm (g x - sg i x) \<partial>M) ----> 0"
+ assume f_sf: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - sf i x) \<partial>M) \<longlonglongrightarrow> 0"
+ assume g_sg: "(\<lambda>i. \<integral>\<^sup>+ x. norm (g x - sg i x) \<partial>M) \<longlonglongrightarrow> 0"
assume sf: "\<forall>i. simple_bochner_integrable M (sf i)"
and sg: "\<forall>i. simple_bochner_integrable M (sg i)"
@@ -584,10 +584,10 @@
show "\<And>i. simple_bochner_integrable M (\<lambda>x. sf i x + sg i x)"
using sf sg by (simp add: simple_bochner_integrable_compose2)
- show "(\<lambda>i. \<integral>\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \<partial>M) ----> 0"
- (is "?f ----> 0")
+ show "(\<lambda>i. \<integral>\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \<partial>M) \<longlonglongrightarrow> 0"
+ (is "?f \<longlonglongrightarrow> 0")
proof (rule tendsto_sandwich)
- show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
+ show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) \<longlonglongrightarrow> 0"
by (auto simp: nn_integral_nonneg)
show "eventually (\<lambda>i. ?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) \<partial>M) + \<integral>\<^sup>+ x. (norm (g x - sg i x)) \<partial>M) sequentially"
(is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
@@ -598,7 +598,7 @@
by (intro nn_integral_add) auto
finally show "?f i \<le> ?g i" .
qed
- show "?g ----> 0"
+ show "?g \<longlonglongrightarrow> 0"
using tendsto_add_ereal[OF _ _ f_sf g_sg] by simp
qed
qed (auto simp: simple_bochner_integral_add tendsto_add)
@@ -614,7 +614,7 @@
then show "(\<lambda>x. T (f x)) \<in> borel_measurable M"
by auto
- fix s assume f_s: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) ----> 0"
+ fix s assume f_s: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0"
assume s: "\<forall>i. simple_bochner_integrable M (s i)"
then show "\<And>i. simple_bochner_integrable M (\<lambda>x. T (s i x))"
by (auto intro: simple_bochner_integrable_compose2 T.zero)
@@ -625,10 +625,10 @@
obtain K where K: "K > 0" "\<And>x i. norm (T (f x) - T (s i x)) \<le> norm (f x - s i x) * K"
using T.pos_bounded by (auto simp: T.diff[symmetric])
- show "(\<lambda>i. \<integral>\<^sup>+ x. norm (T (f x) - T (s i x)) \<partial>M) ----> 0"
- (is "?f ----> 0")
+ show "(\<lambda>i. \<integral>\<^sup>+ x. norm (T (f x) - T (s i x)) \<partial>M) \<longlonglongrightarrow> 0"
+ (is "?f \<longlonglongrightarrow> 0")
proof (rule tendsto_sandwich)
- show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
+ show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) \<longlonglongrightarrow> 0"
by (auto simp: nn_integral_nonneg)
show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M)) sequentially"
@@ -640,12 +640,12 @@
using K by (intro nn_integral_cmult) auto
finally show "?f i \<le> ?g i" .
qed
- show "?g ----> 0"
+ show "?g \<longlonglongrightarrow> 0"
using tendsto_cmult_ereal[OF _ f_s, of "ereal K"] by simp
qed
- assume "(\<lambda>i. simple_bochner_integral M (s i)) ----> x"
- with s show "(\<lambda>i. simple_bochner_integral M (\<lambda>x. T (s i x))) ----> T x"
+ assume "(\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x"
+ with s show "(\<lambda>i. simple_bochner_integral M (\<lambda>x. T (s i x))) \<longlonglongrightarrow> T x"
by (auto intro!: T.tendsto simp: T.simple_bochner_integral_linear)
qed
@@ -724,7 +724,7 @@
proof (elim has_bochner_integral.cases)
fix s v
assume [measurable]: "f \<in> borel_measurable M" and s: "\<And>i. simple_bochner_integrable M (s i)" and
- lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
+ lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
from order_tendstoD[OF lim_0, of "\<infinity>"]
obtain i where f_s_fin: "(\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) < \<infinity>"
by (metis (mono_tags, lifting) eventually_False_sequentially eventually_mono
@@ -760,9 +760,9 @@
shows "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
using assms proof
fix s assume
- x: "(\<lambda>i. simple_bochner_integral M (s i)) ----> x" (is "?s ----> x") and
+ x: "(\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x" (is "?s \<longlonglongrightarrow> x") and
s[simp]: "\<And>i. simple_bochner_integrable M (s i)" and
- lim: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0" and
+ lim: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0" and
f[measurable]: "f \<in> borel_measurable M"
have [measurable]: "\<And>i. s i \<in> borel_measurable M"
@@ -770,7 +770,7 @@
show "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
proof (rule LIMSEQ_le)
- show "(\<lambda>i. ereal (norm (?s i))) ----> norm x"
+ show "(\<lambda>i. ereal (norm (?s i))) \<longlonglongrightarrow> norm x"
using x by (intro tendsto_intros lim_ereal[THEN iffD2])
show "\<exists>N. \<forall>n\<ge>N. norm (?s n) \<le> (\<integral>\<^sup>+x. norm (f x - s n x) \<partial>M) + (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
(is "\<exists>N. \<forall>n\<ge>N. _ \<le> ?t n")
@@ -788,10 +788,10 @@
by (rule nn_integral_add) auto
finally show "norm (?s n) \<le> ?t n" .
qed
- have "?t ----> 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
+ have "?t \<longlonglongrightarrow> 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
using has_bochner_integral_implies_finite_norm[OF i]
by (intro tendsto_add_ereal tendsto_const lim) auto
- then show "?t ----> \<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M"
+ then show "?t \<longlonglongrightarrow> \<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M"
by simp
qed
qed
@@ -802,8 +802,8 @@
assume f[measurable]: "f \<in> borel_measurable M"
fix s t
- assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) ----> 0" (is "?S ----> 0")
- assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - t i x) \<partial>M) ----> 0" (is "?T ----> 0")
+ assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?S \<longlonglongrightarrow> 0")
+ assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - t i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?T \<longlonglongrightarrow> 0")
assume s: "\<And>i. simple_bochner_integrable M (s i)"
assume t: "\<And>i. simple_bochner_integrable M (t i)"
@@ -812,22 +812,22 @@
let ?s = "\<lambda>i. simple_bochner_integral M (s i)"
let ?t = "\<lambda>i. simple_bochner_integral M (t i)"
- assume "?s ----> x" "?t ----> y"
- then have "(\<lambda>i. norm (?s i - ?t i)) ----> norm (x - y)"
+ assume "?s \<longlonglongrightarrow> x" "?t \<longlonglongrightarrow> y"
+ then have "(\<lambda>i. norm (?s i - ?t i)) \<longlonglongrightarrow> norm (x - y)"
by (intro tendsto_intros)
moreover
- have "(\<lambda>i. ereal (norm (?s i - ?t i))) ----> ereal 0"
+ have "(\<lambda>i. ereal (norm (?s i - ?t i))) \<longlonglongrightarrow> ereal 0"
proof (rule tendsto_sandwich)
- show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) ----> ereal 0"
+ show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) \<longlonglongrightarrow> ereal 0"
by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric])
show "eventually (\<lambda>i. norm (?s i - ?t i) \<le> ?S i + ?T i) sequentially"
by (intro always_eventually allI simple_bochner_integral_bounded s t f)
- show "(\<lambda>i. ?S i + ?T i) ----> ereal 0"
- using tendsto_add_ereal[OF _ _ \<open>?S ----> 0\<close> \<open>?T ----> 0\<close>]
+ show "(\<lambda>i. ?S i + ?T i) \<longlonglongrightarrow> ereal 0"
+ using tendsto_add_ereal[OF _ _ \<open>?S \<longlonglongrightarrow> 0\<close> \<open>?T \<longlonglongrightarrow> 0\<close>]
by (simp add: zero_ereal_def[symmetric])
qed
- then have "(\<lambda>i. norm (?s i - ?t i)) ----> 0"
+ then have "(\<lambda>i. norm (?s i - ?t i)) \<longlonglongrightarrow> 0"
by simp
ultimately have "norm (x - y) = 0"
by (rule LIMSEQ_unique)
@@ -841,11 +841,11 @@
shows "has_bochner_integral M g x"
using f
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
- fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
+ fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
also have "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) = (\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M)"
using ae
by (intro ext nn_integral_cong_AE, eventually_elim) simp
- finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M) ----> 0" .
+ finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M) \<longlonglongrightarrow> 0" .
qed (auto intro: g)
lemma has_bochner_integral_eq_AE:
@@ -1144,12 +1144,12 @@
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes f[measurable]: "f \<in> borel_measurable M"
assumes s: "\<And>i. simple_bochner_integrable M (s i)"
- assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) ----> 0" (is "?S ----> 0")
+ assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?S \<longlonglongrightarrow> 0")
shows "integrable M f"
proof -
let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
- have "\<exists>x. ?s ----> x"
+ have "\<exists>x. ?s \<longlonglongrightarrow> x"
unfolding convergent_eq_cauchy
proof (rule metric_CauchyI)
fix e :: real assume "0 < e"
@@ -1172,7 +1172,7 @@
by (simp add: dist_norm)
qed
qed
- then obtain x where "?s ----> x" ..
+ then obtain x where "?s \<longlonglongrightarrow> x" ..
show ?thesis
by (rule, rule) fact+
qed
@@ -1183,14 +1183,14 @@
"\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
and bound: "\<And>j. AE x in M. norm (u j x) \<le> w x"
and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
- and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
- shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> 0"
+ and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
+ shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) \<longlonglongrightarrow> 0"
proof -
have "AE x in M. \<forall>j. norm (u j x) \<le> w x"
unfolding AE_all_countable by rule fact
with u' have bnd: "AE x in M. \<forall>j. norm (u' x - u j x) \<le> 2 * w x"
proof (eventually_elim, intro allI)
- fix i x assume "(\<lambda>i. u i x) ----> u' x" "\<forall>j. norm (u j x) \<le> w x" "\<forall>j. norm (u j x) \<le> w x"
+ fix i x assume "(\<lambda>i. u i x) \<longlonglongrightarrow> u' x" "\<forall>j. norm (u j x) \<le> w x" "\<forall>j. norm (u j x) \<le> w x"
then have "norm (u' x) \<le> w x" "norm (u i x) \<le> w x"
by (auto intro: LIMSEQ_le_const2 tendsto_norm)
then have "norm (u' x) + norm (u i x) \<le> 2 * w x"
@@ -1200,16 +1200,16 @@
finally (xtrans) show "norm (u' x - u i x) \<le> 2 * w x" .
qed
- have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> (\<integral>\<^sup>+x. 0 \<partial>M)"
+ have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. 0 \<partial>M)"
proof (rule nn_integral_dominated_convergence)
show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto
- show "AE x in M. (\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
+ show "AE x in M. (\<lambda>i. ereal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
using u'
proof eventually_elim
- fix x assume "(\<lambda>i. u i x) ----> u' x"
+ fix x assume "(\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
from tendsto_diff[OF tendsto_const[of "u' x"] this]
- show "(\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
+ show "(\<lambda>i. ereal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
by (simp add: zero_ereal_def tendsto_norm_zero_iff)
qed
qed (insert bnd, auto)
@@ -1223,7 +1223,7 @@
proof -
from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
s: "\<And>i. simple_function M (s i)" and
- pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x" and
+ pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" and
bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
by (simp add: norm_conv_dist) metis
@@ -1241,7 +1241,7 @@
show "\<And>i. simple_bochner_integrable M (s i)"
by (rule simple_bochner_integrableI_bounded) fact+
- show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
+ show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
proof (rule nn_integral_dominated_convergence_norm)
show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
using bound by auto
@@ -1249,7 +1249,7 @@
using s by (auto intro: borel_measurable_simple_function)
show "(\<integral>\<^sup>+ x. ereal (2 * norm (f x)) \<partial>M) < \<infinity>"
using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto
- show "AE x in M. (\<lambda>i. s i x) ----> f x"
+ show "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
using pointwise by auto
qed fact
qed fact
@@ -1456,11 +1456,11 @@
lemma
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
- assumes lim: "AE x in M. (\<lambda>i. s i x) ----> f x"
+ assumes lim: "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
assumes bound: "\<And>i. AE x in M. norm (s i x) \<le> w x"
shows integrable_dominated_convergence: "integrable M f"
and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
- and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"
+ and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"
proof -
have "AE x in M. 0 \<le> w x"
using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
@@ -1487,16 +1487,16 @@
have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
using all_bound lim
proof (intro nn_integral_mono_AE, eventually_elim)
- fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) ----> f x"
+ fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) \<longlonglongrightarrow> f x"
then show "ereal (norm (f x)) \<le> ereal (w x)"
by (intro LIMSEQ_le_const2[where X="\<lambda>i. ereal (norm (s i x))"] tendsto_intros lim_ereal[THEN iffD2]) auto
qed
with w show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" by auto
qed fact
- have "(\<lambda>n. ereal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) ----> ereal 0" (is "?d ----> ereal 0")
+ have "(\<lambda>n. ereal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) \<longlonglongrightarrow> ereal 0" (is "?d \<longlonglongrightarrow> ereal 0")
proof (rule tendsto_sandwich)
- show "eventually (\<lambda>n. ereal 0 \<le> ?d n) sequentially" "(\<lambda>_. ereal 0) ----> ereal 0" by auto
+ show "eventually (\<lambda>n. ereal 0 \<le> ?d n) sequentially" "(\<lambda>_. ereal 0) \<longlonglongrightarrow> ereal 0" by auto
show "eventually (\<lambda>n. ?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)) sequentially"
proof (intro always_eventually allI)
fix n
@@ -1506,7 +1506,7 @@
by (intro int_f int_s integrable_diff integral_norm_bound_ereal)
finally show "?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)" .
qed
- show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) ----> ereal 0"
+ show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) \<longlonglongrightarrow> ereal 0"
unfolding zero_ereal_def[symmetric]
apply (subst norm_minus_commute)
proof (rule nn_integral_dominated_convergence_norm[where w=w])
@@ -1514,10 +1514,10 @@
using int_s unfolding integrable_iff_bounded by auto
qed fact+
qed
- then have "(\<lambda>n. integral\<^sup>L M (s n) - integral\<^sup>L M f) ----> 0"
+ then have "(\<lambda>n. integral\<^sup>L M (s n) - integral\<^sup>L M f) \<longlonglongrightarrow> 0"
unfolding lim_ereal tendsto_norm_zero_iff .
from tendsto_add[OF this tendsto_const[of "integral\<^sup>L M f"]]
- show "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f" by simp
+ show "(\<lambda>i. integral\<^sup>L M (s i)) \<longlonglongrightarrow> integral\<^sup>L M f" by simp
qed
context
@@ -1535,15 +1535,15 @@
obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s (X n) x) \<le> w x"
by (auto simp: eventually_sequentially)
- show "(\<lambda>n. integral\<^sup>L M (s (X n))) ----> integral\<^sup>L M f"
+ show "(\<lambda>n. integral\<^sup>L M (s (X n))) \<longlonglongrightarrow> integral\<^sup>L M f"
proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
show "AE x in M. norm (s (X (n + N)) x) \<le> w x" for n
by (rule w) auto
- show "AE x in M. (\<lambda>n. s (X (n + N)) x) ----> f x"
+ 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"
- then show "(\<lambda>n. s (X (n + N)) x) ----> f x"
+ then show "(\<lambda>n. s (X (n + N)) x) \<longlonglongrightarrow> f x"
by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
qed
qed fact+
@@ -1557,11 +1557,11 @@
proof (rule integrable_dominated_convergence)
show "AE x in M. norm (s (N + i) x) \<le> w x" for i :: nat
by (intro w) auto
- show "AE x in M. (\<lambda>i. s (N + real i) x) ----> f x"
+ 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"
- then show "(\<lambda>n. s (N + n) x) ----> f x"
+ 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)
qed
@@ -1606,7 +1606,7 @@
show ?case
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. ereal (integral\<^sup>L M (s i))) ----> ereal (integral\<^sup>L M f)"
+ show "(\<lambda>i. ereal (integral\<^sup>L M (s i))) \<longlonglongrightarrow> ereal (integral\<^sup>L M f)"
unfolding lim_ereal
proof (rule integral_dominated_convergence[where w=f])
show "integrable M f" by fact
@@ -1615,13 +1615,13 @@
qed (insert seq, auto)
have int_s: "\<And>i. integrable M (s i)"
using seq f s_le_f by (intro integrable_bound[OF f(3)]) auto
- have "(\<lambda>i. \<integral>\<^sup>+ x. s i x \<partial>M) ----> \<integral>\<^sup>+ x. f x \<partial>M"
+ have "(\<lambda>i. \<integral>\<^sup>+ x. s i x \<partial>M) \<longlonglongrightarrow> \<integral>\<^sup>+ x. f x \<partial>M"
using seq s_le_f f
by (intro nn_integral_dominated_convergence[where w=f])
(auto simp: integrable_iff_bounded)
also have "(\<lambda>i. \<integral>\<^sup>+x. s i x \<partial>M) = (\<lambda>i. \<integral>x. s i x \<partial>M)"
using seq int_s by simp
- finally show "(\<lambda>i. \<integral>x. s i x \<partial>M) ----> \<integral>\<^sup>+x. f x \<partial>M"
+ finally show "(\<lambda>i. \<integral>x. s i x \<partial>M) \<longlonglongrightarrow> \<integral>\<^sup>+x. f x \<partial>M"
by simp
qed
qed }
@@ -1660,7 +1660,7 @@
by (simp add: suminf_ereal' sums)
qed simp
- have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) ----> (\<Sum>i. f i x)"
+ have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> (\<Sum>i. f i x)"
using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
have 3: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))"
@@ -1742,14 +1742,14 @@
assumes base: "\<And>A c. A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R c)"
assumes add: "\<And>f g. integrable M f \<Longrightarrow> P f \<Longrightarrow> integrable M g \<Longrightarrow> P g \<Longrightarrow> P (\<lambda>x. f x + g x)"
assumes lim: "\<And>f s. (\<And>i. integrable M (s i)) \<Longrightarrow> (\<And>i. P (s i)) \<Longrightarrow>
- (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x) \<Longrightarrow>
+ (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x) \<Longrightarrow>
(\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)) \<Longrightarrow> integrable M f \<Longrightarrow> P f"
shows "P f"
proof -
from \<open>integrable M f\<close> have f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
unfolding integrable_iff_bounded by auto
from borel_measurable_implies_sequence_metric[OF f(1)]
- obtain s where s: "\<And>i. simple_function M (s i)" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x"
+ obtain s where s: "\<And>i. simple_function M (s i)" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
"\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
unfolding norm_conv_dist by metis
@@ -1799,7 +1799,7 @@
then show "P (s' i)"
by (subst s'_eq) (auto intro!: setsum base)
- fix x assume "x \<in> space M" with s show "(\<lambda>i. s' i x) ----> f x"
+ fix x assume "x \<in> space M" with s show "(\<lambda>i. s' i x) \<longlonglongrightarrow> f x"
by (simp add: s'_eq_s)
show "norm (s' i x) \<le> 2 * norm (f x)"
using \<open>x \<in> space M\<close> s by (simp add: s'_eq_s)
@@ -1923,10 +1923,10 @@
case (lim f s)
show ?case
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> integral\<^sup>L (restrict_space M \<Omega>) f"
+ show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) \<longlonglongrightarrow> integral\<^sup>L (restrict_space M \<Omega>) f"
using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) simp_all
- show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
+ show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) \<longlonglongrightarrow> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
unfolding lim
using lim
by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (indicator \<Omega> x *\<^sub>R f x)"])
@@ -1998,16 +1998,16 @@
show ?case
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
+ show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) \<longlonglongrightarrow> integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
proof (rule integral_dominated_convergence)
show "integrable M (\<lambda>x. 2 * norm (g x *\<^sub>R f x))"
by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
- show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) ----> g x *\<^sub>R f x"
+ show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) \<longlonglongrightarrow> g x *\<^sub>R f x"
using lim(3) by (auto intro!: tendsto_scaleR AE_I2[of M])
show "\<And>i. AE x in M. norm (g x *\<^sub>R s i x) \<le> 2 * norm (g x *\<^sub>R f x)"
using lim(4) g by (auto intro!: AE_I2[of M] mult_left_mono simp: field_simps)
qed auto
- show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f"
+ show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) \<longlonglongrightarrow> integral\<^sup>L (density M g) f"
unfolding lim(2)[symmetric]
by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
(insert lim(3-5), auto)
@@ -2077,16 +2077,16 @@
show ?case
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L M (\<lambda>x. f (g x))"
+ show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) \<longlonglongrightarrow> integral\<^sup>L M (\<lambda>x. f (g x))"
proof (rule integral_dominated_convergence)
show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
using lim by (auto simp: integrable_distr_eq)
- show "AE x in M. (\<lambda>i. s i (g x)) ----> f (g x)"
+ show "AE x in M. (\<lambda>i. s i (g x)) \<longlonglongrightarrow> f (g x)"
using lim(3) g[THEN measurable_space] by auto
show "\<And>i. AE x in M. norm (s i (g x)) \<le> 2 * norm (f (g x))"
using lim(4) g[THEN measurable_space] by auto
qed auto
- show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L (distr M N g) f"
+ show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) \<longlonglongrightarrow> integral\<^sup>L (distr M N g) f"
unfolding lim(2)[symmetric]
by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
(insert lim(3-5), auto)
@@ -2266,8 +2266,8 @@
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
assumes i: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
and pos: "\<And>i. AE x in M. 0 \<le> f i x"
- and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
- and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) ----> x"
+ and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
+ and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) \<longlonglongrightarrow> x"
and u: "u \<in> borel_measurable M"
shows "integrable M u"
and "integral\<^sup>L M u = x"
@@ -2295,7 +2295,7 @@
using u by auto
from mono pos[of 0] lim show "AE x in M. ereal (- u x) \<le> 0"
proof eventually_elim
- fix x assume "mono (\<lambda>n. f n x)" "0 \<le> f 0 x" "(\<lambda>i. f i x) ----> u x"
+ fix x assume "mono (\<lambda>n. f n x)" "0 \<le> f 0 x" "(\<lambda>i. f i x) \<longlonglongrightarrow> u x"
then show "ereal (- u x) \<le> 0"
using incseq_le[of "\<lambda>n. f n x" "u x" 0] by (simp add: mono_def incseq_def)
qed
@@ -2307,8 +2307,8 @@
lemma
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
- and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
- and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) ----> x"
+ and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
+ and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) \<longlonglongrightarrow> x"
and u: "u \<in> borel_measurable M"
shows integrable_monotone_convergence: "integrable M u"
and integral_monotone_convergence: "integral\<^sup>L M u = x"
@@ -2320,9 +2320,9 @@
using mono by (auto simp: mono_def le_fun_def)
have 3: "\<And>n. AE x in M. 0 \<le> f n x - f 0 x"
using mono by (auto simp: field_simps mono_def le_fun_def)
- have 4: "AE x in M. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
+ have 4: "AE x in M. (\<lambda>i. f i x - f 0 x) \<longlonglongrightarrow> u x - f 0 x"
using lim by (auto intro!: tendsto_diff)
- have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^sup>L M (f 0)"
+ have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) \<longlonglongrightarrow> x - integral\<^sup>L M (f 0)"
using f ilim by (auto intro!: tendsto_diff)
have 6: "(\<lambda>x. u x - f 0 x) \<in> borel_measurable M"
using f[of 0] u by auto
@@ -2462,17 +2462,17 @@
shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<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) ----> integral\<^sup>L M f"
+ show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) \<longlonglongrightarrow> integral\<^sup>L M f"
proof (rule integral_dominated_convergence)
show "integrable M (\<lambda>x. norm (f x))"
by (rule integrable_norm) fact
- show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
+ show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
proof
fix x
from \<open>filterlim X at_top sequentially\<close>
have "eventually (\<lambda>n. x \<le> X n) sequentially"
unfolding filterlim_at_top_ge[where c=x] by auto
- then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
+ then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
qed
fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
@@ -2497,9 +2497,9 @@
by (rule eventually_sequentiallyI[of "nat \<lceil>x\<rceil>"])
(auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
from filterlim_cong[OF refl refl this]
- have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
+ have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) \<longlonglongrightarrow> f x"
by simp
- have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
+ have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) \<longlonglongrightarrow> x"
using conv filterlim_real_sequentially by (rule filterlim_compose)
have M_measure[simp]: "borel_measurable M = borel_measurable borel"
using M by (simp add: sets_eq_imp_space_eq measurable_def)
@@ -2539,7 +2539,7 @@
proof -
from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
- "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) ----> f x y"
+ "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
"\<And>i x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> norm (s i (x, y)) \<le> 2 * norm (f x y)"
by (auto simp: space_pair_measure norm_conv_dist)
@@ -2569,12 +2569,12 @@
{ assume int_f: "integrable M (f x)"
have int_2f: "integrable M (\<lambda>y. 2 * norm (f x y))"
by (intro integrable_norm integrable_mult_right int_f)
- have "(\<lambda>i. integral\<^sup>L M (\<lambda>y. s i (x, y))) ----> integral\<^sup>L M (f x)"
+ have "(\<lambda>i. integral\<^sup>L M (\<lambda>y. s i (x, y))) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
proof (rule integral_dominated_convergence)
from int_f show "f x \<in> borel_measurable M" by auto
show "\<And>i. (\<lambda>y. s i (x, y)) \<in> borel_measurable M"
using x by simp
- show "AE xa in M. (\<lambda>i. s i (x, xa)) ----> f x xa"
+ show "AE xa in M. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f x xa"
using x s(2) by auto
show "\<And>i. AE xa in M. norm (s i (x, xa)) \<le> 2 * norm (f x xa)"
using x s(3) by auto
@@ -2597,10 +2597,10 @@
qed
then have "integral\<^sup>L M (\<lambda>y. s i (x, y)) = simple_bochner_integral M (\<lambda>y. s i (x, y))"
by (rule simple_bochner_integrable_eq_integral[symmetric]) }
- ultimately have "(\<lambda>i. simple_bochner_integral M (\<lambda>y. s i (x, y))) ----> integral\<^sup>L M (f x)"
+ ultimately have "(\<lambda>i. simple_bochner_integral M (\<lambda>y. s i (x, y))) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
by simp }
then
- show "(\<lambda>i. f' i x) ----> integral\<^sup>L M (f x)"
+ show "(\<lambda>i. f' i x) \<longlonglongrightarrow> integral\<^sup>L M (f x)"
unfolding f'_def
by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
qed
@@ -2779,25 +2779,25 @@
show ?case
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) ----> integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
+ show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) \<longlonglongrightarrow> integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
proof (rule integral_dominated_convergence)
show "integrable (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. 2 * norm (f x))"
using lim(5) by auto
qed (insert lim, auto)
- have "(\<lambda>i. \<integral> x. \<integral> y. s i (x, y) \<partial>M2 \<partial>M1) ----> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
+ have "(\<lambda>i. \<integral> x. \<integral> y. s i (x, y) \<partial>M2 \<partial>M1) \<longlonglongrightarrow> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
proof (rule integral_dominated_convergence)
have "AE x in M1. \<forall>i. integrable M2 (\<lambda>y. s i (x, y))"
unfolding AE_all_countable using AE_integrable_fst'[OF lim(1)] ..
with AE_space AE_integrable_fst'[OF lim(5)]
- show "AE x in M1. (\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) ----> \<integral> y. f (x, y) \<partial>M2"
+ show "AE x in M1. (\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) \<longlonglongrightarrow> \<integral> y. f (x, y) \<partial>M2"
proof eventually_elim
fix x assume x: "x \<in> space M1" and
s: "\<forall>i. integrable M2 (\<lambda>y. s i (x, y))" and f: "integrable M2 (\<lambda>y. f (x, y))"
- show "(\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) ----> \<integral> y. f (x, y) \<partial>M2"
+ show "(\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) \<longlonglongrightarrow> \<integral> y. f (x, y) \<partial>M2"
proof (rule integral_dominated_convergence)
show "integrable M2 (\<lambda>y. 2 * norm (f (x, y)))"
using f by auto
- show "AE xa in M2. (\<lambda>i. s i (x, xa)) ----> f (x, xa)"
+ show "AE xa in M2. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f (x, xa)"
using x lim(3) by (auto simp: space_pair_measure)
show "\<And>i. AE xa in M2. norm (s i (x, xa)) \<le> 2 * norm (f (x, xa))"
using x lim(4) by (auto simp: space_pair_measure)
@@ -2820,7 +2820,7 @@
by simp
qed
qed simp_all
- then show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) ----> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
+ then show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) \<longlonglongrightarrow> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
using lim by simp
qed
qed
@@ -2991,12 +2991,12 @@
using integrable_subalgebra[OF _ N, of f] integrable_subalgebra[OF _ N, of "s i" for i] by simp_all
show ?case
proof (intro LIMSEQ_unique)
- show "(\<lambda>i. integral\<^sup>L N (s i)) ----> integral\<^sup>L N f"
+ show "(\<lambda>i. integral\<^sup>L N (s i)) \<longlonglongrightarrow> integral\<^sup>L N f"
apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
using lim
apply auto
done
- show "(\<lambda>i. integral\<^sup>L N (s i)) ----> integral\<^sup>L M f"
+ show "(\<lambda>i. integral\<^sup>L N (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"
unfolding lim
apply (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
using lim M N(2)
--- a/src/HOL/Probability/Borel_Space.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Dec 29 23:04:53 2015 +0100
@@ -1300,7 +1300,7 @@
lemma borel_measurable_ereal_LIMSEQ:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
- assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
+ assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
and u: "\<And>i. u i \<in> borel_measurable M"
shows "u' \<in> borel_measurable M"
proof -
@@ -1319,7 +1319,7 @@
lemma borel_measurable_LIMSEQ:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
- assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
+ assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
and u: "\<And>i. u i \<in> borel_measurable M"
shows "u' \<in> borel_measurable M"
proof -
@@ -1333,7 +1333,7 @@
lemma borel_measurable_LIMSEQ_metric:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: metric_space"
assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
- assumes lim: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. f i x) ----> g x"
+ assumes lim: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. f i x) \<longlonglongrightarrow> g x"
shows "g \<in> borel_measurable M"
unfolding borel_eq_closed
proof (safe intro!: measurable_measure_of)
@@ -1341,7 +1341,7 @@
have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M"
proof (rule borel_measurable_LIMSEQ)
- show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) ----> infdist (g x) A"
+ show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) \<longlonglongrightarrow> infdist (g x) A"
by (intro tendsto_infdist lim)
show "\<And>i. (\<lambda>x. infdist (f i x) A) \<in> borel_measurable M"
by (intro borel_measurable_continuous_on[where f="\<lambda>x. infdist x A"]
@@ -1381,7 +1381,7 @@
have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
by (cases "Cauchy (\<lambda>i. f i x)")
(auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
- then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) ----> u' x"
+ then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) \<longlonglongrightarrow> u' x"
unfolding u'_def
by (rule convergent_LIMSEQ_iff[THEN iffD1])
qed measurable
--- a/src/HOL/Probability/Caratheodory.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Dec 29 23:04:53 2015 +0100
@@ -540,7 +540,7 @@
lemma (in ring_of_sets) caratheodory_empty_continuous:
assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>"
- assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
proof (intro caratheodory' empty_continuous_imp_countably_additive f)
show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
--- a/src/HOL/Probability/Distributions.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Distributions.thy Tue Dec 29 23:04:53 2015 +0100
@@ -116,7 +116,7 @@
shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = real_of_nat (fact k)"
proof (rule LIMSEQ_unique)
let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
- show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
+ show "?X \<longlonglongrightarrow> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
apply (intro nn_integral_LIMSEQ)
apply (auto simp: incseq_def le_fun_def eventually_sequentially
split: split_indicator intro!: Lim_eventually)
@@ -126,7 +126,7 @@
have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) --->
(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 ----> real_of_nat (fact k)"
+ then show "?X \<longlonglongrightarrow> real_of_nat (fact k)"
by (subst nn_intergal_power_times_exp_Icc)
(auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
qed
--- a/src/HOL/Probability/Fin_Map.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Tue Dec 29 23:04:53 2015 +0100
@@ -420,8 +420,8 @@
lemma tendsto_finmap:
fixes f::"nat \<Rightarrow> ('i \<Rightarrow>\<^sub>F ('a::metric_space))"
assumes ind_f: "\<And>n. domain (f n) = domain g"
- assumes proj_g: "\<And>i. i \<in> domain g \<Longrightarrow> (\<lambda>n. (f n) i) ----> g i"
- shows "f ----> g"
+ assumes proj_g: "\<And>i. i \<in> domain g \<Longrightarrow> (\<lambda>n. (f n) i) \<longlonglongrightarrow> g i"
+ shows "f \<longlonglongrightarrow> g"
unfolding tendsto_iff
proof safe
fix e::real assume "0 < e"
@@ -472,9 +472,9 @@
qed
qed
hence "convergent (p i)" by (metis Cauchy_convergent_iff)
- hence "p i ----> q i" unfolding q_def convergent_def by (metis limI)
+ hence "p i \<longlonglongrightarrow> q i" unfolding q_def convergent_def by (metis limI)
} note p = this
- have "P ----> Q"
+ have "P \<longlonglongrightarrow> Q"
proof (rule metric_LIMSEQ_I)
fix e::real assume "0 < e"
have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Dec 29 23:04:53 2015 +0100
@@ -187,7 +187,7 @@
lemma measure_PiM_countable:
fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets M"
- shows "(\<lambda>n. \<Prod>i\<le>n. measure M (E i)) ----> measure S (Pi UNIV E)"
+ shows "(\<lambda>n. \<Prod>i\<le>n. measure M (E i)) \<longlonglongrightarrow> measure S (Pi UNIV E)"
proof -
let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^sub>E {.. n} E)"
have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"
--- a/src/HOL/Probability/Interval_Integral.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy Tue Dec 29 23:04:53 2015 +0100
@@ -62,16 +62,16 @@
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat \<Rightarrow> real" where
- "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> b"
+ "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
proof (cases b)
case PInf
with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
by (cases a) auto
- moreover have "(\<lambda>x. ereal (real (Suc x))) ----> \<infinity>"
+ moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>"
apply (subst LIMSEQ_Suc_iff)
apply (simp add: Lim_PInfty)
using nat_ceiling_le_eq by blast
- moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) ----> \<infinity>"
+ moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) \<longlonglongrightarrow> \<infinity>"
apply (subst LIMSEQ_Suc_iff)
apply (subst Lim_PInfty)
apply (metis add.commute diff_le_eq nat_ceiling_le_eq ereal_less_eq(3))
@@ -89,7 +89,7 @@
by (intro mult_strict_left_mono) auto
with \<open>a < b\<close> a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))"
by (cases a) (auto simp: real d_def field_simps)
- moreover have "(\<lambda>i. b' - d / Suc (Suc i)) ----> b'"
+ moreover have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
apply (subst filterlim_sequentially_Suc)
apply (subst filterlim_sequentially_Suc)
apply (rule tendsto_eq_intros)
@@ -105,7 +105,7 @@
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat \<Rightarrow> real" where
- "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> a"
+ "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
proof -
have "-b < -a" using \<open>a < b\<close> by simp
from ereal_incseq_approx[OF this] guess X .
@@ -123,7 +123,7 @@
obtains u l :: "nat \<Rightarrow> real" where
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
- "l ----> a" "u ----> b"
+ "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
proof -
from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
@@ -494,12 +494,12 @@
fixes u l :: "nat \<Rightarrow> real"
assumes approx: "einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
- "l ----> a" "u ----> b"
+ "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
fixes f :: "real \<Rightarrow> real"
assumes f_integrable: "\<And>i. set_integrable lborel {l i..u i} f"
assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
- assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) ----> C"
+ assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> C"
shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = C"
@@ -517,7 +517,7 @@
apply (metis approx(2) incseqD order_trans)
done
qed
- have 3: "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) ----> indicator (einterval a b) x *\<^sub>R f x"
+ have 3: "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
proof -
{ fix x i assume "l i \<le> x" "x \<le> u i"
then have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
@@ -530,7 +530,7 @@
then show ?thesis
unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
qed
- have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) ----> C"
+ have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) \<longlonglongrightarrow> C"
using lbint_lim by (simp add: interval_integral_Icc approx less_imp_le)
have 5: "set_borel_measurable lborel (einterval a b) f" by (rule assms)
have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
@@ -548,11 +548,11 @@
assumes "a < b"
assumes approx: "einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
- "l ----> a" "u ----> b"
+ "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
assumes f_integrable: "set_integrable lborel (einterval a b) f"
- shows "(\<lambda>i. LBINT x=l i.. u i. f x) ----> (LBINT x=a..b. f x)"
+ shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
proof -
- have "(\<lambda>i. LBINT x:{l i.. u i}. f x) ----> (LBINT x:einterval a b. f x)"
+ have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
proof (rule integral_dominated_convergence)
show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))"
by (rule integrable_norm) fact
@@ -562,7 +562,7 @@
by (rule set_borel_measurable_subset) (auto simp: approx)
show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)"
by (intro AE_I2) (auto simp: approx split: split_indicator)
- show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) ----> indicator (einterval a b) x *\<^sub>R f x"
+ show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
proof (intro AE_I2 tendsto_intros Lim_eventually)
fix x
{ fix i assume "l i \<le> x" "x \<le> u i"
@@ -570,7 +570,7 @@
have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) }
then show "eventually (\<lambda>xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially"
- using approx order_tendstoD(2)[OF \<open>l ----> a\<close>, of x] order_tendstoD(1)[OF \<open>u ----> b\<close>, of x]
+ using approx order_tendstoD(2)[OF \<open>l \<longlonglongrightarrow> a\<close>, of x] order_tendstoD(1)[OF \<open>u \<longlonglongrightarrow> b\<close>, of x]
by (auto split: split_indicator)
qed
qed
@@ -649,7 +649,7 @@
have 2: "set_borel_measurable lborel (einterval a b) f"
by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous
simp: continuous_on_eq_continuous_at einterval_iff f)
- have 3: "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A"
+ have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
apply (subst FTCi)
apply (intro tendsto_intros)
using B approx unfolding tendsto_at_iff_sequentially comp_def
@@ -683,14 +683,14 @@
by (auto simp add: less_imp_le min_def max_def
intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
intro: has_vector_derivative_at_within)
- have "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A"
+ have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
apply (subst FTCi)
apply (intro tendsto_intros)
using B approx unfolding tendsto_at_iff_sequentially comp_def
apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
using A approx unfolding tendsto_at_iff_sequentially comp_def
by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
- moreover have "(\<lambda>i. LBINT x=l i..u i. f x) ----> (LBINT x=a..b. f x)"
+ moreover have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
by (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx f_integrable])
ultimately show ?thesis
by (elim LIMSEQ_unique)
@@ -863,12 +863,12 @@
by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
proof -
- have A2: "(\<lambda>i. g (l i)) ----> A"
+ have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
by (intro decseq_le, auto simp add: decseq_def)
- have B2: "(\<lambda>i. g (u i)) ----> B"
+ have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
hence B3: "\<And>i. g (u i) \<le> B"
@@ -903,17 +903,17 @@
apply (auto intro!: continuous_at_imp_continuous_on contf contg')
done
} note eq1 = this
- have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) ----> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
+ have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
by (rule assms)
- hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
+ hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
by (simp add: eq1)
have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
apply (auto simp add: incseq_def)
apply (rule order_le_less_trans)
prefer 2 apply (assumption, auto)
by (erule order_less_le_trans, rule g_nondec, auto)
- have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x = A..B. f x)"
+ have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x = A..B. f x)"
apply (subst interval_lebesgue_integral_le_eq, auto simp del: real_scaleR_def)
apply (subst interval_lebesgue_integral_le_eq, rule \<open>A \<le> B\<close>)
apply (subst un, rule set_integral_cont_up, auto simp del: real_scaleR_def)
@@ -965,12 +965,12 @@
by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
proof -
- have A2: "(\<lambda>i. g (l i)) ----> A"
+ have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
by (intro decseq_le, auto simp add: decseq_def)
- have B2: "(\<lambda>i. g (u i)) ----> B"
+ have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
hence B3: "\<And>i. g (u i) \<le> B"
@@ -1006,10 +1006,10 @@
by (simp add: ac_simps)
} note eq1 = this
have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x)
- ----> (LBINT x=a..b. f (g x) * g' x)"
+ \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
by (rule assms)
- hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. f (g x) * g' x)"
+ hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
by (simp add: eq1)
have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
apply (auto simp add: incseq_def)
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Dec 29 23:04:53 2015 +0100
@@ -325,8 +325,8 @@
show "((\<lambda>a. F b - F a) ---> emeasure ?F {a..b}) (at_left a)"
proof (rule tendsto_at_left_sequentially)
show "a - 1 < a" by simp
- fix X assume "\<And>n. X n < a" "incseq X" "X ----> a"
- with \<open>a \<le> b\<close> have "(\<lambda>n. emeasure ?F {X n<..b}) ----> emeasure ?F (\<Inter>n. {X n <..b})"
+ fix X assume "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a"
+ with \<open>a \<le> b\<close> have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})"
apply (intro Lim_emeasure_decseq)
apply (auto simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
apply force
@@ -336,13 +336,13 @@
also have "(\<Inter>n. {X n <..b}) = {a..b}"
using \<open>\<And>n. X n < a\<close>
apply auto
- apply (rule LIMSEQ_le_const2[OF \<open>X ----> a\<close>])
+ apply (rule LIMSEQ_le_const2[OF \<open>X \<longlonglongrightarrow> a\<close>])
apply (auto intro: less_imp_le)
apply (auto intro: less_le_trans)
done
also have "(\<lambda>n. emeasure ?F {X n<..b}) = (\<lambda>n. F b - F (X n))"
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)) ----> emeasure ?F {a..b}" .
+ 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)"
using cont_F
@@ -808,7 +808,7 @@
by (intro setsum_mono2) auto
from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
by (auto simp add: disjoint_family_on_def)
- show "\<And>x. (\<lambda>k. ?f k x) ----> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
+ show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
apply (auto simp: * setsum.If_cases Iio_Int_singleton)
apply (rule_tac k="Suc xa" in LIMSEQ_offset)
apply (simp add: tendsto_const)
@@ -816,7 +816,7 @@
have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
by (intro emeasure_mono) auto
- with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) ----> ?M (\<Union>i. F i)"
+ with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
unfolding sums_def[symmetric] UN_extend_simps
by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq)
qed
@@ -836,12 +836,12 @@
show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
by (auto simp: box_def)
{ fix x assume "x \<in> A"
- moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) ----> indicator (\<Union>k::nat. A \<inter> ?B k) x"
+ moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
- ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) ----> 1"
+ ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
by (simp add: indicator_def UN_box_eq_UNIV) }
- have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) ----> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
+ have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
proof (intro ext emeasure_eq_ereal_measure)
@@ -850,7 +850,7 @@
then show "emeasure lborel (A \<inter> ?B n) \<noteq> \<infinity>"
by auto
qed
- finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) ----> measure lborel A"
+ finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A"
using emeasure_eq_ereal_measure[of lborel A] finite
by (simp add: UN_box_eq_UNIV)
qed
@@ -912,16 +912,16 @@
have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)
- have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) ----> integral UNIV f"
+ have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
proof (rule monotone_convergence_increasing)
show "\<forall>k. U k integrable_on UNIV" using U_int by auto
show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
then show "bounded {integral UNIV (U k) |k. True}"
using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
- show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) ----> f x"
+ show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
using seq by auto
qed
- moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) ----> (\<integral>\<^sup>+x. f x \<partial>lborel)"
+ moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
using seq U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
ultimately have "integral UNIV f = r"
by (auto simp add: int_eq p seq intro: LIMSEQ_unique)
@@ -1073,9 +1073,9 @@
simp del: times_ereal.simps)
show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
using lim by (auto simp add: abs_mult)
- show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) ----> f x"
+ show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
using lim by auto
- show "(\<lambda>k. integral\<^sup>L lborel (s k)) ----> integral\<^sup>L lborel f"
+ show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
using lim lim(1)[THEN borel_measurable_integrable]
by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
qed
@@ -1258,7 +1258,7 @@
from reals_Archimedean2[of "x - a"] guess n ..
then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
- then show "(\<lambda>n. ?f n x) ----> ?fR x"
+ then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
by (rule Lim_eventually)
qed
then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
@@ -1281,12 +1281,12 @@
by (intro DERIV_nonneg_imp_nondecreasing[where f=F])
(simp, metis add_increasing2 order_refl order_trans of_nat_0_le_iff)
qed
- have "(\<lambda>x. F (a + real x)) ----> T"
+ have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
apply (rule filterlim_real_sequentially)
done
- then show "(\<lambda>n. ereal (F (a + real n) - F a)) ----> ereal (T - F a)"
+ then show "(\<lambda>n. ereal (F (a + real n) - F a)) \<longlonglongrightarrow> ereal (T - F a)"
unfolding lim_ereal
by (intro tendsto_diff) auto
qed
--- a/src/HOL/Probability/Measure_Space.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Tue Dec 29 23:04:53 2015 +0100
@@ -63,7 +63,7 @@
lemma LIMSEQ_binaryset:
assumes f: "f {} = 0"
- shows "(\<lambda>n. \<Sum>i<n. f (binaryset A B i)) ----> f A + f B"
+ shows "(\<lambda>n. \<Sum>i<n. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
proof -
have "(\<lambda>n. \<Sum>i < Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
proof
@@ -72,11 +72,11 @@
by (induct n) (auto simp add: binaryset_def f)
qed
moreover
- have "... ----> f A + f B" by (rule tendsto_const)
+ have "... \<longlonglongrightarrow> f A + f B" by (rule tendsto_const)
ultimately
- have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
+ have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
by metis
- hence "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) ----> f A + f B"
+ hence "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
by simp
thus ?thesis by (rule LIMSEQ_offset [where k=2])
qed
@@ -281,7 +281,7 @@
lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
assumes f: "positive M f" "additive M f"
shows "countably_additive M f \<longleftrightarrow>
- (\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i))"
+ (\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i))"
unfolding countably_additive_def
proof safe
assume count_sum: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)"
@@ -290,20 +290,20 @@
with count_sum[THEN spec, of "disjointed A"] A(3)
have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
- moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
+ moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
using f(1)[unfolded positive_def] dA
by (auto intro!: summable_LIMSEQ summable_ereal_pos)
from LIMSEQ_Suc[OF this]
- have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
+ have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
unfolding lessThan_Suc_atMost .
moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
using disjointed_additive[OF f A(1,2)] .
- ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
+ ultimately show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)" by simp
next
- assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+ assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
- have "(\<lambda>n. f (\<Union>i<n. A i)) ----> f (\<Union>i. A i)"
+ have "(\<lambda>n. f (\<Union>i<n. A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
proof (unfold *[symmetric], intro cont[rule_format])
show "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
using A * by auto
@@ -321,15 +321,15 @@
lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
assumes f: "positive M f" "additive M f"
- shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))
- \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0)"
+ shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))
+ \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0)"
proof safe
- assume cont: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))"
+ assume cont: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))"
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
- with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
+ with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
using \<open>positive M f\<close>[unfolded positive_def] by auto
next
- assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
@@ -350,7 +350,7 @@
then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
using A by auto }
note f_fin = this
- have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
+ have "(\<lambda>i. f (A i - (\<Inter>i. A i))) \<longlonglongrightarrow> 0"
proof (intro cont[rule_format, OF _ decseq _ f_fin])
show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
using A by auto
@@ -372,14 +372,14 @@
ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
by simp
with LIMSEQ_INF[OF decseq_fA]
- show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
+ show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i)" by simp
qed
lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
assumes f: "positive M f" "additive M f" "\<forall>A\<in>M. f A \<noteq> \<infinity>"
- assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
assumes A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
- shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+ shows "(\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
proof -
have "\<forall>A\<in>M. \<exists>x. f A = ereal x"
proof
@@ -387,7 +387,7 @@
unfolding positive_def by (cases "f A") auto
qed
from bchoice[OF this] guess f' .. note f' = this[rule_format]
- from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
+ from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) \<longlonglongrightarrow> 0"
by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
moreover
{ fix i
@@ -399,17 +399,17 @@
using A by (subst (asm) (1 2 3) f') auto
then have "f ((\<Union>i. A i) - A i) = ereal (f' (\<Union>i. A i) - f' (A i))"
using A f' by auto }
- ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
+ ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) \<longlonglongrightarrow> 0"
by (simp add: zero_ereal_def)
- then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
+ then have "(\<lambda>i. f' (A i)) \<longlonglongrightarrow> f' (\<Union>i. A i)"
by (rule Lim_transform2[OF tendsto_const])
- then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+ then show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
using A by (subst (1 2) f') auto
qed
lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>M. f A \<noteq> \<infinity>"
- assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
shows "countably_additive M f"
using countably_additive_iff_continuous_from_below[OF f]
using empty_continuous_imp_continuous_from_below[OF f fin] cont
@@ -503,7 +503,7 @@
qed
lemma Lim_emeasure_incseq:
- "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
+ "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) \<longlonglongrightarrow> emeasure M (\<Union>i. A i)"
using emeasure_countably_additive
by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
emeasure_additive)
@@ -604,7 +604,7 @@
lemma Lim_emeasure_decseq:
assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
- shows "(\<lambda>i. emeasure M (A i)) ----> emeasure M (\<Inter>i. A i)"
+ shows "(\<lambda>i. emeasure M (A i)) \<longlonglongrightarrow> emeasure M (\<Inter>i. A i)"
using LIMSEQ_INF[OF decseq_emeasure, OF A]
using INF_emeasure_decseq[OF A fin] by simp
@@ -1525,7 +1525,7 @@
lemma Lim_measure_incseq:
assumes A: "range A \<subseteq> sets M" "incseq A" and fin: "emeasure M (\<Union>i. A i) \<noteq> \<infinity>"
- shows "(\<lambda>i. (measure M (A i))) ----> (measure M (\<Union>i. A i))"
+ shows "(\<lambda>i. (measure M (A i))) \<longlonglongrightarrow> (measure M (\<Union>i. A i))"
proof -
have "ereal ((measure M (\<Union>i. A i))) = emeasure M (\<Union>i. A i)"
using fin by (auto simp: emeasure_eq_ereal_measure)
@@ -1537,7 +1537,7 @@
lemma Lim_measure_decseq:
assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
- shows "(\<lambda>n. measure M (A n)) ----> measure M (\<Inter>i. A i)"
+ shows "(\<lambda>n. measure M (A n)) \<longlonglongrightarrow> measure M (\<Inter>i. A i)"
proof -
have "emeasure M (\<Inter>i. A i) \<le> emeasure M (A 0)"
using A by (auto intro!: emeasure_mono)
@@ -1624,12 +1624,12 @@
lemma (in finite_measure) finite_Lim_measure_incseq:
assumes A: "range A \<subseteq> sets M" "incseq A"
- shows "(\<lambda>i. measure M (A i)) ----> measure M (\<Union>i. A i)"
+ shows "(\<lambda>i. measure M (A i)) \<longlonglongrightarrow> measure M (\<Union>i. A i)"
using Lim_measure_incseq[OF A] by simp
lemma (in finite_measure) finite_Lim_measure_decseq:
assumes A: "range A \<subseteq> sets M" "decseq A"
- shows "(\<lambda>n. measure M (A n)) ----> measure M (\<Inter>i. A i)"
+ shows "(\<lambda>n. measure M (A n)) \<longlonglongrightarrow> measure M (\<Inter>i. A i)"
using Lim_measure_decseq[OF A] by simp
lemma (in finite_measure) finite_measure_compl:
@@ -1805,7 +1805,7 @@
unfolding countably_additive_iff_continuous_from_below[OF positive additive]
proof safe
fix F :: "nat \<Rightarrow> 'a set" assume "incseq F"
- show "(\<lambda>i. ?M (F i)) ----> ?M (\<Union>i. F i)"
+ show "(\<lambda>i. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
proof cases
assume "\<exists>i. \<forall>j\<ge>i. F i = F j"
then guess i .. note i = this
@@ -1823,7 +1823,7 @@
have "incseq (\<lambda>i. ?M (F i))"
using \<open>incseq F\<close> unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
- then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
+ then have "(\<lambda>i. ?M (F i)) \<longlonglongrightarrow> (SUP n. ?M (F n))"
by (rule LIMSEQ_SUP)
moreover have "(SUP n. ?M (F n)) = \<infinity>"
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Dec 29 23:04:53 2015 +0100
@@ -1450,10 +1450,10 @@
lemma nn_integral_LIMSEQ:
assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>n x. 0 \<le> f n x"
- and u: "\<And>x. (\<lambda>i. f i x) ----> u x"
- shows "(\<lambda>n. integral\<^sup>N M (f n)) ----> integral\<^sup>N M u"
+ and u: "\<And>x. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
+ shows "(\<lambda>n. integral\<^sup>N M (f n)) \<longlonglongrightarrow> integral\<^sup>N M u"
proof -
- have "(\<lambda>n. integral\<^sup>N M (f n)) ----> (SUP n. integral\<^sup>N M (f n))"
+ have "(\<lambda>n. integral\<^sup>N M (f n)) \<longlonglongrightarrow> (SUP n. integral\<^sup>N M (f n))"
using f by (intro LIMSEQ_SUP[of "\<lambda>n. integral\<^sup>N M (f n)"] incseq_nn_integral)
also have "(SUP n. integral\<^sup>N M (f n)) = integral\<^sup>N M (\<lambda>x. SUP n. f n x)"
using f by (intro nn_integral_monotone_convergence_SUP[symmetric])
@@ -1467,8 +1467,8 @@
"\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
and bound: "\<And>j. AE x in M. 0 \<le> u j x" "\<And>j. AE x in M. u j x \<le> w x"
and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
- and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
- shows "(\<lambda>i. (\<integral>\<^sup>+x. u i x \<partial>M)) ----> (\<integral>\<^sup>+x. u' x \<partial>M)"
+ and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
+ shows "(\<lambda>i. (\<integral>\<^sup>+x. u i x \<partial>M)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. u' x \<partial>M)"
proof -
have "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
by (intro nn_integral_limsup[OF _ _ bound w]) auto
@@ -1489,9 +1489,9 @@
assumes "(\<integral>\<^sup>+ x. f 0 x \<partial>M) < \<infinity>" and nn: "\<And>x i. 0 \<le> f i x"
shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))"
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral\<^sup>N M (f i)) ----> (INF i. integral\<^sup>N M (f i))"
+ show "(\<lambda>i. integral\<^sup>N M (f i)) \<longlonglongrightarrow> (INF i. integral\<^sup>N M (f i))"
using f by (intro LIMSEQ_INF) (auto intro!: nn_integral_mono simp: decseq_def le_fun_def)
- show "(\<lambda>i. integral\<^sup>N M (f i)) ----> \<integral>\<^sup>+ x. (INF i. f i x) \<partial>M"
+ show "(\<lambda>i. integral\<^sup>N M (f i)) \<longlonglongrightarrow> \<integral>\<^sup>+ x. (INF i. f i x) \<partial>M"
proof (rule nn_integral_dominated_convergence)
show "(\<integral>\<^sup>+ x. f 0 x \<partial>M) < \<infinity>" "\<And>i. f i \<in> borel_measurable M" "f 0 \<in> borel_measurable M"
by fact+
@@ -1499,7 +1499,7 @@
using nn by auto
show "\<And>j. AE x in M. f j x \<le> f 0 x"
using f by (auto simp: decseq_def le_fun_def)
- show "AE x in M. (\<lambda>i. f i x) ----> (INF i. f i x)"
+ show "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> (INF i. f i x)"
using f by (auto intro!: LIMSEQ_INF simp: decseq_def le_fun_def)
show "(\<lambda>x. INF i. f i x) \<in> borel_measurable M"
by auto
--- a/src/HOL/Probability/Projective_Family.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Tue Dec 29 23:04:53 2015 +0100
@@ -207,7 +207,7 @@
with \<open>(\<Inter>i. A i) = {}\<close> * show False
by (subst (asm) prod_emb_trans) (auto simp: A[abs_def])
qed
- moreover have "(\<lambda>i. P (J i) (X i)) ----> (INF i. P (J i) (X i))"
+ moreover have "(\<lambda>i. P (J i) (X i)) \<longlonglongrightarrow> (INF i. P (J i) (X i))"
proof (intro LIMSEQ_INF antimonoI)
fix x y :: nat assume "x \<le> y"
have "P (J y \<union> J x) (emb (J y \<union> J x) (J y) (X y)) \<le> P (J y \<union> J x) (emb (J y \<union> J x) (J x) (X x))"
@@ -217,7 +217,7 @@
then show "P (J y) (X y) \<le> P (J x) (X x)"
using * by (simp add: emeasure_P)
qed
- ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
+ ultimately show "(\<lambda>i. \<mu>G (A i)) \<longlonglongrightarrow> 0"
by (auto simp: A[abs_def] mu_G_spec *)
qed
then obtain \<mu> where eq: "\<forall>s\<in>generator. \<mu> s = \<mu>G s"
--- a/src/HOL/Probability/Projective_Limit.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Tue Dec 29 23:04:53 2015 +0100
@@ -53,12 +53,12 @@
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
from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this] guess l r .
- hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) ----> l"
+ hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
using subseq_o[OF \<open>subseq (op + m)\<close> \<open>subseq r\<close>] by (auto simp: o_def)
- thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) ----> l" by blast
+ thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
qed
-sublocale finmap_seqs_into_compact \<subseteq> subseqs "\<lambda>n s. (\<exists>l. (\<lambda>i. ((f o s) i)\<^sub>F n) ----> l)"
+sublocale finmap_seqs_into_compact \<subseteq> subseqs "\<lambda>n s. (\<exists>l. (\<lambda>i. ((f o s) i)\<^sub>F n) \<longlonglongrightarrow> l)"
proof
fix n s
assume "subseq s"
@@ -72,24 +72,24 @@
by auto
qed
from compactE'[OF compact_projset this] guess ls rs .
- thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) ----> l)" by (auto simp: o_def)
+ thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def)
qed
-lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^sub>F n) ----> l"
+lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^sub>F n) \<longlonglongrightarrow> l"
proof -
- obtain l where "(\<lambda>i. ((f o (diagseq o op + (Suc n))) i)\<^sub>F n) ----> l"
+ obtain l where "(\<lambda>i. ((f o (diagseq o op + (Suc n))) i)\<^sub>F n) \<longlonglongrightarrow> l"
proof (atomize_elim, rule diagseq_holds)
fix r s n
assume "subseq r"
- assume "\<exists>l. (\<lambda>i. ((f \<circ> s) i)\<^sub>F n) ----> l"
- then obtain l where "((\<lambda>i. (f i)\<^sub>F n) o s) ----> l"
+ assume "\<exists>l. (\<lambda>i. ((f \<circ> s) i)\<^sub>F n) \<longlonglongrightarrow> l"
+ then obtain l where "((\<lambda>i. (f i)\<^sub>F n) o s) \<longlonglongrightarrow> l"
by (auto simp: o_def)
- hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) ----> l" using \<open>subseq r\<close>
+ hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>subseq r\<close>
by (rule LIMSEQ_subseq_LIMSEQ)
- thus "\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r)) i)\<^sub>F n) ----> l" by (auto simp add: o_def)
+ thus "\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r)) i)\<^sub>F n) \<longlonglongrightarrow> l" by (auto simp add: o_def)
qed
- hence "(\<lambda>i. ((f (diagseq (i + Suc n))))\<^sub>F n) ----> l" by (simp add: ac_simps)
- hence "(\<lambda>i. (f (diagseq i))\<^sub>F n) ----> l" by (rule LIMSEQ_offset)
+ hence "(\<lambda>i. ((f (diagseq (i + Suc n))))\<^sub>F n) \<longlonglongrightarrow> l" by (simp add: ac_simps)
+ hence "(\<lambda>i. (f (diagseq i))\<^sub>F n) \<longlonglongrightarrow> l" by (rule LIMSEQ_offset)
thus ?thesis ..
qed
@@ -362,10 +362,10 @@
using \<open>j \<in> J (Suc n)\<close> \<open>j \<in> J (Suc m)\<close>
unfolding j by (subst proj_fm, auto)+
qed
- have "\<forall>t. \<exists>z. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z"
+ have "\<forall>t. \<exists>z. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> z"
using diagonal_tendsto ..
then obtain z where z:
- "\<And>t. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z t"
+ "\<And>t. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> z t"
unfolding choice_iff by blast
{
fix n :: nat assume "n \<ge> 1"
@@ -377,7 +377,7 @@
assume t: "t \<in> domain (finmap_of (Utn ` J n) z)"
hence "t \<in> Utn ` J n" by simp
then obtain j where j: "t = Utn j" "j \<in> J n" by auto
- have "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> z t"
+ have "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> z t"
apply (subst (2) tendsto_iff, subst eventually_sequentially)
proof safe
fix e :: real assume "0 < e"
@@ -407,12 +407,12 @@
finally show "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e" .
qed
qed
- hence "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> (finmap_of (Utn ` J n) z)\<^sub>F t"
+ hence "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> (finmap_of (Utn ` J n) z)\<^sub>F t"
by (simp add: tendsto_intros)
} ultimately
- have "(\<lambda>i. fm n (y (Suc (diagseq i)))) ----> finmap_of (Utn ` J n) z"
+ have "(\<lambda>i. fm n (y (Suc (diagseq i)))) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
by (rule tendsto_finmap)
- hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) ----> finmap_of (Utn ` J n) z"
+ hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
by (intro lim_subseq) (simp add: subseq_def)
moreover
have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Dec 29 23:04:53 2015 +0100
@@ -216,7 +216,7 @@
have A: "incseq A" by (auto intro!: incseq_SucI)
from finite_Lim_measure_incseq[OF _ A] \<open>range A \<subseteq> sets M\<close>
M'.finite_Lim_measure_incseq[OF _ A]
- have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
+ have convergent: "(\<lambda>i. ?d (A i)) \<longlonglongrightarrow> ?d (\<Union>i. A i)"
by (auto intro!: tendsto_diff simp: sets_eq)
obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
@@ -261,7 +261,7 @@
show "(\<Inter>i. A i) \<in> sets M" using \<open>\<And>n. A n \<in> sets M\<close> by auto
have "decseq A" using A by (auto intro!: decseq_SucI)
from A(1) finite_Lim_measure_decseq[OF _ this] N.finite_Lim_measure_decseq[OF _ this]
- have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: tendsto_diff simp: sets_eq)
+ have "(\<lambda>i. ?d (A i)) \<longlonglongrightarrow> ?d (\<Inter>i. A i)" by (auto intro!: tendsto_diff simp: sets_eq)
thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
by (rule_tac LIMSEQ_le_const) auto
next
--- a/src/HOL/Probability/Regularity.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Regularity.thy Tue Dec 29 23:04:53 2015 +0100
@@ -131,7 +131,7 @@
have x: "space M = (\<Union>x\<in>X. cball x r)"
by (auto simp add: sU) (metis dist_commute order_less_imp_le)
let ?U = "\<Union>k. (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)"
- have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M ?U"
+ have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M ?U"
by (rule Lim_emeasure_incseq)
(auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
also have "?U = space M"
@@ -140,13 +140,13 @@
show "x \<in> ?U"
using X(1) d by (auto intro!: exI[where x="to_nat_on X d"] simp: dist_commute Bex_def)
qed (simp add: sU)
- finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M (space M)" .
+ finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M (space M)" .
} note M_space = this
{
fix e ::real and n :: nat assume "e > 0" "n > 0"
hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
from M_space[OF \<open>1/n>0\<close>]
- have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
+ have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) \<longlonglongrightarrow> measure M (space M)"
unfolding emeasure_eq_measure by simp
from metric_LIMSEQ_D[OF this \<open>0 < e * 2 powr -n\<close>]
obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <
@@ -351,9 +351,9 @@
case (union D)
then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed)
with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure)
- also have "(\<lambda>n. \<Sum>i<n. M (D i)) ----> (\<Sum>i. M (D i))"
+ also have "(\<lambda>n. \<Sum>i<n. M (D i)) \<longlonglongrightarrow> (\<Sum>i. M (D i))"
by (intro summable_LIMSEQ summable_ereal_pos emeasure_nonneg)
- finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
+ finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i<n. measure M (D i)) \<longlonglongrightarrow> measure M (\<Union>i. D i)"
by (simp add: emeasure_eq_measure)
have "(\<Union>i. D i) \<in> sets M" using \<open>range D \<subseteq> sets M\<close> by auto
--- a/src/HOL/Probability/Set_Integral.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Probability/Set_Integral.thy Tue Dec 29 23:04:53 2015 +0100
@@ -327,7 +327,7 @@
assumes "\<And>i. A i \<in> sets M" "mono A"
assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
and intgbl: "\<And>i::nat. set_integrable M (A i) f"
- and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) ----> l"
+ and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
shows "set_integrable M (\<Union>i. A i) f"
apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
apply (rule intgbl)
@@ -336,7 +336,7 @@
using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
proof (rule AE_I2)
{ fix x assume "x \<in> space M"
- show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
+ show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
proof cases
assume "\<exists>i. x \<in> A i"
then guess i ..
@@ -409,7 +409,7 @@
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
and intgbl: "set_integrable M (\<Union>i. A i) f"
- shows "(\<lambda>i. LINT x:(A i)|M. f x) ----> LINT x:(\<Union>i. A i)|M. f x"
+ shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
have int_A: "\<And>i. set_integrable M (A i) f"
using intgbl by (rule set_integrable_subset) auto
@@ -418,10 +418,10 @@
using intgbl integrable_norm[OF intgbl] by auto
{ fix x i assume "x \<in> A i"
- with A have "(\<lambda>xa. indicator (A xa) x::real) ----> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) ----> 1"
+ with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
by (intro filterlim_cong refl)
(fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
- then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
+ then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
qed (auto split: split_indicator)
@@ -430,7 +430,7 @@
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
and int0: "set_integrable M (A 0) f"
- shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) ----> LINT x:(\<Inter>i. A i)|M. f x"
+ shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
proof (rule integral_dominated_convergence)
have int_A: "\<And>i. set_integrable M (A i) f"
using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
@@ -443,10 +443,10 @@
show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
using A by (auto split: split_indicator simp: decseq_def)
{ fix x i assume "x \<in> space M" "x \<notin> A i"
- with A have "(\<lambda>i. indicator (A i) x::real) ----> 0 \<longleftrightarrow> (\<lambda>i. 0::real) ----> 0"
+ with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0"
by (intro filterlim_cong refl)
(auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
- then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Inter>i. A i) x *\<^sub>R f x"
+ then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x *\<^sub>R f x"
by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
qed
--- a/src/HOL/Real_Vector_Spaces.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Dec 29 23:04:53 2015 +0100
@@ -1708,20 +1708,20 @@
subsubsection \<open>Limits of Sequences\<close>
-lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
+lemma lim_sequentially: "X \<longlonglongrightarrow> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
unfolding tendsto_iff eventually_sequentially ..
lemmas LIMSEQ_def = lim_sequentially (*legacy binding*)
-lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
+lemma LIMSEQ_iff_nz: "X \<longlonglongrightarrow> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)
lemma metric_LIMSEQ_I:
- "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)"
+ "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X \<longlonglongrightarrow> (L::'a::metric_space)"
by (simp add: lim_sequentially)
lemma metric_LIMSEQ_D:
- "\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
+ "\<lbrakk>X \<longlonglongrightarrow> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
by (simp add: lim_sequentially)
@@ -1840,7 +1840,7 @@
done
theorem LIMSEQ_imp_Cauchy:
- assumes X: "X ----> a" shows "Cauchy X"
+ assumes X: "X \<longlonglongrightarrow> a" shows "Cauchy X"
proof (rule metric_CauchyI)
fix e::real assume "0 < e"
hence "0 < e/2" by simp
@@ -1890,7 +1890,7 @@
assumes inc: "\<And>n. f n \<le> f (Suc n)"
and bdd: "\<And>n. f n \<le> l"
and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
- shows "f ----> l"
+ shows "f \<longlonglongrightarrow> l"
proof (rule increasing_tendsto)
fix x assume "x < l"
with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
@@ -1937,7 +1937,7 @@
thus "\<And>s. s \<in> S \<Longrightarrow> s \<le> X N + 1"
by (rule bound_isUb)
qed
- have "X ----> Sup S"
+ have "X \<longlonglongrightarrow> Sup S"
proof (rule metric_LIMSEQ_I)
fix r::real assume "0 < r"
hence r: "0 < r/2" by simp
@@ -1976,7 +1976,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)) ----> y"
+ assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) \<longlonglongrightarrow> y"
shows "(f ---> y) at_top"
proof -
from nhds_countable[of y] guess A . note A = this
@@ -2008,7 +2008,7 @@
lemma tendsto_at_topI_sequentially_real:
fixes f :: "real \<Rightarrow> real"
assumes mono: "mono f"
- assumes limseq: "(\<lambda>n. f (real n)) ----> y"
+ assumes limseq: "(\<lambda>n. f (real n)) \<longlonglongrightarrow> y"
shows "(f ---> y) at_top"
proof (rule tendstoI)
fix e :: real assume "0 < e"
--- a/src/HOL/Series.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Series.thy Tue Dec 29 23:04:53 2015 +0100
@@ -19,7 +19,7 @@
sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
(infixr "sums" 80)
where
- "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) ----> s"
+ "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s"
definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool" where
"summable f \<longleftrightarrow> (\<exists>s. f sums s)"
@@ -152,7 +152,7 @@
by (simp add: summable_def sums_def suminf_def)
(metis convergent_LIMSEQ_iff convergent_def lim_def)
-lemma summable_LIMSEQ: "summable f \<Longrightarrow> (\<lambda>n. \<Sum>i<n. f i) ----> suminf f"
+lemma summable_LIMSEQ: "summable f \<Longrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> suminf f"
by (rule summable_sums [unfolded sums_def])
lemma sums_unique: "f sums s \<Longrightarrow> s = suminf f"
@@ -223,7 +223,7 @@
lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
proof
assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
- then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
+ then have f: "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> 0"
using summable_LIMSEQ[of f] by simp
then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
proof (rule LIMSEQ_le_const)
@@ -268,13 +268,13 @@
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
shows "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
proof -
- have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) ----> s + f 0"
+ have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
- also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) ----> s + f 0"
+ also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0)
also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
proof
- assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) ----> s + f 0"
+ assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
with tendsto_add[OF this tendsto_const, of "- f 0"]
show "(\<lambda>i. f (Suc i)) sums s"
by (simp add: sums_def)
@@ -361,7 +361,7 @@
by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF \<open>summable f\<close>])
qed
-lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
+lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f \<longlonglongrightarrow> 0"
apply (drule summable_iff_convergent [THEN iffD1])
apply (drule convergent_Cauchy)
apply (simp only: Cauchy_iff LIMSEQ_iff, safe)
@@ -503,11 +503,11 @@
assume less_1: "norm c < 1"
hence neq_1: "c \<noteq> 1" by auto
hence neq_0: "c - 1 \<noteq> 0" by simp
- from less_1 have lim_0: "(\<lambda>n. c^n) ----> 0"
+ from less_1 have lim_0: "(\<lambda>n. c^n) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_power_zero)
- hence "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) ----> 0 / (c - 1) - 1 / (c - 1)"
+ hence "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)"
using neq_0 by (intro tendsto_intros)
- hence "(\<lambda>n. (c ^ n - 1) / (c - 1)) ----> 1 / (1 - c)"
+ hence "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)"
by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
thus "(\<lambda>n. c ^ n) sums (1 / (1 - c))"
by (simp add: sums_def geometric_sum neq_1)
@@ -522,7 +522,7 @@
lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
proof
assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
- hence "(\<lambda>n. norm c ^ n) ----> 0"
+ hence "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0"
by (simp add: norm_power [symmetric] tendsto_norm_zero_iff summable_LIMSEQ_zero)
from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1"
by (auto simp: eventually_at_top_linorder)
@@ -545,28 +545,28 @@
subsection \<open>Telescoping\<close>
lemma telescope_sums:
- assumes "f ----> (c :: 'a :: real_normed_vector)"
+ assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
shows "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
unfolding sums_def
proof (subst LIMSEQ_Suc_iff [symmetric])
have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff)
- also have "\<dots> ----> c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
- finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) ----> c - f 0" .
+ also have "\<dots> \<longlonglongrightarrow> c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
+ finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0" .
qed
lemma telescope_sums':
- assumes "f ----> (c :: 'a :: real_normed_vector)"
+ assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
shows "(\<lambda>n. f n - f (Suc n)) sums (f 0 - c)"
using sums_minus[OF telescope_sums[OF assms]] by (simp add: algebra_simps)
lemma telescope_summable:
- assumes "f ----> (c :: 'a :: real_normed_vector)"
+ assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
shows "summable (\<lambda>n. f (Suc n) - f n)"
using telescope_sums[OF assms] by (simp add: sums_iff)
lemma telescope_summable':
- assumes "f ----> (c :: 'a :: real_normed_vector)"
+ assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
shows "summable (\<lambda>n. f n - f (Suc n))"
using summable_minus[OF telescope_summable[OF assms]] by (simp add: algebra_simps)
@@ -733,14 +733,14 @@
unfolding real_norm_def
by (simp only: abs_of_nonneg setsum_nonneg [rule_format])
- have "(\<lambda>n. (\<Sum>k<n. a k) * (\<Sum>k<n. b k)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
+ have "(\<lambda>n. (\<Sum>k<n. a k) * (\<Sum>k<n. b k)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b])
- hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
+ hence 1: "(\<lambda>n. setsum ?g (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
- have "(\<lambda>n. (\<Sum>k<n. norm (a k)) * (\<Sum>k<n. norm (b k))) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
+ have "(\<lambda>n. (\<Sum>k<n. norm (a k)) * (\<Sum>k<n. norm (b k))) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
using a b by (intro tendsto_mult summable_LIMSEQ)
- hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
+ hence "(\<lambda>n. setsum ?f (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
hence "convergent (\<lambda>n. setsum ?f (?S1 n))"
by (rule convergentI)
@@ -774,11 +774,11 @@
apply (rule order_trans [OF norm_setsum setsum_mono])
apply (auto simp add: norm_mult_ineq)
done
- hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"
+ hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) \<longlonglongrightarrow> 0"
unfolding tendsto_Zfun_iff diff_0_right
by (simp only: setsum_diff finite_S1 S2_le_S1)
- with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
+ with 1 have "(\<lambda>n. setsum ?g (?S2 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
by (rule Lim_transform2)
thus ?thesis by (simp only: sums_def setsum_triangle_reindex)
qed
@@ -933,12 +933,12 @@
have "incseq (\<lambda>n. \<Sum>i<n. (f \<circ> g) i)"
by (rule incseq_SucI) (auto simp add: pos)
- then obtain L where L: "(\<lambda> n. \<Sum>i<n. (f \<circ> g) i) ----> L"
+ then obtain L where L: "(\<lambda> n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> L"
using smaller by(rule incseq_convergent)
hence "(f \<circ> g) sums L" by (simp add: sums_def)
thus "summable (f o g)" by (auto simp add: sums_iff)
- hence "(\<lambda>n. \<Sum>i<n. (f \<circ> g) i) ----> suminf (f \<circ> g)"
+ hence "(\<lambda>n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> suminf (f \<circ> g)"
by(rule summable_LIMSEQ)
thus le: "suminf (f \<circ> g) \<le> suminf f"
by(rule LIMSEQ_le_const2)(blast intro: smaller[rule_format])
@@ -971,7 +971,7 @@
shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
unfolding sums_def
proof
- assume lim: "(\<lambda>n. \<Sum>k<n. f k) ----> c"
+ assume lim: "(\<lambda>n. \<Sum>k<n. f k) \<longlonglongrightarrow> c"
have "(\<lambda>n. \<Sum>k<n. f (g k)) = (\<lambda>n. \<Sum>k<g n. f k)"
proof
fix n :: nat
@@ -982,10 +982,10 @@
(auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
qed
- also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> ----> c" unfolding o_def .
- finally show "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c" .
+ also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c" unfolding o_def .
+ finally show "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" .
next
- assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c"
+ assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c"
def g_inv \<equiv> "\<lambda>n. LEAST m. g m \<ge> n"
from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n
by (auto simp: filterlim_at_top eventually_at_top_linorder)
@@ -1020,8 +1020,8 @@
}
hence "filterlim g_inv at_top sequentially"
by (auto simp: filterlim_at_top eventually_at_top_linorder)
- from lim and this have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) ----> c" by (rule filterlim_compose)
- finally show "(\<lambda>n. \<Sum>k<n. f k) ----> c" .
+ from lim and this have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) \<longlonglongrightarrow> c" by (rule filterlim_compose)
+ finally show "(\<lambda>n. \<Sum>k<n. f k) \<longlonglongrightarrow> c" .
qed
lemma summable_mono_reindex:
--- a/src/HOL/Topological_Spaces.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Dec 29 23:04:53 2015 +0100
@@ -779,16 +779,16 @@
abbreviation (in topological_space)
LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
- ("((_)/ ----> (_))" [60, 60] 60) where
- "X ----> L \<equiv> (X ---> L) sequentially"
+ ("((_)/ \<longlonglongrightarrow> (_))" [60, 60] 60) where
+ "X \<longlonglongrightarrow> L \<equiv> (X ---> L) sequentially"
abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
"lim X \<equiv> Lim sequentially X"
definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
- "convergent X = (\<exists>L. X ----> L)"
+ "convergent X = (\<exists>L. X \<longlonglongrightarrow> L)"
-lemma lim_def: "lim X = (THE L. X ----> L)"
+lemma lim_def: "lim X = (THE L. X \<longlonglongrightarrow> L)"
unfolding Lim_def ..
subsubsection \<open>Monotone sequences and subsequences\<close>
@@ -996,81 +996,81 @@
lemma LIMSEQ_const_iff:
fixes k l :: "'a::t2_space"
- shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
+ shows "(\<lambda>n. k) \<longlonglongrightarrow> l \<longleftrightarrow> k = l"
using trivial_limit_sequentially by (rule tendsto_const_iff)
lemma LIMSEQ_SUP:
- "incseq X \<Longrightarrow> X ----> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})"
+ "incseq X \<Longrightarrow> X \<longlonglongrightarrow> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})"
by (intro increasing_tendsto)
(auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
lemma LIMSEQ_INF:
- "decseq X \<Longrightarrow> X ----> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})"
+ "decseq X \<Longrightarrow> X \<longlonglongrightarrow> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})"
by (intro decreasing_tendsto)
(auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans)
lemma LIMSEQ_ignore_initial_segment:
- "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
+ "f \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. f (n + k)) \<longlonglongrightarrow> a"
unfolding tendsto_def
by (subst eventually_sequentially_seg[where k=k])
lemma LIMSEQ_offset:
- "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
+ "(\<lambda>n. f (n + k)) \<longlonglongrightarrow> a \<Longrightarrow> f \<longlonglongrightarrow> a"
unfolding tendsto_def
by (subst (asm) eventually_sequentially_seg[where k=k])
-lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
+lemma LIMSEQ_Suc: "f \<longlonglongrightarrow> l \<Longrightarrow> (\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l"
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
-lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
+lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l \<Longrightarrow> f \<longlonglongrightarrow> l"
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
-lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
+lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
lemma LIMSEQ_unique:
fixes a b :: "'a::t2_space"
- shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
+ shows "\<lbrakk>X \<longlonglongrightarrow> a; X \<longlonglongrightarrow> b\<rbrakk> \<Longrightarrow> a = b"
using trivial_limit_sequentially by (rule tendsto_unique)
lemma LIMSEQ_le_const:
- "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
+ "\<lbrakk>X \<longlonglongrightarrow> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
lemma LIMSEQ_le:
- "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
+ "\<lbrakk>X \<longlonglongrightarrow> x; Y \<longlonglongrightarrow> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
lemma LIMSEQ_le_const2:
- "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
+ "\<lbrakk>X \<longlonglongrightarrow> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
-lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
+lemma convergentD: "convergent X ==> \<exists>L. (X \<longlonglongrightarrow> L)"
by (simp add: convergent_def)
-lemma convergentI: "(X ----> L) ==> convergent X"
+lemma convergentI: "(X \<longlonglongrightarrow> L) ==> convergent X"
by (auto simp add: convergent_def)
-lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
+lemma convergent_LIMSEQ_iff: "convergent X = (X \<longlonglongrightarrow> lim X)"
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
lemma convergent_const: "convergent (\<lambda>n. c)"
by (rule convergentI, rule tendsto_const)
lemma monoseq_le:
- "monoseq a \<Longrightarrow> a ----> (x::'a::linorder_topology) \<Longrightarrow>
+ "monoseq a \<Longrightarrow> a \<longlonglongrightarrow> (x::'a::linorder_topology) \<Longrightarrow>
((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
lemma LIMSEQ_subseq_LIMSEQ:
- "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
+ "\<lbrakk> X \<longlonglongrightarrow> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) \<longlonglongrightarrow> L"
unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq])
lemma convergent_subseq_convergent:
"\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
-lemma limI: "X ----> L ==> lim X = L"
+lemma limI: "X \<longlonglongrightarrow> L ==> lim X = L"
by (rule tendsto_Lim) (rule trivial_limit_sequentially)
lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
@@ -1078,10 +1078,10 @@
subsubsection\<open>Increasing and Decreasing Series\<close>
-lemma incseq_le: "incseq X \<Longrightarrow> X ----> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)"
+lemma incseq_le: "incseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)"
by (metis incseq_def LIMSEQ_le_const)
-lemma decseq_le: "decseq X \<Longrightarrow> X ----> L \<Longrightarrow> (L::'a::linorder_topology) \<le> X n"
+lemma decseq_le: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> (L::'a::linorder_topology) \<le> X n"
by (metis decseq_def LIMSEQ_le_const2)
subsection \<open>First countable topologies\<close>
@@ -1142,7 +1142,7 @@
lemma (in first_countable_topology) countable_basis:
obtains A :: "nat \<Rightarrow> 'a set" where
"\<And>i. open (A i)" "\<And>i. x \<in> A i"
- "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F ----> x"
+ "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F \<longlonglongrightarrow> x"
proof atomize_elim
obtain A :: "nat \<Rightarrow> 'a set" where A:
"\<And>i. open (A i)"
@@ -1154,25 +1154,25 @@
with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
by (auto elim: eventually_mono simp: subset_eq)
}
- with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F ----> x)"
+ with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F \<longlonglongrightarrow> x)"
by (intro exI[of _ A]) (auto simp: tendsto_def)
qed
lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within:
- assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
+ assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
shows "eventually P (inf (nhds a) (principal s))"
proof (rule ccontr)
obtain A :: "nat \<Rightarrow> 'a set" where A:
"\<And>i. open (A i)"
"\<And>i. a \<in> A i"
- "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F ----> a"
+ "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F \<longlonglongrightarrow> a"
by (rule countable_basis) blast
assume "\<not> ?thesis"
with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
then obtain F where F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
by blast
- with A have "F ----> a" by auto
+ with A have "F \<longlonglongrightarrow> a" by auto
hence "eventually (\<lambda>n. P (F n)) sequentially"
using assms F0 by simp
thus "False" by (simp add: F3)
@@ -1180,23 +1180,23 @@
lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially:
"eventually P (inf (nhds a) (principal s)) \<longleftrightarrow>
- (\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
+ (\<forall>f. (\<forall>n. f n \<in> s) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
proof (safe intro!: sequentially_imp_eventually_nhds_within)
assume "eventually P (inf (nhds a) (principal s))"
then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x"
by (auto simp: eventually_inf_principal eventually_nhds)
- moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
+ moreover fix f assume "\<forall>n. f n \<in> s" "f \<longlonglongrightarrow> a"
ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
by (auto dest!: topological_tendstoD elim: eventually_mono)
qed
lemma (in first_countable_topology) eventually_nhds_iff_sequentially:
- "eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
+ "eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp
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 ----> x \<longrightarrow> ((f \<circ> X) ----> a))"
+ 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))"
unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap at_within_def eventually_nhds_within_iff_sequentially comp_def
by metis
@@ -1269,39 +1269,39 @@
subsubsection \<open>Relation of LIM and LIMSEQ\<close>
lemma (in first_countable_topology) sequentially_imp_eventually_within:
- "(\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow>
+ "(\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow>
eventually P (at a within s)"
unfolding at_within_def
by (intro sequentially_imp_eventually_nhds_within) auto
lemma (in first_countable_topology) sequentially_imp_eventually_at:
- "(\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> eventually P (at a)"
+ "(\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> eventually P (at a)"
using assms sequentially_imp_eventually_within [where s=UNIV] by simp
lemma LIMSEQ_SEQ_conv1:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
assumes f: "f -- a --> l"
- shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
+ shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
using tendsto_compose_eventually [OF f, where F=sequentially] by simp
lemma LIMSEQ_SEQ_conv2:
fixes f :: "'a::first_countable_topology \<Rightarrow> 'b::topological_space"
- assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
+ assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
shows "f -- a --> l"
using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at)
lemma LIMSEQ_SEQ_conv:
- "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::first_countable_topology) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
+ "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> (a::'a::first_countable_topology) \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L) =
(X -- a --> (L::'b::topological_space))"
using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
lemma sequentially_imp_eventually_at_left:
fixes a :: "'a :: {linorder_topology, first_countable_topology}"
assumes b[simp]: "b < a"
- assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
+ assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f \<longlonglongrightarrow> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
shows "eventually P (at_left a)"
proof (safe intro!: sequentially_imp_eventually_within)
- fix X assume X: "\<forall>n. X n \<in> {..< a} \<and> X n \<noteq> a" "X ----> a"
+ fix X assume X: "\<forall>n. X n \<in> {..< a} \<and> X n \<noteq> a" "X \<longlonglongrightarrow> a"
show "eventually (\<lambda>n. P (X n)) sequentially"
proof (rule ccontr)
assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially"
@@ -1319,8 +1319,8 @@
by (auto dest!: not_eventuallyD)
qed
then guess s ..
- then have "\<And>n. b < X (s n)" "\<And>n. X (s n) < a" "incseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) ----> a" "\<And>n. \<not> P (X (s n))"
- using X by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X ----> a\<close>, unfolded comp_def])
+ then have "\<And>n. b < X (s n)" "\<And>n. X (s n) < a" "incseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a" "\<And>n. \<not> P (X (s n))"
+ using X by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
from *[OF this(1,2,3,4)] this(5) show False by auto
qed
qed
@@ -1328,7 +1328,7 @@
lemma tendsto_at_left_sequentially:
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 ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
+ 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)"
using assms unfolding tendsto_def [where l=L]
by (simp add: sequentially_imp_eventually_at_left)
@@ -1336,10 +1336,10 @@
lemma sequentially_imp_eventually_at_right:
fixes a :: "'a :: {linorder_topology, first_countable_topology}"
assumes b[simp]: "a < b"
- assumes *: "\<And>f. (\<And>n. a < f n) \<Longrightarrow> (\<And>n. f n < b) \<Longrightarrow> decseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
+ assumes *: "\<And>f. (\<And>n. a < f n) \<Longrightarrow> (\<And>n. f n < b) \<Longrightarrow> decseq f \<Longrightarrow> f \<longlonglongrightarrow> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
shows "eventually P (at_right a)"
proof (safe intro!: sequentially_imp_eventually_within)
- fix X assume X: "\<forall>n. X n \<in> {a <..} \<and> X n \<noteq> a" "X ----> a"
+ fix X assume X: "\<forall>n. X n \<in> {a <..} \<and> X n \<noteq> a" "X \<longlonglongrightarrow> a"
show "eventually (\<lambda>n. P (X n)) sequentially"
proof (rule ccontr)
assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially"
@@ -1357,8 +1357,8 @@
by (auto dest!: not_eventuallyD)
qed
then guess s ..
- then have "\<And>n. a < X (s n)" "\<And>n. X (s n) < b" "decseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) ----> a" "\<And>n. \<not> P (X (s n))"
- using X by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X ----> a\<close>, unfolded comp_def])
+ then have "\<And>n. a < X (s n)" "\<And>n. X (s n) < b" "decseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a" "\<And>n. \<not> P (X (s n))"
+ using X by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
from *[OF this(1,2,3,4)] this(5) show False by auto
qed
qed
@@ -1366,7 +1366,7 @@
lemma tendsto_at_right_sequentially:
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 ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
+ 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)"
using assms unfolding tendsto_def [where l=L]
by (simp add: sequentially_imp_eventually_at_right)
--- a/src/HOL/Transcendental.thy Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Transcendental.thy Tue Dec 29 23:04:53 2015 +0100
@@ -41,7 +41,7 @@
lemma root_test_convergence:
fixes f :: "nat \<Rightarrow> 'a::banach"
- assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" \<comment> "could be weakened to lim sup"
+ assumes f: "(\<lambda>n. root n (norm (f n))) \<longlonglongrightarrow> x" \<comment> "could be weakened to lim sup"
assumes "x < 1"
shows "summable f"
proof -
@@ -92,7 +92,7 @@
shows "summable (\<lambda>n. norm (f n * z ^ n))"
proof -
from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
- from 1 have "(\<lambda>n. f n * x^n) ----> 0"
+ from 1 have "(\<lambda>n. f n * x^n) \<longlonglongrightarrow> 0"
by (rule summable_LIMSEQ_zero)
hence "convergent (\<lambda>n. f n * x^n)"
by (rule convergentI)
@@ -148,7 +148,7 @@
lemma powser_times_n_limit_0:
fixes x :: "'a::{real_normed_div_algebra,banach}"
assumes "norm x < 1"
- shows "(\<lambda>n. of_nat n * x ^ n) ----> 0"
+ shows "(\<lambda>n. of_nat n * x ^ n) \<longlonglongrightarrow> 0"
proof -
have "norm x / (1 - norm x) \<ge> 0"
using assms
@@ -270,9 +270,9 @@
lemma sums_alternating_upper_lower:
fixes a :: "nat \<Rightarrow> real"
- assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
- shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) ----> l) \<and>
- ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) ----> l)"
+ assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a \<longlonglongrightarrow> 0"
+ shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) \<longlonglongrightarrow> l) \<and>
+ ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) \<longlonglongrightarrow> l)"
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
proof (rule nested_sequence_unique)
have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
@@ -294,11 +294,11 @@
show "?f n \<le> ?g n" using fg_diff a_pos
unfolding One_nat_def by auto
qed
- show "(\<lambda>n. ?f n - ?g n) ----> 0" unfolding fg_diff
+ show "(\<lambda>n. ?f n - ?g n) \<longlonglongrightarrow> 0" unfolding fg_diff
proof (rule LIMSEQ_I)
fix r :: real
assume "0 < r"
- with \<open>a ----> 0\<close>[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
+ with \<open>a \<longlonglongrightarrow> 0\<close>[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
by auto
hence "\<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
thus "\<exists>N. \<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
@@ -307,14 +307,14 @@
lemma summable_Leibniz':
fixes a :: "nat \<Rightarrow> real"
- assumes a_zero: "a ----> 0"
+ assumes a_zero: "a \<longlonglongrightarrow> 0"
and a_pos: "\<And> n. 0 \<le> a n"
and a_monotone: "\<And> n. a (Suc n) \<le> a n"
shows summable: "summable (\<lambda> n. (-1)^n * a n)"
and "\<And>n. (\<Sum>i<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
- and "(\<lambda>n. \<Sum>i<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
+ and "(\<lambda>n. \<Sum>i<2*n. (-1)^i*a i) \<longlonglongrightarrow> (\<Sum>i. (-1)^i*a i)"
and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i<2*n+1. (-1)^i*a i)"
- and "(\<lambda>n. \<Sum>i<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
+ and "(\<lambda>n. \<Sum>i<2*n+1. (-1)^i*a i) \<longlonglongrightarrow> (\<Sum>i. (-1)^i*a i)"
proof -
let ?S = "\<lambda>n. (-1)^n * a n"
let ?P = "\<lambda>n. \<Sum>i<n. ?S i"
@@ -322,20 +322,20 @@
let ?g = "\<lambda>n. ?P (2 * n + 1)"
obtain l :: real
where below_l: "\<forall> n. ?f n \<le> l"
- and "?f ----> l"
+ and "?f \<longlonglongrightarrow> l"
and above_l: "\<forall> n. l \<le> ?g n"
- and "?g ----> l"
+ and "?g \<longlonglongrightarrow> l"
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
let ?Sa = "\<lambda>m. \<Sum>n<m. ?S n"
- have "?Sa ----> l"
+ have "?Sa \<longlonglongrightarrow> l"
proof (rule LIMSEQ_I)
fix r :: real
assume "0 < r"
- with \<open>?f ----> l\<close>[THEN LIMSEQ_D]
+ with \<open>?f \<longlonglongrightarrow> l\<close>[THEN LIMSEQ_D]
obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto
- from \<open>0 < r\<close> \<open>?g ----> l\<close>[THEN LIMSEQ_D]
+ from \<open>0 < r\<close> \<open>?g \<longlonglongrightarrow> l\<close>[THEN LIMSEQ_D]
obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto
{
@@ -377,22 +377,22 @@
unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
show "?f n \<le> suminf ?S"
unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
- show "?g ----> suminf ?S"
- using \<open>?g ----> l\<close> \<open>l = suminf ?S\<close> by auto
- show "?f ----> suminf ?S"
- using \<open>?f ----> l\<close> \<open>l = suminf ?S\<close> by auto
+ show "?g \<longlonglongrightarrow> suminf ?S"
+ using \<open>?g \<longlonglongrightarrow> l\<close> \<open>l = suminf ?S\<close> by auto
+ show "?f \<longlonglongrightarrow> suminf ?S"
+ using \<open>?f \<longlonglongrightarrow> l\<close> \<open>l = suminf ?S\<close> by auto
qed
theorem summable_Leibniz:
fixes a :: "nat \<Rightarrow> real"
- assumes a_zero: "a ----> 0" and "monoseq a"
+ assumes a_zero: "a \<longlonglongrightarrow> 0" and "monoseq a"
shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
and "0 < a 0 \<longrightarrow>
(\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
and "a 0 < 0 \<longrightarrow>
(\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
- and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
- and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
+ and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) \<longlonglongrightarrow> (\<Sum>i. (- 1)^i*a i)" (is "?f")
+ and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) \<longlonglongrightarrow> (\<Sum>i. (- 1)^i*a i)" (is "?g")
proof -
have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
@@ -404,13 +404,13 @@
have "a (Suc n) \<le> a n"
using ord[where n="Suc n" and m=n] by auto
} note mono = this
- note leibniz = summable_Leibniz'[OF \<open>a ----> 0\<close> ge0]
+ note leibniz = summable_Leibniz'[OF \<open>a \<longlonglongrightarrow> 0\<close> ge0]
from leibniz[OF mono]
show ?thesis using \<open>0 \<le> a 0\<close> by auto
next
let ?a = "\<lambda> n. - a n"
case False
- with monoseq_le[OF \<open>monoseq a\<close> \<open>a ----> 0\<close>]
+ with monoseq_le[OF \<open>monoseq a\<close> \<open>a \<longlonglongrightarrow> 0\<close>]
have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n"
by auto
@@ -421,7 +421,7 @@
} note monotone = this
note leibniz =
summable_Leibniz'[OF _ ge0, of "\<lambda>x. x",
- OF tendsto_minus[OF \<open>a ----> 0\<close>, unfolded minus_zero] monotone]
+ OF tendsto_minus[OF \<open>a \<longlonglongrightarrow> 0\<close>, unfolded minus_zero] monotone]
have "summable (\<lambda> n. (-1)^n * ?a n)"
using leibniz(1) by auto
then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l"
@@ -724,7 +724,7 @@
then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0"
using K False
by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
- have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) ----> 0"
+ have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) \<longlonglongrightarrow> 0"
using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"])
then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> real_of_nat n * norm x ^ n < r ^ n"
using r unfolding LIMSEQ_iff
@@ -2646,7 +2646,7 @@
lemma tendsto_exp_limit_sequentially:
fixes x :: real
- shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
+ shows "(\<lambda>n. (1 + x / n) ^ n) \<longlonglongrightarrow> exp x"
proof (rule filterlim_mono_eventually)
from reals_Archimedean2 [of "\<bar>x\<bar>"] obtain n :: nat where *: "real n > \<bar>x\<bar>" ..
hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
@@ -2658,7 +2658,7 @@
done
then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
by (rule eventually_mono) (erule powr_realpow)
- show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
+ show "(\<lambda>n. (1 + x / real n) powr real n) \<longlonglongrightarrow> exp x"
by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
qed auto
@@ -4986,7 +4986,7 @@
lemma zeroseq_arctan_series:
fixes x :: real
assumes "\<bar>x\<bar> \<le> 1"
- shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
+ shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) \<longlonglongrightarrow> 0" (is "?a \<longlonglongrightarrow> 0")
proof (cases "x = 0")
case True
thus ?thesis
@@ -4994,12 +4994,12 @@
next
case False
have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
- show "?a ----> 0"
+ show "?a \<longlonglongrightarrow> 0"
proof (cases "\<bar>x\<bar> < 1")
case True
hence "norm x < 1" by auto
from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF \<open>norm x < 1\<close>, THEN LIMSEQ_Suc]]
- have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
+ have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) \<longlonglongrightarrow> 0"
unfolding inverse_eq_divide Suc_eq_plus1 by simp
then show ?thesis using pos2 by (rule LIMSEQ_linear)
next
@@ -5252,15 +5252,15 @@
by (rule LIM_less_bound)
hence "?diff 1 n \<le> ?a 1 n" by auto
}
- have "?a 1 ----> 0"
+ have "?a 1 \<longlonglongrightarrow> 0"
unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat simp del: of_nat_Suc)
- have "?diff 1 ----> 0"
+ have "?diff 1 \<longlonglongrightarrow> 0"
proof (rule LIMSEQ_I)
fix r :: real
assume "0 < r"
obtain N :: nat where N_I: "\<And>n. N \<le> n \<Longrightarrow> ?a 1 n < r"
- using LIMSEQ_D[OF \<open>?a 1 ----> 0\<close> \<open>0 < r\<close>] by auto
+ using LIMSEQ_D[OF \<open>?a 1 \<longlonglongrightarrow> 0\<close> \<open>0 < r\<close>] by auto
{
fix n
assume "N \<le> n" from \<open>?diff 1 n \<le> ?a 1 n\<close> N_I[OF this]