# HG changeset patch # User wenzelm # Date 1451426693 -3600 # Node ID e01015e49041761ac4e419a8e897b5c19de563a2 # Parent e13e70f32407a3f82d6eb8f1a3cca49c3371f09f more symbols; diff -r e13e70f32407 -r e01015e49041 NEWS --- 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 "\" for type and sort constraints has been removed: in LaTeX document output it looks the same as "::". INCOMPATIBILITY, use plain "::" instead. diff -r e13e70f32407 -r e01015e49041 src/HOL/Complex.thy --- 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 \ complex" assume X: "Cauchy X" - then have "(\n. Complex (Re (X n)) (Im (X n))) ----> Complex (lim (\n. Re (X n))) (lim (\n. Im (X n)))" + then have "(\n. Complex (Re (X n)) (Im (X n))) \ Complex (lim (\n. Re (X n))) (lim (\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) diff -r e13e70f32407 -r e01015e49041 src/HOL/Decision_Procs/Approximation.thy --- 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"] \0 \ x\ \x < 1\ by auto have "norm x < 1" using assms by auto - have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric] + have "?a \ 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 \norm x < 1\]]] by auto have "0 \ ?a n" for n by (rule mult_nonneg_nonneg) (auto simp: \0 \ x\) @@ -2117,7 +2117,7 @@ by (rule mult_left_mono, fact less_imp_le[OF \x < 1\]) (auto simp: \0 \ x\) thus "x ^ Suc (Suc n) \ x ^ Suc n" by auto qed auto - from summable_Leibniz'(2,4)[OF \?a ----> 0\ \\n. 0 \ ?a n\, OF \\n. ?a (Suc n) \ ?a n\, unfolded ln_eq] + from summable_Leibniz'(2,4)[OF \?a \ 0\ \\n. 0 \ ?a n\, OF \\n. ?a (Suc n) \ ?a n\, unfolded ln_eq] show ?lb and ?ub unfolding atLeast0LessThan by auto qed diff -r e13e70f32407 -r e01015e49041 src/HOL/Library/BigO.thy --- 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) \ g ----> 0 \ f ----> (0::real)" +lemma bigo_LIMSEQ1: "f =o O(g) \ g \ 0 \ f \ (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) \ h ----> 0 \ f ----> a \ g ----> (a::real)" +lemma bigo_LIMSEQ2: "f =o g +o O(h) \ h \ 0 \ f \ a \ g \ (a::real)" apply (drule set_plus_imp_minus) apply (drule bigo_LIMSEQ1) apply assumption diff -r e13e70f32407 -r e01015e49041 src/HOL/Library/Extended_Real.thy --- 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 \ 'a" assume S: "incseq S" and S_x: "S ----> x" + fix S :: "nat \ 'a" assume S: "incseq S" and S_x: "S \ x" from S_x have x_eq: "x = (SUP i. S i)" by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S) - show "(\n. f (S n)) ----> f x" + show "(\n. f (S n)) \ 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 \ 'a" assume S: "decseq S" and S_x: "S ----> x" + fix S :: "nat \ 'a" assume S: "decseq S" and S_x: "S \ x" from S_x have x_eq: "x = (INF i. S i)" by (rule LIMSEQ_unique) (intro LIMSEQ_INF S) - show "(\n. f (S n)) ----> f x" + show "(\n. f (S n)) \ 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 \ -\" - shows "\f. incseq f \ (\i::nat. f i < x) \ (f ----> x)" + shows "\f. incseq f \ (\i::nat. f i < x) \ (f \ x)" proof (cases x) case (real r) - moreover have "(\n. r - inverse (real (Suc n))) ----> r - 0" + moreover have "(\n. r - inverse (real (Suc n))) \ r - 0" by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) ultimately show ?thesis by (intro exI[of _ "\n. x - inverse (Suc n)"]) (auto simp: incseq_def) @@ -2141,7 +2141,7 @@ by (auto intro!: exI[of _ "\_. -\"] simp: bot_ereal_def) next assume "Sup A \ -\" - then obtain l where "incseq l" and l: "\i::nat. l i < Sup A" and l_Sup: "l ----> Sup A" + then obtain l where "incseq l" and l: "\i::nat. l i < Sup A" and l_Sup: "l \ Sup A" by (auto dest: countable_approach) have "\f. \n. (f n \ A \ l n \ f n) \ (f n \ 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 \ (SUP i. f i)" by (rule LIMSEQ_SUP \incseq f\)+ - show "f ----> Sup A" + show "f \ 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 (\n. ereal (a n))" and "lim (\n. ereal (a n)) = ereal (lim a)" proof - - from assms obtain L where L: "a ----> L" unfolding convergent_def .. - hence lim: "(\n. ereal (a n)) ----> ereal L" using lim_ereal by auto + from assms obtain L where L: "a \ L" unfolding convergent_def .. + hence lim: "(\n. ereal (a n)) \ ereal L" using lim_ereal by auto thus "convergent (\n. ereal (a n))" unfolding convergent_def .. thus "lim (\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 ----> \ \ (\B. \N. \n\N. f n \ ereal B)" +lemma Lim_PInfty: "f \ \ \ (\B. \N. \n\N. f n \ 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 ----> -\ \ (\B. \N. \n\N. ereal B \ f n)" +lemma Lim_MInfty: "f \ -\ \ (\B. \N. \n\N. ereal B \ 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 \ (\n. f n \ ereal B) \ l \ \" +lemma Lim_bounded_PInfty: "f \ l \ (\n. f n \ ereal B) \ l \ \" using LIMSEQ_le_const2[of f l "ereal B"] by auto -lemma Lim_bounded_MInfty: "f ----> l \ (\n. ereal B \ f n) \ l \ -\" +lemma Lim_bounded_MInfty: "f \ l \ (\n. ereal B \ f n) \ l \ -\" using LIMSEQ_le_const[of f l "ereal B"] by auto lemma tendsto_explicit: - "f ----> f0 \ (\S. open S \ f0 \ S \ (\N. \n\N. f n \ S))" + "f \ f0 \ (\S. open S \ f0 \ S \ (\N. \n\N. f n \ S))" unfolding tendsto_def eventually_sequentially by auto -lemma Lim_bounded_PInfty2: "f ----> l \ \n\N. f n \ ereal B \ l \ \" +lemma Lim_bounded_PInfty2: "f \ l \ \n\N. f n \ ereal B \ l \ \" using LIMSEQ_le_const2[of f l "ereal B"] by fastforce -lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \ \n\M. f n \ C \ l \ C" +lemma Lim_bounded_ereal: "f \ (l :: 'a::linorder_topology) \ \n\M. f n \ C \ l \ C" by (intro LIMSEQ_le_const2) auto lemma Lim_bounded2_ereal: - assumes lim:"f ----> (l :: 'a::linorder_topology)" + assumes lim:"f \ (l :: 'a::linorder_topology)" and ge: "\n\N. f n \ C" shows "l \ C" using ge @@ -2696,7 +2696,7 @@ fixes x :: ereal assumes "\x\ \ \" and "\r. 0 < r \ \N. \n\N. u n < x + r \ x < u n + r" - shows "u ----> x" + shows "u \ 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 \ f0" assumes "open S" and "f0 \ S" obtains N where "\n\N. f n \ S" @@ -2742,10 +2742,10 @@ lemma ereal_LimI_finite_iff: fixes x :: ereal assumes "\x\ \ \" - shows "u ----> x \ (\r. 0 < r \ (\N. \n\N. u n < x + r \ x < u n + r))" + shows "u \ x \ (\r. 0 < r \ (\N. \n\N. u n < x + r \ x < u n + r))" (is "?lhs \ ?rhs") proof - assume lim: "u ----> x" + assume lim: "u \ x" { fix r :: ereal assume "r > 0" @@ -2762,7 +2762,7 @@ by auto next assume ?rhs - then show "u ----> x" + then show "u \ x" using ereal_LimI_finite[of x] assms by auto qed @@ -2924,7 +2924,7 @@ shows "suminf f \ x" proof (rule Lim_bounded_ereal) have "summable f" using pos[THEN summable_ereal_pos] . - then show "(\N. \n suminf f" + then show "(\N. \n suminf f" by (auto dest!: summable_sums simp: sums_def atLeast0LessThan) show "\n\0. setsum f {.. x" using assms by auto @@ -3195,11 +3195,11 @@ assumes f: "\i. 0 \ f i" shows "(\i. f (i + k)) \ suminf f" proof - - have "(\n. \i (\i. f (i + k))" + have "(\n. \i (\i. f (i + k))" using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f) - moreover have "(\n. \i (\i. f i)" + moreover have "(\n. \i (\i. f i)" using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f) - then have "(\n. \i (\i. f i)" + then have "(\n. \i (\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 \ real" and L :: real assumes 1: "limsup X \ L" and 2: "L \ liminf X" - shows "X ----> L" + shows "X \ L" proof - from 1 2 have "limsup X \ 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 (\n. ereal(X n)) = L" .. - hence "(\n. ereal (X n)) ----> L" + hence "(\n. ereal (X n)) \ 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 \ ereal" - shows "X ----> \ \ liminf X = \" + shows "X \ \ \ liminf X = \" by (metis Liminf_PInfty trivial_limit_sequentially) lemma limsup_MInfty: fixes X :: "nat \ ereal" - shows "X ----> -\ \ limsup X = -\" + shows "X \ -\ \ limsup X = -\" by (metis Limsup_MInfty trivial_limit_sequentially) lemma ereal_lim_mono: fixes X Y :: "nat \ 'a::linorder_topology" assumes "\n. N \ n \ X n \ Y n" - and "X ----> x" - and "Y ----> y" + and "X \ x" + and "Y \ y" shows "x \ y" using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto lemma incseq_le_ereal: fixes X :: "nat \ 'a::linorder_topology" assumes inc: "incseq X" - and lim: "X ----> L" + and lim: "X \ L" shows "X N \ 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 \ (L::'a::linorder_topology)" shows "X N \ 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 "\n. b n \ s" - and "b ----> a" + and "b \ a" shows "a \ 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 "\n. b n \ s" - and "b ----> a" + and "b \ a" shows "Inf s \ a" by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower) lemma SUP_Lim_ereal: fixes X :: "nat \ 'a::{complete_linorder,linorder_topology}" assumes inc: "incseq X" - and l: "X ----> l" + and l: "X \ 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 \ 'a::{complete_linorder,linorder_topology}" assumes dec: "decseq X" - and l: "X ----> l" + and l: "X \ 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 \ f ----> x" + shows "(SUP n. ereal (f n)) = ereal x \ f \ x" proof have inc: "incseq (\i. ereal (f i))" using \mono f\ unfolding mono_def incseq_def by auto { - assume "f ----> x" - then have "(\i. ereal (f i)) ----> ereal x" + assume "f \ x" + then have "(\i. ereal (f i)) \ 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 \ x" by auto } qed diff -r e13e70f32407 -r e01015e49041 src/HOL/Library/Formal_Power_Series.thy --- 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: "(\n. setsum (\i. fps_const(a$i) * X^i) {0..n}) ----> a" - (is "?s ----> a") +lemma fps_notation: "(\n. setsum (\i. fps_const(a$i) * X^i) {0..n}) \ a" + (is "?s \ a") proof - have "\n0. \n \ 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 (\i. X (M i) $ i)" + show "X \ Abs_fps (\i. X (M i) $ i)" unfolding tendsto_iff proof safe fix e::real assume e: "0 < e" - have "(\n. inverse (2 ^ n) :: real) ----> 0" by (rule LIMSEQ_inverse_realpow_zero) simp_all + have "(\n. inverse (2 ^ n) :: real) \ 0" by (rule LIMSEQ_inverse_realpow_zero) simp_all from this and e have "eventually (\i. inverse (2 ^ i) < e) sequentially" by (rule order_tendstoD) then obtain i where "inverse (2 ^ i) < e" diff -r e13e70f32407 -r e01015e49041 src/HOL/Library/Indicator_Function.thy --- 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 "(\i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\i. A i) x" + shows "(\i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \ indicator (\i. A i) x" proof cases assume "\i. x \ A i" then obtain i where "x \ A i" @@ -97,9 +97,9 @@ qed (auto simp: indicator_def) lemma LIMSEQ_indicator_UN: - "(\k. indicator (\i indicator (\i. A i) x" + "(\k. indicator (\i indicator (\i. A i) x" proof - - have "(\k. indicator (\i indicator (\k. \ik. indicator (\i indicator (\k. \ik. \ii. A i)" by auto @@ -108,7 +108,7 @@ lemma LIMSEQ_indicator_decseq: assumes "decseq A" - shows "(\i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\i. A i) x" + shows "(\i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \ indicator (\i. A i) x" proof cases assume "\i. x \ A i" then obtain i where "x \ A i" @@ -122,9 +122,9 @@ qed (auto simp: indicator_def) lemma LIMSEQ_indicator_INT: - "(\k. indicator (\i indicator (\i. A i) x" + "(\k. indicator (\i indicator (\i. A i) x" proof - - have "(\k. indicator (\i indicator (\k. \ik. indicator (\i indicator (\k. \ik. \ii. A i)" by auto diff -r e13e70f32407 -r e01015e49041 src/HOL/Library/Liminf_Limsup.thy --- 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 "\n m. n \ m \ f n \ f m" - obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})" + obtains l where "f \ (l::'a::{complete_linorder,linorder_topology})" proof - show "f ----> (SUP n. f n)" + show "f \ (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 "\n m. n \ m \ f n \ f m" - obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})" + obtains l where "f \ (l::'a::{complete_linorder,linorder_topology})" proof - show "f ----> (INF n. f n)" + show "f \ (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 \ 'a::{complete_linorder,linorder_topology}" - shows "\l r. subseq r \ (X \ r) ----> l" + shows "\l r. subseq r \ (X \ r) \ l" proof - obtain r where "subseq r" and mono: "monoseq (X \ r)" using seq_monosub[of X] @@ -393,7 +393,7 @@ by auto then have "(\n m. m \ n \ (X \ r) m \ (X \ r) n) \ (\n m. m \ n \ (X \ r) n \ (X \ r) m)" by (auto simp add: monoseq_def) - then obtain l where "(X \ r) ----> l" + then obtain l where "(X \ r) \ l" using lim_increasing_cl[of "X \ r"] lim_decreasing_cl[of "X \ r"] by auto then show ?thesis diff -r e13e70f32407 -r e01015e49041 src/HOL/Library/Lub_Glb.thy --- 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 \ real" assumes u: "isLub UNIV {x. \n. X n = x} u" (* FIXME: use 'range X' *) assumes X: "\m n. m \ n \ X m \ X n" - shows "X ----> u" + shows "X \ u" proof - - have "X ----> (SUP i. X i)" + have "X \ (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" diff -r e13e70f32407 -r e01015e49041 src/HOL/Library/Product_Vector.thy --- 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 \ 'a \ 'b" assume "Cauchy X" - have 1: "(\n. fst (X n)) ----> lim (\n. fst (X n))" + have 1: "(\n. fst (X n)) \ lim (\n. fst (X n))" using Cauchy_fst [OF \Cauchy X\] by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - have 2: "(\n. snd (X n)) ----> lim (\n. snd (X n))" + have 2: "(\n. snd (X n)) \ lim (\n. snd (X n))" using Cauchy_snd [OF \Cauchy X\] by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - have "X ----> (lim (\n. fst (X n)), lim (\n. snd (X n)))" + have "X \ (lim (\n. fst (X n)), lim (\n. snd (X n)))" using tendsto_Pair [OF 1 2] by simp then show "convergent X" by (rule convergentI) diff -r e13e70f32407 -r e01015e49041 src/HOL/Limits.thy --- 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: "\n. m \ n --> X n = X m ==> \L. (X ----> L)" +lemma Bmonoseq_LIMSEQ: "\n. m \ n --> X n = X m ==> \L. (X \ 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 \Limits of Sequences\ -lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z" +lemma [trans]: "X=Y ==> Y \ z ==> X \ z" by simp lemma LIMSEQ_iff: fixes L :: "'a::real_normed_vector" - shows "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" + shows "(X \ L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" unfolding lim_sequentially dist_norm .. lemma LIMSEQ_I: fixes L :: "'a::real_normed_vector" - shows "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X ----> L" + shows "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X \ L" by (simp add: LIMSEQ_iff) lemma LIMSEQ_D: fixes L :: "'a::real_normed_vector" - shows "\X ----> L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" + shows "\X \ L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" by (simp add: LIMSEQ_iff) -lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ n. X (n * l)) ----> x" +lemma LIMSEQ_linear: "\ X \ x ; l > 0 \ \ (\ n. X (n * l)) \ 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 "\X ----> a; a \ 0\ \ Bseq (\n. inverse (X n))" + shows "\X \ a; a \ 0\ \ Bseq (\n. inverse (X n))" by (rule Bfun_inverse) text\Transformation of limit.\ @@ -1607,7 +1607,7 @@ text\An unbounded sequence's inverse tends to 0\ lemma LIMSEQ_inverse_zero: - "\r::real. \N. \n\N. r < X n \ (\n. inverse (X n)) ----> 0" + "\r::real. \N. \n\N. r < X n \ (\n. inverse (X n)) \ 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\The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity\ -lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" +lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) \ 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\ lemma LIMSEQ_inverse_real_of_nat_add: - "(%n. r + inverse(real(Suc n))) ----> r" + "(%n. r + inverse(real(Suc n))) \ 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))) \ 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)))) \ 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: "((\n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially" using lim_1_over_n by (simp add: inverse_eq_divide) -lemma LIMSEQ_Suc_n_over_n: "(\n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) ----> 1" +lemma LIMSEQ_Suc_n_over_n: "(\n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \ 1" proof (rule Lim_transform_eventually) show "eventually (\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 "(\n. 1 + inverse (of_nat n) :: 'a) ----> 1 + 0" + have "(\n. 1 + inverse (of_nat n) :: 'a) \ 1 + 0" by (intro tendsto_add tendsto_const lim_inverse_n) - thus "(\n. 1 + inverse (of_nat n) :: 'a) ----> 1" by simp + thus "(\n. 1 + inverse (of_nat n) :: 'a) \ 1" by simp qed -lemma LIMSEQ_n_over_Suc_n: "(\n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) ----> 1" +lemma LIMSEQ_n_over_Suc_n: "(\n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \ 1" proof (rule Lim_transform_eventually) show "eventually (\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 "(\n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> inverse 1" + have "(\n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \ inverse 1" by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all - thus "(\n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> 1" by simp + thus "(\n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \ 1" by simp qed subsection \Convergence on sequences\ @@ -1733,8 +1733,8 @@ assumes "convergent f" shows "convergent (\n. norm (f n))" proof - - from assms have "f ----> lim f" by (simp add: convergent_LIMSEQ_iff) - hence "(\n. norm (f n)) ----> norm (lim f)" by (rule tendsto_norm) + from assms have "f \ lim f" by (simp add: convergent_LIMSEQ_iff) + hence "(\n. norm (f n)) \ norm (lim f)" by (rule tendsto_norm) thus ?thesis by (auto simp: convergent_def) qed @@ -1794,7 +1794,7 @@ fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" assumes u: "bdd_above (range X)" assumes X: "incseq X" - shows "X ----> (SUP i. X i)" + shows "X \ (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 \ 'a::{conditionally_complete_linorder, linorder_topology}" assumes u: "bdd_below (range X)" assumes X: "decseq X" - shows "X ----> (INF i. X i)" + shows "X \ (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 \ real" assumes "incseq X" and "\i. X i \ B" - obtains L where "X ----> L" "\i. X i \ L" + obtains L where "X \ L" "\i. X i \ L" proof atomize_elim from incseq_bounded[OF assms] \incseq X\ Bseq_monoseq_convergent[of X] - obtain L where "X ----> L" + obtain L where "X \ L" by (auto simp: convergent_def monoseq_def incseq_def) - with \incseq X\ show "\L. X ----> L \ (\i. X i \ L)" + with \incseq X\ show "\L. X \ L \ (\i. X i \ L)" by (auto intro!: exI[of _ L] incseq_le) qed lemma decseq_convergent: fixes X :: "nat \ real" assumes "decseq X" and "\i. B \ X i" - obtains L where "X ----> L" "\i. L \ X i" + obtains L where "X \ L" "\i. L \ X i" proof atomize_elim from decseq_bounded[OF assms] \decseq X\ Bseq_monoseq_convergent[of X] - obtain L where "X ----> L" + obtain L where "X \ L" by (auto simp: convergent_def monoseq_def decseq_def) - with \decseq X\ show "\L. X ----> L \ (\i. L \ X i)" + with \decseq X\ show "\L. X \ L \ (\i. L \ X i)" by (auto intro!: exI[of _ L] decseq_le) qed @@ -1901,39 +1901,39 @@ "[| 0 \ (x::real); x \ 1 |] ==> convergent (%n. x ^ n)" by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) -lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" +lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \ (\n. inverse (x ^ n)) \ 0" by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp lemma LIMSEQ_realpow_zero: - "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" + "\0 \ (x::real); x < 1\ \ (\n. x ^ n) \ 0" proof cases assume "0 \ x" and "x \ 0" hence x0: "0 < x" by simp assume x1: "x < 1" from x0 x1 have "1 < inverse x" by (rule one_less_inverse) - hence "(\n. inverse (inverse x ^ n)) ----> 0" + hence "(\n. inverse (inverse x ^ n)) \ 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 \ (\n. x ^ n) ----> 0" + shows "norm x < 1 \ (\n. x ^ n) \ 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 \ (\n. a / (x ^ n) :: real) ----> 0" +lemma LIMSEQ_divide_realpow_zero: "1 < x \ (\n. a / (x ^ n) :: real) \ 0" by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp text\Limit of @{term "c^n"} for @{term"\c\ < 1"}\ -lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) ----> 0" +lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) \ 0" by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) -lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\n. c ^ n :: real) ----> 0" +lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\n. c ^ n :: real) \ 0" by (rule LIMSEQ_power_zero) simp @@ -2162,8 +2162,8 @@ subsection \Nested Intervals and Bisection -- Needed for Compactness\ lemma nested_sequence_unique: - assumes "\n. f n \ f (Suc n)" "\n. g (Suc n) \ g n" "\n. f n \ g n" "(\n. f n - g n) ----> 0" - shows "\l::real. ((\n. f n \ l) \ f ----> l) \ ((\n. l \ g n) \ g ----> l)" + assumes "\n. f n \ f (Suc n)" "\n. g (Suc n) \ g n" "\n. f n \ g n" "(\n. f n - g n) \ 0" + shows "\l::real. ((\n. f n \ l) \ f \ l) \ ((\n. l \ g n) \ g \ 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 \decseq g\ have "g n \ g 0" by (rule decseqD) simp with \\n. f n \ g n\[THEN spec, of n] have "f n \ g 0" by auto } - then obtain u where "f ----> u" "\i. f i \ u" + then obtain u where "f \ u" "\i. f i \ u" using incseq_convergent[OF \incseq f\] by auto moreover { fix n from \incseq f\ have "f 0 \ f n" by (rule incseqD) simp with \\n. f n \ g n\[THEN spec, of n] have "f 0 \ g n" by simp } - then obtain l where "g ----> l" "\i. l \ g i" + then obtain l where "g \ l" "\i. l \ g i" using decseq_convergent[OF \decseq g\] by auto - moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \f ----> u\ \g ----> l\]] + moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \f \ u\ \g \ l\]] ultimately show ?thesis by auto qed @@ -2198,14 +2198,14 @@ { fix n have "l n \ u n" by (induct n) auto } note this[simp] - have "\x. ((\n. l n \ x) \ l ----> x) \ ((\n. x \ u n) \ u ----> x)" + have "\x. ((\n. l n \ x) \ l \ x) \ ((\n. x \ u n) \ u \ x)" proof (safe intro!: nested_sequence_unique) fix n show "l n \ l (Suc n)" "u (Suc n) \ 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 "(\n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero) + then show "(\n. l n - u n) \ 0" by (simp add: LIMSEQ_divide_realpow_zero) qed fact - then obtain x where x: "\n. l n \ x" "\n. x \ u n" and "l ----> x" "u ----> x" by auto + then obtain x where x: "\n. l n \ x" "\n. x \ u n" and "l \ x" "u \ x" by auto obtain d where "0 < d" and d: "\a b. a \ x \ x \ b \ b - a < d \ P a b" using \l 0 \ x\ \x \ u 0\ local[of x] by auto @@ -2218,9 +2218,9 @@ qed (simp add: \\ P a b\) } moreover { have "eventually (\n. x - d / 2 < l n) sequentially" - using \0 < d\ \l ----> x\ by (intro order_tendstoD[of _ x]) auto + using \0 < d\ \l \ x\ by (intro order_tendstoD[of _ x]) auto moreover have "eventually (\n. u n < x + d / 2) sequentially" - using \0 < d\ \u ----> x\ by (intro order_tendstoD[of _ x]) auto + using \0 < d\ \u \ x\ by (intro order_tendstoD[of _ x]) auto ultimately have "eventually (\n. P (l n) (u n)) sequentially" proof eventually_elim fix n assume "x - d / 2 < l n" "u n < x + d / 2" diff -r e13e70f32407 -r e01015e49041 src/HOL/Metis_Examples/Clausification.thy --- 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 \ x" and 1: "f ----> lim f" + assumes fn_le: "!!n. f n \ x" and 1: "f \ lim f" shows "lim f \ x" by (metis 1 LIMSEQ_le_const2 fn_le) diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy --- 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: "\n. f n \ Abs_bcontfun ` (Pi I X \ bcontfun)" and lim: "f ----> l" + assume seq: "\n. f n \ Abs_bcontfun ` (Pi I X \ bcontfun)" and lim: "f \ l" have lim_fun: "\e>0. \N. \n\N. \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="\_. True", simplified]) @@ -156,7 +156,7 @@ by (auto simp: Abs_bcontfun_inverse) qed moreover note sequentially_bot - moreover have "(\n. Rep_bcontfun (f n) x) ----> Rep_bcontfun l x" + moreover have "(\n. Rep_bcontfun (f n) x) \ Rep_bcontfun l x" using lim_fun by (blast intro!: metric_LIMSEQ_I) ultimately show "Rep_bcontfun l x \ X x" by (rule Lim_in_closed_set) diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy --- 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 (\n. X n x)" . } - then obtain v where v: "\x. (\n. X n x) ----> v x" + then obtain v where v: "\x. (\n. X n x) \ 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: "(\n. norm (X n)) ----> K" + then obtain K where K: "(\n. norm (X n)) \ K" unfolding Cauchy_convergent_iff convergent_def by metis @@ -290,10 +290,10 @@ by (simp add: ac_simps) qed qed - hence Bv: "\x. (\n. X n x) ----> Blinfun v x" + hence Bv: "\x. (\n. X n x) \ Blinfun v x" by (auto simp: bounded_linear_Blinfun_apply v) - have "X ----> Blinfun v" + have "X \ Blinfun v" proof (rule LIMSEQ_I) fix r::real assume "r > 0" def r' \ "r / 2" @@ -320,7 +320,7 @@ using M[OF n elim] by (simp add: mult_right_mono) finally show ?case . qed - have tendsto_v: "(\m. norm (X n x - X m x)) ----> norm (X n x - Blinfun v x)" + have tendsto_v: "(\m. norm (X n x - X m x)) \ norm (X n x - Blinfun v x)" by (auto intro!: tendsto_intros Bv) show "norm ((X n - Blinfun v) x) \ r' * norm x" by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps) diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- 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 "\n. \x\s. (f n has_derivative (op * (f' n x))) (at x within s)" by (metis has_field_derivative_def df) - next show "(\n. f n x) ----> l" + next show "(\n. f n x) \ l" by (rule tf) next show "\e>0. \N. \n\N. \x\s. \h. cmod (f' n x * h - g' x * h) \ e * cmod h" by (blast intro: **) diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- 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 "\n>0. 3 \ n \ 1 \ ln (real_of_nat n)" using ln3_gt_1 by (force intro: order_trans [of _ "ln 3"] ln3_gt_1) - moreover have "(\n. cmod (Ln (of_nat n) / of_nat n powr s)) ----> 0" + moreover have "(\n. cmod (Ln (of_nat n) / of_nat n powr s)) \ 0" using lim_Ln_over_power [OF assms] by (metis tendsto_norm_zero_iff) ultimately show ?thesis diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Derivative.thy --- 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: "\x\s. (\n. f n x) ----> g x" .. + then obtain g where g: "\x\s. (\n. f n x) \ g x" .. have lem2: "\e>0. \N. \n\N. \x\s. \y\s. norm ((f n x - f n y) - (g x - g y)) \ e * norm (x - y)" proof (rule, rule) fix e :: real diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- 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 \ 'a ^ 'b" assume "Cauchy X" - have "\i. (\n. X n $ i) ----> lim (\n. X n $ i)" + have "\i. (\n. X n $ i) \ lim (\n. X n $ i)" using Cauchy_vec_nth [OF \Cauchy X\] by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - hence "X ----> vec_lambda (\i. lim (\n. X n $ i))" + hence "X \ vec_lambda (\i. lim (\n. X n $ i))" by (simp add: vec_tendstoI) then show "convergent X" by (rule convergentI) diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ s" using convergent_eq_cauchy[symmetric] by blast show ?thesis unfolding integrable_on_def has_integral @@ -10201,8 +10201,8 @@ fixes f :: "nat \ 'a::euclidean_space \ real" assumes f: "\k. (f k has_integral x k) s" assumes "\k x. x \ s \ f k x \ f (Suc k) x" - assumes "\x. x \ s \ (\k. f k x) ----> g x" - assumes "x ----> x'" + assumes "\x. x \ s \ (\k. f k x) \ g x" + assumes "x \ x'" shows "(g has_integral x') s" proof - have x_eq: "x = (\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 \ (\k. integral s (f k)) ----> integral s g" + have "g integrable_on s \ (\k. integral s (f k)) \ 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 _ \x ----> x'\]) (simp add: x_eq) + by (intro LIMSEQ_unique[OF _ \x \ x'\]) (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 \ j} \ Inf {f j x |j. Suc k \ j}" by (intro cInf_superset_mono) (auto simp: \x\s\) - show "(\k::nat. Inf {f j x |j. k \ j}) ----> g x" + show "(\k::nat. Inf {f j x |j. k \ j}) \ g x" proof (rule LIMSEQ_I, goal_cases) case r: (1 r) then have "0 'n::euclidean_space \ real" assumes "\k. (f k has_integral y k) s" "h integrable_on s" - "\k. \x\s. norm (f k x) \ h x" "\x\s. (\k. f k x) ----> g x" - and x: "y ----> x" + "\k. \x\s. norm (f k x) \ h x" "\x\s. (\k. f k x) \ g x" + and x: "y \ x" shows "(g has_integral x) s" proof - have int_f: "\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 "(\i. integral s (f i)) ----> x" + show "(\i. integral s (f i)) \ x" using integral_unique[OF assms(1)] x by simp - show "(\i. integral s (f i)) ----> integral s g" + show "(\i. integral s (f i)) \ integral s g" by (intro dominated_convergence[OF int_f assms(2)]) fact+ qed ultimately show ?thesis diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 \ s ----> l \ (s \ r) ----> l" +lemma lim_subseq: "subseq r \ s \ l \ (s \ r) \ l" by (rule LIMSEQ_subseq_LIMSEQ) lemma countable_PiE: @@ -2365,7 +2365,7 @@ lemma Lim_within_LIMSEQ: fixes a :: "'a::first_countable_topology" - assumes "\S. (\n. S n \ a \ S n \ T) \ S ----> a \ (\n. X (S n)) ----> L" + assumes "\S. (\n. S n \ a \ S n \ T) \ S \ a \ (\n. X (S n)) \ 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 \ S" "f n \ A n" "x \ f n" by auto } then have "\n. f n \ S - {x}" by auto - moreover have "(\n. f n) ----> x" + moreover have "(\n. f n) \ x" proof (rule topological_tendstoI) fix S assume "open S" "x \ S" @@ -2441,7 +2441,7 @@ ultimately show ?rhs by fast next assume ?rhs - then obtain f :: "nat \ 'a" where f: "\n. f n \ S - {x}" and lim: "f ----> x" + then obtain f :: "nat \ 'a" where f: "\n. f n \ S - {x}" and lim: "f \ 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: "\U. l\U \ open U \ infinite (U \ range f)" - shows "\r. subseq r \ (f \ r) ----> l" + shows "\r. subseq r \ (f \ r) \ 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 "(\n. f (r n)) ----> l" + have "(\n. f (r n)) \ l" proof (rule topological_tendstoI) fix S assume "open S" "l \ S" @@ -3560,7 +3560,7 @@ ultimately show "eventually (\i. f (r i) \ S) sequentially" by eventually_elim auto qed - ultimately show "\r. subseq r \ (f \ r) ----> l" + ultimately show "\r. subseq r \ (f \ r) \ 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 "\r. subseq r \ (f \ r) ----> l" + shows "\r. subseq r \ (f \ r) \ 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 "\n. f n \ s" and "f ----> l" + assumes "closed s" and "\n. f n \ s" and "f \ l" shows "l \ s" proof (rule ccontr) assume "l \ s" - with \closed s\ and \f ----> l\ have "eventually (\n. f n \ - s) sequentially" + with \closed s\ and \f \ l\ have "eventually (\n. f n \ - s) sequentially" by (fast intro: topological_tendstoD) with \\n. f n \ s\ show "False" by simp @@ -4005,13 +4005,13 @@ hence "\n. f n \ s" and "\n. f n \ t" by simp_all from \seq_compact s\ and \\n. f n \ s\ - obtain l r where "l \ s" and r: "subseq r" and l: "(f \ r) ----> l" + obtain l r where "l \ s" and r: "subseq r" and l: "(f \ r) \ l" by (rule seq_compactE) from \\n. f n \ t\ have "\n. (f \ r) n \ t" by simp from \closed t\ and this and l have "l \ t" by (rule closed_sequentially) - with \l \ s\ and r and l show "\l\s \ t. \r. subseq r \ (f \ r) ----> l" + with \l \ s\ and r and l show "\l\s \ t. \r. subseq r \ (f \ r) \ l" by fast qed @@ -4027,7 +4027,7 @@ proof (safe intro!: countably_compactI) fix A assume A: "\a\A. open a" "U \ \A" "countable A" - have subseq: "\X. range X \ U \ \r x. x \ U \ subseq r \ (X \ r) ----> x" + have subseq: "\X. range X \ U \ \r x. x \ U \ subseq r \ (X \ r) \ x" using \seq_compact U\ by (fastforce simp: seq_compact_def subset_eq) show "\T\A. finite T \ U \ \T" proof cases @@ -4048,7 +4048,7 @@ using \A \ {}\ unfolding X_def SUP_def by (intro T) (auto intro: from_nat_into) then have "range X \ U" by auto - with subseq[of X] obtain r x where "x \ U" and r: "subseq r" "(X \ r) ----> x" + with subseq[of X] obtain r x where "x \ U" and r: "subseq r" "(X \ r) \ x" by auto from \x\U\ \U \ \A\ from_nat_into_surj[OF \countable A\] obtain n where "x \ 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 "(\n. X (r n)) ----> x" + have "(\n. X (r n)) \ x" proof (rule topological_tendstoI) fix S assume "open S" "x \ S" @@ -4133,7 +4133,7 @@ ultimately show "eventually (\i. X (r i) \ S) sequentially" by eventually_elim auto qed - ultimately show "\x \ U. \r. subseq r \ (X \ r) ----> x" + ultimately show "\x \ U. \r. subseq r \ (X \ r) \ x" using \x \ U\ 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: "\n. f (r n) = f l" using infinite_enumerate by blast - then have "subseq r \ (f \ r) ----> f l" + then have "subseq r \ (f \ r) \ f l" by (simp add: fr o_def) - with f show "\l\s. \r. subseq r \ (f \ r) ----> l" + with f show "\l\s. \r. subseq r \ (f \ r) \ l" by auto next case False @@ -4326,7 +4326,7 @@ lemma compact_def: "compact (S :: 'a::metric_space set) \ - (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ (f \ r) ----> l))" + (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ (f \ r) \ l))" unfolding compact_eq_seq_compact_metric seq_compact_def by auto subsubsection \Complete the chain of compactness variants\ @@ -4405,7 +4405,7 @@ (* TODO: is this lemma necessary? *) lemma bounded_increasing_convergent: fixes s :: "nat \ real" - shows "bounded {s n| n. True} \ \n. s n \ s (Suc n) \ \l. s ----> l" + shows "bounded {s n| n. True} \ \n. s n \ s (Suc n) \ \l. s \ 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 \ r)" unfolding Bseq_eq_bounded using f by (force intro: bounded_subset) - with r show "\l r. subseq r \ (f \ r) ----> l" + with r show "\l r. subseq r \ (f \ r) \ l" using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def) qed @@ -4531,7 +4531,7 @@ by (rule bounded_fst) then have s1: "bounded (range (fst \ f))" by (simp add: image_comp) - obtain l1 r1 where r1: "subseq r1" and l1: "(\n. fst (f (r1 n))) ----> l1" + obtain l1 r1 where r1: "subseq r1" and l1: "(\n. fst (f (r1 n))) \ l1" using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast from f have s2: "bounded (range (snd \ f \ r1))" by (auto simp add: image_comp intro: bounded_snd bounded_subset) @@ -4551,16 +4551,16 @@ subsubsection \Completeness\ definition complete :: "'a::metric_space set \ bool" - where "complete s \ (\f. (\n. f n \ s) \ Cauchy f \ (\l\s. f ----> l))" + where "complete s \ (\f. (\n. f n \ s) \ Cauchy f \ (\l\s. f \ l))" lemma completeI: - assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f ----> l" + assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f \ l" shows "complete s" using assms unfolding complete_def by fast lemma completeE: assumes "complete s" and "\n. f n \ s" and "Cauchy f" - obtains l where "l \ s" and "f ----> l" + obtains l where "l \ s" and "f \ l" using assms unfolding complete_def by fast lemma compact_imp_complete: @@ -4570,7 +4570,7 @@ { fix f assume as: "(\n::nat. f n \ s)" "Cauchy f" - from as(1) obtain l r where lr: "l\s" "subseq r" "(f \ r) ----> l" + from as(1) obtain l r where lr: "l\s" "subseq r" "(f \ r) \ 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 "\l\s. \r. subseq r \ (f \ r) ----> l" + ultimately show "\l\s. \r. subseq r \ (f \ r) \ l" using assms unfolding complete_def by blast qed qed @@ -4789,19 +4789,19 @@ proof (rule completeI) fix f :: "nat \ 'a" assume "Cauchy f" then have "convergent f" by (rule Cauchy_convergent) - then show "\l\UNIV. f ----> l" unfolding convergent_def by simp + then show "\l\UNIV. f \ 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 "\n. f n \ s" and "f ----> x" - from \f ----> x\ have "Cauchy f" + fix f x assume "\n. f n \ s" and "f \ x" + from \f \ x\ have "Cauchy f" by (rule LIMSEQ_imp_Cauchy) - with \complete s\ and \\n. f n \ s\ obtain l where "l \ s" and "f ----> l" + with \complete s\ and \\n. f n \ s\ obtain l where "l \ s" and "f \ l" by (rule completeE) - from \f ----> x\ and \f ----> l\ have "x = l" + from \f \ x\ and \f \ l\ have "x = l" by (rule LIMSEQ_unique) with \l \ s\ show "x \ s" by simp @@ -4814,11 +4814,11 @@ fix f assume "\n. f n \ s \ t" and "Cauchy f" then have "\n. f n \ s" and "\n. f n \ t" by simp_all - from \complete s\ obtain l where "l \ s" and "f ----> l" + from \complete s\ obtain l where "l \ s" and "f \ l" using \\n. f n \ s\ and \Cauchy f\ by (rule completeE) - from \closed t\ and \\n. f n \ t\ and \f ----> l\ have "l \ t" + from \closed t\ and \\n. f n \ t\ and \f \ l\ have "l \ t" by (rule closed_sequentially) - with \l \ s\ and \f ----> l\ show "\l\s \ t. f ----> l" + with \l \ s\ and \f \ l\ show "\l\s \ t. f \ l" by fast qed @@ -4887,7 +4887,7 @@ using choice[of "\n x. x \ 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 \ s 0" "subseq r" "(x \ r) ----> l" + then obtain l r where lr: "l \ s 0" "subseq r" "(x \ r) \ l" using x and assms(3) unfolding seq_compact_def by blast have "\n. l \ s n" proof @@ -4898,7 +4898,7 @@ using x and assms(3) and lr(2) [THEN seq_suble] by auto then have "\i. (x \ r) (i + n) \ s n" using assms(3) by (fast intro!: le_add2) - moreover have "(\i. (x \ r) (i + n)) ----> l" + moreover have "(\i. (x \ r) (i + n)) \ l" using lr(3) by (rule LIMSEQ_ignore_initial_segment) ultimately show "l \ s n" by (rule closed_sequentially) @@ -5497,9 +5497,9 @@ } note le = this { fix x y - assume f: "(\n. dist (f (x n)) (f (y n))) ----> 0" - assume g: "(\n. dist (g (x n)) (g (y n))) ----> 0" - have "(\n. \dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\) ----> 0" + assume f: "(\n. dist (f (x n)) (f (y n))) \ 0" + assume g: "(\n. dist (g (x n)) (g (y n))) \ 0" + have "(\n. \dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\) \ 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 \ x) ----> (f x0)" + and "x \ x0" + shows "(f \ x) \ (f x0)" proof (rule topological_tendstoI) fix S assume "open S" "f x0 \ S" diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Uniform_Limit.thy --- 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 "\x\X. dist (f n x) (?f x) < e" proof fix x assume x: "x \ X" - with assms have "(\n. f n x) ----> ?f x" + with assms have "(\n. f n x) \ ?f x" by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff) with \e/2 > 0\ have "eventually (\m. m \ N \ dist (f m x) (?f x) < e/2) sequentially" by (intro tendstoD eventually_conj eventually_ge_at_top) diff -r e13e70f32407 -r e01015e49041 src/HOL/NSA/HSEQ.thy --- 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 \ L" shows "X ----NS> L" proof (rule NSLIMSEQ_I) fix N assume N: "N \ HNatInfinite" have "starfun X N - star_of L \ Infinitesimal" @@ -180,7 +180,7 @@ qed lemma NSLIMSEQ_LIMSEQ: - assumes X: "X ----NS> L" shows "X ----> L" + assumes X: "X ----NS> L" shows "X \ L" proof (rule LIMSEQ_I) fix r::real assume r: "0 < r" have "\no. \n\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 \ L) = (f ----NS> L)" by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ) subsubsection {* Derived theorems about @{term NSLIMSEQ} *} diff -r e13e70f32407 -r e01015e49041 src/HOL/NthRoot.thy --- 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: "(\n. root n n) ----> 1" +lemma LIMSEQ_root: "(\n. root n n) \ 1" proof - def x \ "\n. root n n - 1" - have "x ----> sqrt 0" + have "x \ sqrt 0" proof (rule tendsto_sandwich[OF _ _ tendsto_const]) - show "(\x. sqrt (2 / x)) ----> sqrt 0" + show "(\x. sqrt (2 / x)) \ 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 "(\n. root n c) ----> 1" + shows "(\n. root n c) \ 1" proof - { fix c :: real assume "1 \ c" def x \ "\n. root n c - 1" - have "x ----> 0" + have "x \ 0" proof (rule tendsto_sandwich[OF _ _ tendsto_const]) - show "(\n. c / n) ----> 0" + show "(\n. c / n) \ 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 (\n. 0 \ x n) sequentially" using \1 \ c\ 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 "(\n. root n c) ----> 1" + from tendsto_add[OF this tendsto_const[of 1]] have "(\n. root n c) \ 1" by (simp add: x_def) } note ge_1 = this @@ -724,7 +724,7 @@ assume "\ 1 \ c" with \0 < c\ have "1 \ 1 / c" by simp - then have "(\n. 1 / root n (1 / c)) ----> 1 / 1" + then have "(\n. 1 / root n (1 / c)) \ 1 / 1" by (intro tendsto_divide tendsto_const ge_1 \1 \ 1 / c\ one_neq_zero) then show ?thesis by (rule filterlim_cong[THEN iffD1, rotated 3]) diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Bochner_Integration.thy --- 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 \ 'b :: {metric_space, second_countable_topology}" assumes [measurable]: "f \ borel_measurable M" - shows "\F. (\i. simple_function M (F i)) \ (\x\space M. (\i. F i x) ----> f x) \ + shows "\F. (\i. simple_function M (F i)) \ (\x\space M. (\i. F i x) \ f x) \ (\i. \x\space M. dist (F i x) z \ 2 * dist (f x) z)" proof - obtain D :: "'b set" where "countable D" and D: "\X. open X \ X \ {} \ \d\D. d \ X" @@ -101,7 +101,7 @@ note * = this fix x assume "x \ space M" - show "(\i. F i x) ----> f x" + show "(\i. F i x) \ f x" proof cases assume "f x = z" then have "\i n. x \ A i n" @@ -173,7 +173,7 @@ assumes set: "\A. A \ sets M \ P (indicator A)" assumes mult: "\u c. 0 \ c \ u \ borel_measurable M \ (\x. 0 \ u x) \ P u \ P (\x. c * u x)" assumes add: "\u v. u \ borel_measurable M \ (\x. 0 \ u x) \ P u \ v \ borel_measurable M \ (\x. 0 \ v x) \ (\x. x \ space M \ u x = 0 \ v x = 0) \ P v \ P (\x. v x + u x)" - assumes seq: "\U. (\i. U i \ borel_measurable M) \ (\i x. 0 \ U i x) \ (\i. P (U i)) \ incseq U \ (\x. x \ space M \ (\i. U i x) ----> u x) \ P u" + assumes seq: "\U. (\i. U i \ borel_measurable M) \ (\i x. 0 \ U i x) \ (\i. P (U i)) \ incseq U \ (\x. x \ space M \ (\i. U i x) \ u x) \ P u" shows "P u" proof - have "(\x. ereal (u x)) \ borel_measurable M" using u by auto @@ -199,13 +199,13 @@ intro!: real_of_ereal_positive_mono) next fix x assume x: "x \ space M" - have "(\i. U i x) ----> (SUP i. U i x)" + have "(\i. U i x) \ (SUP i. U i x)" using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def) moreover have "(\i. U i x) = (\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 "(\i. U' i x) ----> u x" + ultimately show "(\i. U' i x) \ u x" by simp next fix i @@ -516,8 +516,8 @@ for M f x where "f \ borel_measurable M \ (\i. simple_bochner_integrable M (s i)) \ - (\i. \\<^sup>+x. norm (f x - s i x) \M) ----> 0 \ - (\i. simple_bochner_integral M (s i)) ----> x \ + (\i. \\<^sup>+x. norm (f x - s i x) \M) \ 0 \ + (\i. simple_bochner_integral M (s i)) \ x \ has_bochner_integral M f x" lemma has_bochner_integral_cong: @@ -530,7 +530,7 @@ "f \ borel_measurable M \ g \ borel_measurable M \ (AE x in M. f x = g x) \ has_bochner_integral M f x \ 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="\x. x ----> 0"] + by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\x. x \ 0"] nn_integral_cong_AE) auto @@ -572,8 +572,8 @@ has_bochner_integral M (\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: "(\i. \\<^sup>+ x. norm (f x - sf i x) \M) ----> 0" - assume g_sg: "(\i. \\<^sup>+ x. norm (g x - sg i x) \M) ----> 0" + assume f_sf: "(\i. \\<^sup>+ x. norm (f x - sf i x) \M) \ 0" + assume g_sg: "(\i. \\<^sup>+ x. norm (g x - sg i x) \M) \ 0" assume sf: "\i. simple_bochner_integrable M (sf i)" and sg: "\i. simple_bochner_integrable M (sg i)" @@ -584,10 +584,10 @@ show "\i. simple_bochner_integrable M (\x. sf i x + sg i x)" using sf sg by (simp add: simple_bochner_integrable_compose2) - show "(\i. \\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \M) ----> 0" - (is "?f ----> 0") + show "(\i. \\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \M) \ 0" + (is "?f \ 0") proof (rule tendsto_sandwich) - show "eventually (\n. 0 \ ?f n) sequentially" "(\_. 0) ----> 0" + show "eventually (\n. 0 \ ?f n) sequentially" "(\_. 0) \ 0" by (auto simp: nn_integral_nonneg) show "eventually (\i. ?f i \ (\\<^sup>+ x. (norm (f x - sf i x)) \M) + \\<^sup>+ x. (norm (g x - sg i x)) \M) sequentially" (is "eventually (\i. ?f i \ ?g i) sequentially") @@ -598,7 +598,7 @@ by (intro nn_integral_add) auto finally show "?f i \ ?g i" . qed - show "?g ----> 0" + show "?g \ 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 "(\x. T (f x)) \ borel_measurable M" by auto - fix s assume f_s: "(\i. \\<^sup>+ x. norm (f x - s i x) \M) ----> 0" + fix s assume f_s: "(\i. \\<^sup>+ x. norm (f x - s i x) \M) \ 0" assume s: "\i. simple_bochner_integrable M (s i)" then show "\i. simple_bochner_integrable M (\x. T (s i x))" by (auto intro: simple_bochner_integrable_compose2 T.zero) @@ -625,10 +625,10 @@ obtain K where K: "K > 0" "\x i. norm (T (f x) - T (s i x)) \ norm (f x - s i x) * K" using T.pos_bounded by (auto simp: T.diff[symmetric]) - show "(\i. \\<^sup>+ x. norm (T (f x) - T (s i x)) \M) ----> 0" - (is "?f ----> 0") + show "(\i. \\<^sup>+ x. norm (T (f x) - T (s i x)) \M) \ 0" + (is "?f \ 0") proof (rule tendsto_sandwich) - show "eventually (\n. 0 \ ?f n) sequentially" "(\_. 0) ----> 0" + show "eventually (\n. 0 \ ?f n) sequentially" "(\_. 0) \ 0" by (auto simp: nn_integral_nonneg) show "eventually (\i. ?f i \ K * (\\<^sup>+ x. norm (f x - s i x) \M)) sequentially" @@ -640,12 +640,12 @@ using K by (intro nn_integral_cmult) auto finally show "?f i \ ?g i" . qed - show "?g ----> 0" + show "?g \ 0" using tendsto_cmult_ereal[OF _ f_s, of "ereal K"] by simp qed - assume "(\i. simple_bochner_integral M (s i)) ----> x" - with s show "(\i. simple_bochner_integral M (\x. T (s i x))) ----> T x" + assume "(\i. simple_bochner_integral M (s i)) \ x" + with s show "(\i. simple_bochner_integral M (\x. T (s i x))) \ 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 \ borel_measurable M" and s: "\i. simple_bochner_integrable M (s i)" and - lim_0: "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) ----> 0" + lim_0: "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) \ 0" from order_tendstoD[OF lim_0, of "\"] obtain i where f_s_fin: "(\\<^sup>+ x. ereal (norm (f x - s i x)) \M) < \" by (metis (mono_tags, lifting) eventually_False_sequentially eventually_mono @@ -760,9 +760,9 @@ shows "norm x \ (\\<^sup>+x. norm (f x) \M)" using assms proof fix s assume - x: "(\i. simple_bochner_integral M (s i)) ----> x" (is "?s ----> x") and + x: "(\i. simple_bochner_integral M (s i)) \ x" (is "?s \ x") and s[simp]: "\i. simple_bochner_integrable M (s i)" and - lim: "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) ----> 0" and + lim: "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) \ 0" and f[measurable]: "f \ borel_measurable M" have [measurable]: "\i. s i \ borel_measurable M" @@ -770,7 +770,7 @@ show "norm x \ (\\<^sup>+x. norm (f x) \M)" proof (rule LIMSEQ_le) - show "(\i. ereal (norm (?s i))) ----> norm x" + show "(\i. ereal (norm (?s i))) \ norm x" using x by (intro tendsto_intros lim_ereal[THEN iffD2]) show "\N. \n\N. norm (?s n) \ (\\<^sup>+x. norm (f x - s n x) \M) + (\\<^sup>+x. norm (f x) \M)" (is "\N. \n\N. _ \ ?t n") @@ -788,10 +788,10 @@ by (rule nn_integral_add) auto finally show "norm (?s n) \ ?t n" . qed - have "?t ----> 0 + (\\<^sup>+ x. ereal (norm (f x)) \M)" + have "?t \ 0 + (\\<^sup>+ x. ereal (norm (f x)) \M)" using has_bochner_integral_implies_finite_norm[OF i] by (intro tendsto_add_ereal tendsto_const lim) auto - then show "?t ----> \\<^sup>+ x. ereal (norm (f x)) \M" + then show "?t \ \\<^sup>+ x. ereal (norm (f x)) \M" by simp qed qed @@ -802,8 +802,8 @@ assume f[measurable]: "f \ borel_measurable M" fix s t - assume "(\i. \\<^sup>+ x. norm (f x - s i x) \M) ----> 0" (is "?S ----> 0") - assume "(\i. \\<^sup>+ x. norm (f x - t i x) \M) ----> 0" (is "?T ----> 0") + assume "(\i. \\<^sup>+ x. norm (f x - s i x) \M) \ 0" (is "?S \ 0") + assume "(\i. \\<^sup>+ x. norm (f x - t i x) \M) \ 0" (is "?T \ 0") assume s: "\i. simple_bochner_integrable M (s i)" assume t: "\i. simple_bochner_integrable M (t i)" @@ -812,22 +812,22 @@ let ?s = "\i. simple_bochner_integral M (s i)" let ?t = "\i. simple_bochner_integral M (t i)" - assume "?s ----> x" "?t ----> y" - then have "(\i. norm (?s i - ?t i)) ----> norm (x - y)" + assume "?s \ x" "?t \ y" + then have "(\i. norm (?s i - ?t i)) \ norm (x - y)" by (intro tendsto_intros) moreover - have "(\i. ereal (norm (?s i - ?t i))) ----> ereal 0" + have "(\i. ereal (norm (?s i - ?t i))) \ ereal 0" proof (rule tendsto_sandwich) - show "eventually (\i. 0 \ ereal (norm (?s i - ?t i))) sequentially" "(\_. 0) ----> ereal 0" + show "eventually (\i. 0 \ ereal (norm (?s i - ?t i))) sequentially" "(\_. 0) \ ereal 0" by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric]) show "eventually (\i. norm (?s i - ?t i) \ ?S i + ?T i) sequentially" by (intro always_eventually allI simple_bochner_integral_bounded s t f) - show "(\i. ?S i + ?T i) ----> ereal 0" - using tendsto_add_ereal[OF _ _ \?S ----> 0\ \?T ----> 0\] + show "(\i. ?S i + ?T i) \ ereal 0" + using tendsto_add_ereal[OF _ _ \?S \ 0\ \?T \ 0\] by (simp add: zero_ereal_def[symmetric]) qed - then have "(\i. norm (?s i - ?t i)) ----> 0" + then have "(\i. norm (?s i - ?t i)) \ 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 "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) ----> 0" + fix s assume "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) \ 0" also have "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) = (\i. \\<^sup>+ x. ereal (norm (g x - s i x)) \M)" using ae by (intro ext nn_integral_cong_AE, eventually_elim) simp - finally show "(\i. \\<^sup>+ x. ereal (norm (g x - s i x)) \M) ----> 0" . + finally show "(\i. \\<^sup>+ x. ereal (norm (g x - s i x)) \M) \ 0" . qed (auto intro: g) lemma has_bochner_integral_eq_AE: @@ -1144,12 +1144,12 @@ fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes f[measurable]: "f \ borel_measurable M" assumes s: "\i. simple_bochner_integrable M (s i)" - assumes lim: "(\i. \\<^sup>+x. norm (f x - s i x) \M) ----> 0" (is "?S ----> 0") + assumes lim: "(\i. \\<^sup>+x. norm (f x - s i x) \M) \ 0" (is "?S \ 0") shows "integrable M f" proof - let ?s = "\n. simple_bochner_integral M (s n)" - have "\x. ?s ----> x" + have "\x. ?s \ 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 \ x" .. show ?thesis by (rule, rule) fact+ qed @@ -1183,14 +1183,14 @@ "\i. u i \ borel_measurable M" "u' \ borel_measurable M" "w \ borel_measurable M" and bound: "\j. AE x in M. norm (u j x) \ w x" and w: "(\\<^sup>+x. w x \M) < \" - and u': "AE x in M. (\i. u i x) ----> u' x" - shows "(\i. (\\<^sup>+x. norm (u' x - u i x) \M)) ----> 0" + and u': "AE x in M. (\i. u i x) \ u' x" + shows "(\i. (\\<^sup>+x. norm (u' x - u i x) \M)) \ 0" proof - have "AE x in M. \j. norm (u j x) \ w x" unfolding AE_all_countable by rule fact with u' have bnd: "AE x in M. \j. norm (u' x - u j x) \ 2 * w x" proof (eventually_elim, intro allI) - fix i x assume "(\i. u i x) ----> u' x" "\j. norm (u j x) \ w x" "\j. norm (u j x) \ w x" + fix i x assume "(\i. u i x) \ u' x" "\j. norm (u j x) \ w x" "\j. norm (u j x) \ w x" then have "norm (u' x) \ w x" "norm (u i x) \ w x" by (auto intro: LIMSEQ_le_const2 tendsto_norm) then have "norm (u' x) + norm (u i x) \ 2 * w x" @@ -1200,16 +1200,16 @@ finally (xtrans) show "norm (u' x - u i x) \ 2 * w x" . qed - have "(\i. (\\<^sup>+x. norm (u' x - u i x) \M)) ----> (\\<^sup>+x. 0 \M)" + have "(\i. (\\<^sup>+x. norm (u' x - u i x) \M)) \ (\\<^sup>+x. 0 \M)" proof (rule nn_integral_dominated_convergence) show "(\\<^sup>+x. 2 * w x \M) < \" by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto - show "AE x in M. (\i. ereal (norm (u' x - u i x))) ----> 0" + show "AE x in M. (\i. ereal (norm (u' x - u i x))) \ 0" using u' proof eventually_elim - fix x assume "(\i. u i x) ----> u' x" + fix x assume "(\i. u i x) \ u' x" from tendsto_diff[OF tendsto_const[of "u' x"] this] - show "(\i. ereal (norm (u' x - u i x))) ----> 0" + show "(\i. ereal (norm (u' x - u i x))) \ 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: "\i. simple_function M (s i)" and - pointwise: "\x. x \ space M \ (\i. s i x) ----> f x" and + pointwise: "\x. x \ space M \ (\i. s i x) \ f x" and bound: "\i x. x \ space M \ norm (s i x) \ 2 * norm (f x)" by (simp add: norm_conv_dist) metis @@ -1241,7 +1241,7 @@ show "\i. simple_bochner_integrable M (s i)" by (rule simple_bochner_integrableI_bounded) fact+ - show "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) ----> 0" + show "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) \ 0" proof (rule nn_integral_dominated_convergence_norm) show "\j. AE x in M. norm (s j x) \ 2 * norm (f x)" using bound by auto @@ -1249,7 +1249,7 @@ using s by (auto intro: borel_measurable_simple_function) show "(\\<^sup>+ x. ereal (2 * norm (f x)) \M) < \" using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto - show "AE x in M. (\i. s i x) ----> f x" + show "AE x in M. (\i. s i x) \ f x" using pointwise by auto qed fact qed fact @@ -1456,11 +1456,11 @@ lemma fixes f :: "'a \ 'b::{banach, second_countable_topology}" and w :: "'a \ real" assumes "f \ borel_measurable M" "\i. s i \ borel_measurable M" "integrable M w" - assumes lim: "AE x in M. (\i. s i x) ----> f x" + assumes lim: "AE x in M. (\i. s i x) \ f x" assumes bound: "\i. AE x in M. norm (s i x) \ w x" shows integrable_dominated_convergence: "integrable M f" and integrable_dominated_convergence2: "\i. integrable M (s i)" - and integral_dominated_convergence: "(\i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f" + and integral_dominated_convergence: "(\i. integral\<^sup>L M (s i)) \ integral\<^sup>L M f" proof - have "AE x in M. 0 \ w x" using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans) @@ -1487,16 +1487,16 @@ have "(\\<^sup>+ x. ereal (norm (f x)) \M) \ (\\<^sup>+x. w x \M)" using all_bound lim proof (intro nn_integral_mono_AE, eventually_elim) - fix x assume "\i. norm (s i x) \ w x" "(\i. s i x) ----> f x" + fix x assume "\i. norm (s i x) \ w x" "(\i. s i x) \ f x" then show "ereal (norm (f x)) \ ereal (w x)" by (intro LIMSEQ_le_const2[where X="\i. ereal (norm (s i x))"] tendsto_intros lim_ereal[THEN iffD2]) auto qed with w show "(\\<^sup>+ x. ereal (norm (f x)) \M) < \" by auto qed fact - have "(\n. ereal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) ----> ereal 0" (is "?d ----> ereal 0") + have "(\n. ereal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) \ ereal 0" (is "?d \ ereal 0") proof (rule tendsto_sandwich) - show "eventually (\n. ereal 0 \ ?d n) sequentially" "(\_. ereal 0) ----> ereal 0" by auto + show "eventually (\n. ereal 0 \ ?d n) sequentially" "(\_. ereal 0) \ ereal 0" by auto show "eventually (\n. ?d n \ (\\<^sup>+x. norm (s n x - f x) \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 \ (\\<^sup>+x. norm (s n x - f x) \M)" . qed - show "(\n. \\<^sup>+x. norm (s n x - f x) \M) ----> ereal 0" + show "(\n. \\<^sup>+x. norm (s n x - f x) \M) \ 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 "(\n. integral\<^sup>L M (s n) - integral\<^sup>L M f) ----> 0" + then have "(\n. integral\<^sup>L M (s n) - integral\<^sup>L M f) \ 0" unfolding lim_ereal tendsto_norm_zero_iff . from tendsto_add[OF this tendsto_const[of "integral\<^sup>L M f"]] - show "(\i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f" by simp + show "(\i. integral\<^sup>L M (s i)) \ integral\<^sup>L M f" by simp qed context @@ -1535,15 +1535,15 @@ obtain N where w: "\n. N \ n \ AE x in M. norm (s (X n) x) \ w x" by (auto simp: eventually_sequentially) - show "(\n. integral\<^sup>L M (s (X n))) ----> integral\<^sup>L M f" + show "(\n. integral\<^sup>L M (s (X n))) \ integral\<^sup>L M f" proof (rule LIMSEQ_offset, rule integral_dominated_convergence) show "AE x in M. norm (s (X (n + N)) x) \ w x" for n by (rule w) auto - show "AE x in M. (\n. s (X (n + N)) x) ----> f x" + show "AE x in M. (\n. s (X (n + N)) x) \ f x" using lim proof eventually_elim fix x assume "((\i. s i x) ---> f x) at_top" - then show "(\n. s (X (n + N)) x) ----> f x" + then show "(\n. s (X (n + N)) x) \ 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) \ w x" for i :: nat by (intro w) auto - show "AE x in M. (\i. s (N + real i) x) ----> f x" + show "AE x in M. (\i. s (N + real i) x) \ f x" using lim proof eventually_elim fix x assume "((\i. s i x) ---> f x) at_top" - then show "(\n. s (N + n) x) ----> f x" + then show "(\n. s (N + n) x) \ 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 "(\i. ereal (integral\<^sup>L M (s i))) ----> ereal (integral\<^sup>L M f)" + show "(\i. ereal (integral\<^sup>L M (s i))) \ 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: "\i. integrable M (s i)" using seq f s_le_f by (intro integrable_bound[OF f(3)]) auto - have "(\i. \\<^sup>+ x. s i x \M) ----> \\<^sup>+ x. f x \M" + have "(\i. \\<^sup>+ x. s i x \M) \ \\<^sup>+ x. f x \M" using seq s_le_f f by (intro nn_integral_dominated_convergence[where w=f]) (auto simp: integrable_iff_bounded) also have "(\i. \\<^sup>+x. s i x \M) = (\i. \x. s i x \M)" using seq int_s by simp - finally show "(\i. \x. s i x \M) ----> \\<^sup>+x. f x \M" + finally show "(\i. \x. s i x \M) \ \\<^sup>+x. f x \M" by simp qed qed } @@ -1660,7 +1660,7 @@ by (simp add: suminf_ereal' sums) qed simp - have 2: "AE x in M. (\n. \i (\i. f i x)" + have 2: "AE x in M. (\n. \i (\i. f i x)" using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel) have 3: "\j. AE x in M. norm (\i (\i. norm (f i x))" @@ -1742,14 +1742,14 @@ assumes base: "\A c. A \ sets M \ emeasure M A < \ \ P (\x. indicator A x *\<^sub>R c)" assumes add: "\f g. integrable M f \ P f \ integrable M g \ P g \ P (\x. f x + g x)" assumes lim: "\f s. (\i. integrable M (s i)) \ (\i. P (s i)) \ - (\x. x \ space M \ (\i. s i x) ----> f x) \ + (\x. x \ space M \ (\i. s i x) \ f x) \ (\i x. x \ space M \ norm (s i x) \ 2 * norm (f x)) \ integrable M f \ P f" shows "P f" proof - from \integrable M f\ have f: "f \ borel_measurable M" "(\\<^sup>+x. norm (f x) \M) < \" unfolding integrable_iff_bounded by auto from borel_measurable_implies_sequence_metric[OF f(1)] - obtain s where s: "\i. simple_function M (s i)" "\x. x \ space M \ (\i. s i x) ----> f x" + obtain s where s: "\i. simple_function M (s i)" "\x. x \ space M \ (\i. s i x) \ f x" "\i x. x \ space M \ norm (s i x) \ 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 \ space M" with s show "(\i. s' i x) ----> f x" + fix x assume "x \ space M" with s show "(\i. s' i x) \ f x" by (simp add: s'_eq_s) show "norm (s' i x) \ 2 * norm (f x)" using \x \ space M\ s by (simp add: s'_eq_s) @@ -1923,10 +1923,10 @@ case (lim f s) show ?case proof (rule LIMSEQ_unique) - show "(\i. integral\<^sup>L (restrict_space M \) (s i)) ----> integral\<^sup>L (restrict_space M \) f" + show "(\i. integral\<^sup>L (restrict_space M \) (s i)) \ integral\<^sup>L (restrict_space M \) f" using lim by (intro integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) simp_all - show "(\i. integral\<^sup>L (restrict_space M \) (s i)) ----> (\ x. indicator \ x *\<^sub>R f x \M)" + show "(\i. integral\<^sup>L (restrict_space M \) (s i)) \ (\ x. indicator \ x *\<^sub>R f x \M)" unfolding lim using lim by (intro integral_dominated_convergence[where w="\x. 2 * norm (indicator \ x *\<^sub>R f x)"]) @@ -1998,16 +1998,16 @@ show ?case proof (rule LIMSEQ_unique) - show "(\i. integral\<^sup>L M (\x. g x *\<^sub>R s i x)) ----> integral\<^sup>L M (\x. g x *\<^sub>R f x)" + show "(\i. integral\<^sup>L M (\x. g x *\<^sub>R s i x)) \ integral\<^sup>L M (\x. g x *\<^sub>R f x)" proof (rule integral_dominated_convergence) show "integrable M (\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. (\i. g x *\<^sub>R s i x) ----> g x *\<^sub>R f x" + show "AE x in M. (\i. g x *\<^sub>R s i x) \ g x *\<^sub>R f x" using lim(3) by (auto intro!: tendsto_scaleR AE_I2[of M]) show "\i. AE x in M. norm (g x *\<^sub>R s i x) \ 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 "(\i. integral\<^sup>L M (\x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f" + show "(\i. integral\<^sup>L M (\x. g x *\<^sub>R s i x)) \ integral\<^sup>L (density M g) f" unfolding lim(2)[symmetric] by (rule integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) (insert lim(3-5), auto) @@ -2077,16 +2077,16 @@ show ?case proof (rule LIMSEQ_unique) - show "(\i. integral\<^sup>L M (\x. s i (g x))) ----> integral\<^sup>L M (\x. f (g x))" + show "(\i. integral\<^sup>L M (\x. s i (g x))) \ integral\<^sup>L M (\x. f (g x))" proof (rule integral_dominated_convergence) show "integrable M (\x. 2 * norm (f (g x)))" using lim by (auto simp: integrable_distr_eq) - show "AE x in M. (\i. s i (g x)) ----> f (g x)" + show "AE x in M. (\i. s i (g x)) \ f (g x)" using lim(3) g[THEN measurable_space] by auto show "\i. AE x in M. norm (s i (g x)) \ 2 * norm (f (g x))" using lim(4) g[THEN measurable_space] by auto qed auto - show "(\i. integral\<^sup>L M (\x. s i (g x))) ----> integral\<^sup>L (distr M N g) f" + show "(\i. integral\<^sup>L M (\x. s i (g x))) \ integral\<^sup>L (distr M N g) f" unfolding lim(2)[symmetric] by (rule integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) (insert lim(3-5), auto) @@ -2266,8 +2266,8 @@ fixes f :: "nat \ 'a \ real" assumes i: "\i. integrable M (f i)" and mono: "AE x in M. mono (\n. f n x)" and pos: "\i. AE x in M. 0 \ f i x" - and lim: "AE x in M. (\i. f i x) ----> u x" - and ilim: "(\i. integral\<^sup>L M (f i)) ----> x" + and lim: "AE x in M. (\i. f i x) \ u x" + and ilim: "(\i. integral\<^sup>L M (f i)) \ x" and u: "u \ 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) \ 0" proof eventually_elim - fix x assume "mono (\n. f n x)" "0 \ f 0 x" "(\i. f i x) ----> u x" + fix x assume "mono (\n. f n x)" "0 \ f 0 x" "(\i. f i x) \ u x" then show "ereal (- u x) \ 0" using incseq_le[of "\n. f n x" "u x" 0] by (simp add: mono_def incseq_def) qed @@ -2307,8 +2307,8 @@ lemma fixes f :: "nat \ 'a \ real" assumes f: "\i. integrable M (f i)" and mono: "AE x in M. mono (\n. f n x)" - and lim: "AE x in M. (\i. f i x) ----> u x" - and ilim: "(\i. integral\<^sup>L M (f i)) ----> x" + and lim: "AE x in M. (\i. f i x) \ u x" + and ilim: "(\i. integral\<^sup>L M (f i)) \ x" and u: "u \ 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: "\n. AE x in M. 0 \ f n x - f 0 x" using mono by (auto simp: field_simps mono_def le_fun_def) - have 4: "AE x in M. (\i. f i x - f 0 x) ----> u x - f 0 x" + have 4: "AE x in M. (\i. f i x - f 0 x) \ u x - f 0 x" using lim by (auto intro!: tendsto_diff) - have 5: "(\i. (\x. f i x - f 0 x \M)) ----> x - integral\<^sup>L M (f 0)" + have 5: "(\i. (\x. f i x - f 0 x \M)) \ x - integral\<^sup>L M (f 0)" using f ilim by (auto intro!: tendsto_diff) have 6: "(\x. u x - f 0 x) \ borel_measurable M" using f[of 0] u by auto @@ -2462,17 +2462,17 @@ shows "((\y. \ x. indicator {.. y} x *\<^sub>R f x \M) ---> \ x. f x \M) at_top" proof (rule tendsto_at_topI_sequentially) fix X :: "nat \ real" assume "filterlim X at_top sequentially" - show "(\n. \x. indicator {..X n} x *\<^sub>R f x \M) ----> integral\<^sup>L M f" + show "(\n. \x. indicator {..X n} x *\<^sub>R f x \M) \ integral\<^sup>L M f" proof (rule integral_dominated_convergence) show "integrable M (\x. norm (f x))" by (rule integrable_norm) fact - show "AE x in M. (\n. indicator {..X n} x *\<^sub>R f x) ----> f x" + show "AE x in M. (\n. indicator {..X n} x *\<^sub>R f x) \ f x" proof fix x from \filterlim X at_top sequentially\ have "eventually (\n. x \ X n) sequentially" unfolding filterlim_at_top_ge[where c=x] by auto - then show "(\n. indicator {..X n} x *\<^sub>R f x) ----> f x" + then show "(\n. indicator {..X n} x *\<^sub>R f x) \ 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) \ norm (f x)" @@ -2497,9 +2497,9 @@ by (rule eventually_sequentiallyI[of "nat \x\"]) (auto split: split_indicator simp: nat_le_iff ceiling_le_iff) } from filterlim_cong[OF refl refl this] - have "AE x in M. (\i. f x * indicator {..real i} x) ----> f x" + have "AE x in M. (\i. f x * indicator {..real i} x) \ f x" by simp - have "(\i. \ x. f x * indicator {..real i} x \M) ----> x" + have "(\i. \ x. f x * indicator {..real i} x \M) \ 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: "\i. simple_function (N \\<^sub>M M) (s i)" - "\x y. x \ space N \ y \ space M \ (\i. s i (x, y)) ----> f x y" + "\x y. x \ space N \ y \ space M \ (\i. s i (x, y)) \ f x y" "\i x y. x \ space N \ y \ space M \ norm (s i (x, y)) \ 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 (\y. 2 * norm (f x y))" by (intro integrable_norm integrable_mult_right int_f) - have "(\i. integral\<^sup>L M (\y. s i (x, y))) ----> integral\<^sup>L M (f x)" + have "(\i. integral\<^sup>L M (\y. s i (x, y))) \ integral\<^sup>L M (f x)" proof (rule integral_dominated_convergence) from int_f show "f x \ borel_measurable M" by auto show "\i. (\y. s i (x, y)) \ borel_measurable M" using x by simp - show "AE xa in M. (\i. s i (x, xa)) ----> f x xa" + show "AE xa in M. (\i. s i (x, xa)) \ f x xa" using x s(2) by auto show "\i. AE xa in M. norm (s i (x, xa)) \ 2 * norm (f x xa)" using x s(3) by auto @@ -2597,10 +2597,10 @@ qed then have "integral\<^sup>L M (\y. s i (x, y)) = simple_bochner_integral M (\y. s i (x, y))" by (rule simple_bochner_integrable_eq_integral[symmetric]) } - ultimately have "(\i. simple_bochner_integral M (\y. s i (x, y))) ----> integral\<^sup>L M (f x)" + ultimately have "(\i. simple_bochner_integral M (\y. s i (x, y))) \ integral\<^sup>L M (f x)" by simp } then - show "(\i. f' i x) ----> integral\<^sup>L M (f x)" + show "(\i. f' i x) \ 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 "(\i. integral\<^sup>L (M1 \\<^sub>M M2) (s i)) ----> integral\<^sup>L (M1 \\<^sub>M M2) f" + show "(\i. integral\<^sup>L (M1 \\<^sub>M M2) (s i)) \ integral\<^sup>L (M1 \\<^sub>M M2) f" proof (rule integral_dominated_convergence) show "integrable (M1 \\<^sub>M M2) (\x. 2 * norm (f x))" using lim(5) by auto qed (insert lim, auto) - have "(\i. \ x. \ y. s i (x, y) \M2 \M1) ----> \ x. \ y. f (x, y) \M2 \M1" + have "(\i. \ x. \ y. s i (x, y) \M2 \M1) \ \ x. \ y. f (x, y) \M2 \M1" proof (rule integral_dominated_convergence) have "AE x in M1. \i. integrable M2 (\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. (\i. \ y. s i (x, y) \M2) ----> \ y. f (x, y) \M2" + show "AE x in M1. (\i. \ y. s i (x, y) \M2) \ \ y. f (x, y) \M2" proof eventually_elim fix x assume x: "x \ space M1" and s: "\i. integrable M2 (\y. s i (x, y))" and f: "integrable M2 (\y. f (x, y))" - show "(\i. \ y. s i (x, y) \M2) ----> \ y. f (x, y) \M2" + show "(\i. \ y. s i (x, y) \M2) \ \ y. f (x, y) \M2" proof (rule integral_dominated_convergence) show "integrable M2 (\y. 2 * norm (f (x, y)))" using f by auto - show "AE xa in M2. (\i. s i (x, xa)) ----> f (x, xa)" + show "AE xa in M2. (\i. s i (x, xa)) \ f (x, xa)" using x lim(3) by (auto simp: space_pair_measure) show "\i. AE xa in M2. norm (s i (x, xa)) \ 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 "(\i. integral\<^sup>L (M1 \\<^sub>M M2) (s i)) ----> \ x. \ y. f (x, y) \M2 \M1" + then show "(\i. integral\<^sup>L (M1 \\<^sub>M M2) (s i)) \ \ x. \ y. f (x, y) \M2 \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 "(\i. integral\<^sup>L N (s i)) ----> integral\<^sup>L N f" + show "(\i. integral\<^sup>L N (s i)) \ integral\<^sup>L N f" apply (rule integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) using lim apply auto done - show "(\i. integral\<^sup>L N (s i)) ----> integral\<^sup>L M f" + show "(\i. integral\<^sup>L N (s i)) \ integral\<^sup>L M f" unfolding lim apply (rule integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) using lim M N(2) diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Borel_Space.thy --- 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 \ 'a \ ereal" - assumes u': "\x. x \ space M \ (\i. u i x) ----> u' x" + assumes u': "\x. x \ space M \ (\i. u i x) \ u' x" and u: "\i. u i \ borel_measurable M" shows "u' \ borel_measurable M" proof - @@ -1319,7 +1319,7 @@ lemma borel_measurable_LIMSEQ: fixes u :: "nat \ 'a \ real" - assumes u': "\x. x \ space M \ (\i. u i x) ----> u' x" + assumes u': "\x. x \ space M \ (\i. u i x) \ u' x" and u: "\i. u i \ borel_measurable M" shows "u' \ borel_measurable M" proof - @@ -1333,7 +1333,7 @@ lemma borel_measurable_LIMSEQ_metric: fixes f :: "nat \ 'a \ 'b :: metric_space" assumes [measurable]: "\i. f i \ borel_measurable M" - assumes lim: "\x. x \ space M \ (\i. f i x) ----> g x" + assumes lim: "\x. x \ space M \ (\i. f i x) \ g x" shows "g \ borel_measurable M" unfolding borel_eq_closed proof (safe intro!: measurable_measure_of) @@ -1341,7 +1341,7 @@ have [measurable]: "(\x. infdist (g x) A) \ borel_measurable M" proof (rule borel_measurable_LIMSEQ) - show "\x. x \ space M \ (\i. infdist (f i x) A) ----> infdist (g x) A" + show "\x. x \ space M \ (\i. infdist (f i x) A) \ infdist (g x) A" by (intro tendsto_infdist lim) show "\i. (\x. infdist (f i x) A) \ borel_measurable M" by (intro borel_measurable_continuous_on[where f="\x. infdist x A"] @@ -1381,7 +1381,7 @@ have "convergent (\i. if Cauchy (\i. f i x) then f i x else 0)" by (cases "Cauchy (\i. f i x)") (auto simp add: convergent_eq_cauchy[symmetric] convergent_def) - then show "(\i. if Cauchy (\i. f i x) then f i x else 0) ----> u' x" + then show "(\i. if Cauchy (\i. f i x) then f i x else 0) \ u' x" unfolding u'_def by (rule convergent_LIMSEQ_iff[THEN iffD1]) qed measurable diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Caratheodory.thy --- 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: "\A. A \ M \ f A \ \" - assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) ----> 0" + assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 0" shows "\\ :: 'a set \ ereal. (\s \ M. \ s = f s) \ measure_space \ (sigma_sets \ M) \" proof (intro caratheodory' empty_continuous_imp_countably_additive f) show "\A\M. f A \ \" using fin by auto diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Distributions.thy --- 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 "(\\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \lborel) = real_of_nat (fact k)" proof (rule LIMSEQ_unique) let ?X = "\n. \\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \lborel" - show "?X ----> (\\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \lborel)" + show "?X \ (\\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \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 "((\x::real. (1 - (\n\k. (x ^ n / exp x) / (fact n))) * fact k) ---> (1 - (\n\k. 0 / (fact n))) * fact k) at_top" by (intro tendsto_intros tendsto_power_div_exp_0) simp - then show "?X ----> real_of_nat (fact k)" + then show "?X \ 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 diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Fin_Map.thy --- 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 \ ('i \\<^sub>F ('a::metric_space))" assumes ind_f: "\n. domain (f n) = domain g" - assumes proj_g: "\i. i \ domain g \ (\n. (f n) i) ----> g i" - shows "f ----> g" + assumes proj_g: "\i. i \ domain g \ (\n. (f n) i) \ g i" + shows "f \ 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 \ q i" unfolding q_def convergent_def by (metis limI) } note p = this - have "P ----> Q" + have "P \ Q" proof (rule metric_LIMSEQ_I) fix e::real assume "0 < e" have "\ni. \i\d. \n\ni i. dist (p i n) (q i) < e" diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Infinite_Product_Measure.thy --- 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 \ 'a set" assumes E: "\i. E i \ sets M" - shows "(\n. \i\n. measure M (E i)) ----> measure S (Pi UNIV E)" + shows "(\n. \i\n. measure M (E i)) \ measure S (Pi UNIV E)" proof - let ?E = "\n. emb UNIV {..n} (Pi\<^sub>E {.. n} E)" have "\n. (\i\n. measure M (E i)) = measure S (?E n)" diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Interval_Integral.thy --- 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 \ real" where - "incseq X" "\i. a < X i" "\i. X i < b" "X ----> b" + "incseq X" "\i. a < X i" "\i. X i < b" "X \ b" proof (cases b) case PInf with \a < b\ have "a = -\ \ (\r. a = ereal r)" by (cases a) auto - moreover have "(\x. ereal (real (Suc x))) ----> \" + moreover have "(\x. ereal (real (Suc x))) \ \" apply (subst LIMSEQ_Suc_iff) apply (simp add: Lim_PInfty) using nat_ceiling_le_eq by blast - moreover have "\r. (\x. ereal (r + real (Suc x))) ----> \" + moreover have "\r. (\x. ereal (r + real (Suc x))) \ \" 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 \a < b\ a' have "\i. a < ereal (b' - d / real (Suc (Suc i)))" by (cases a) (auto simp: real d_def field_simps) - moreover have "(\i. b' - d / Suc (Suc i)) ----> b'" + moreover have "(\i. b' - d / Suc (Suc i)) \ 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 \ real" where - "decseq X" "\i. a < X i" "\i. X i < b" "X ----> a" + "decseq X" "\i. a < X i" "\i. X i < b" "X \ a" proof - have "-b < -a" using \a < b\ by simp from ereal_incseq_approx[OF this] guess X . @@ -123,7 +123,7 @@ obtains u l :: "nat \ real" where "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" - "l ----> a" "u ----> b" + "l \ a" "u \ b" proof - from dense[OF \a < b\] obtain c where "a < c" "c < b" by safe from ereal_incseq_approx[OF \c < b\] guess u . note u = this @@ -494,12 +494,12 @@ fixes u l :: "nat \ real" assumes approx: "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" - "l ----> a" "u ----> b" + "l \ a" "u \ b" fixes f :: "real \ real" assumes f_integrable: "\i. set_integrable lborel {l i..u i} f" assumes f_nonneg: "AE x in lborel. a < ereal x \ ereal x < b \ 0 \ f x" assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" - assumes lbint_lim: "(\i. LBINT x=l i.. u i. f x) ----> C" + assumes lbint_lim: "(\i. LBINT x=l i.. u i. f x) \ 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. (\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. (\i. indicator {l i..u i} x *\<^sub>R f x) \ indicator (einterval a b) x *\<^sub>R f x" proof - { fix x i assume "l i \ x" "x \ u i" then have "eventually (\i. l i \ x \ x \ 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: "(\i. \ x. indicator {l i..u i} x *\<^sub>R f x \lborel) ----> C" + have 4: "(\i. \ x. indicator {l i..u i} x *\<^sub>R f x \lborel) \ 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 (\x. indicator (einterval a b) x *\<^sub>R f x)" @@ -548,11 +548,11 @@ assumes "a < b" assumes approx: "einterval a b = (\i. {l i .. u i})" "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" - "l ----> a" "u ----> b" + "l \ a" "u \ b" assumes f_integrable: "set_integrable lborel (einterval a b) f" - shows "(\i. LBINT x=l i.. u i. f x) ----> (LBINT x=a..b. f x)" + shows "(\i. LBINT x=l i.. u i. f x) \ (LBINT x=a..b. f x)" proof - - have "(\i. LBINT x:{l i.. u i}. f x) ----> (LBINT x:einterval a b. f x)" + have "(\i. LBINT x:{l i.. u i}. f x) \ (LBINT x:einterval a b. f x)" proof (rule integral_dominated_convergence) show "integrable lborel (\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 "\i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \ 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. (\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. (\i. indicator {l i..u i} x *\<^sub>R f x) \ indicator (einterval a b) x *\<^sub>R f x" proof (intro AE_I2 tendsto_intros Lim_eventually) fix x { fix i assume "l i \ x" "x \ u i" @@ -570,7 +570,7 @@ have "eventually (\i. l i \ x \ x \ u i) sequentially" by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) } then show "eventually (\xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially" - using approx order_tendstoD(2)[OF \l ----> a\, of x] order_tendstoD(1)[OF \u ----> b\, of x] + using approx order_tendstoD(2)[OF \l \ a\, of x] order_tendstoD(1)[OF \u \ b\, 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: "(\i. LBINT x=l i..u i. f x) ----> B - A" + have 3: "(\i. LBINT x=l i..u i. f x) \ 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 "(\i. LBINT x=l i..u i. f x) ----> B - A" + have "(\i. LBINT x=l i..u i. f x) \ B - A" apply (subst FTCi) apply (intro tendsto_intros) using B approx unfolding tendsto_at_iff_sequentially comp_def apply (elim allE[of _ "\i. ereal (u i)"], auto) using A approx unfolding tendsto_at_iff_sequentially comp_def by (elim allE[of _ "\i. ereal (l i)"], auto) - moreover have "(\i. LBINT x=l i..u i. f x) ----> (LBINT x=a..b. f x)" + moreover have "(\i. LBINT x=l i..u i. f x) \ (LBINT x=a..b. f x)" by (rule interval_integral_Icc_approx_integrable [OF \a < b\ 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 \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) ----> A" + have A2: "(\i. g (l i)) \ A" using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\i. ereal (l i)" in spec, auto) hence A3: "\i. g (l i) \ A" by (intro decseq_le, auto simp add: decseq_def) - have B2: "(\i. g (u i)) ----> B" + have B2: "(\i. g (u i)) \ B" using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\i. ereal (u i)" in spec, auto) hence B3: "\i. g (u i) \ B" @@ -903,17 +903,17 @@ apply (auto intro!: continuous_at_imp_continuous_on contf contg') done } note eq1 = this - have "(\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 "(\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))" apply (rule interval_integral_Icc_approx_integrable [OF \a < b\ approx]) by (rule assms) - hence 2: "(\i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. g' x *\<^sub>R f (g x))" + hence 2: "(\i. (LBINT y=g (l i)..g (u i). f y)) \ (LBINT x=a..b. g' x *\<^sub>R f (g x))" by (simp add: eq1) have incseq: "incseq (\i. {g (l i)<..i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x = A..B. f x)" + have "(\i. (LBINT y=g (l i)..g (u i). f y)) \ (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 \A \ B\) 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 \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) ----> A" + have A2: "(\i. g (l i)) \ A" using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\i. ereal (l i)" in spec, auto) hence A3: "\i. g (l i) \ A" by (intro decseq_le, auto simp add: decseq_def) - have B2: "(\i. g (u i)) ----> B" + have B2: "(\i. g (u i)) \ B" using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def) by (drule_tac x = "\i. ereal (u i)" in spec, auto) hence B3: "\i. g (u i) \ B" @@ -1006,10 +1006,10 @@ by (simp add: ac_simps) } note eq1 = this have "(\i. LBINT x=l i..u i. f (g x) * g' x) - ----> (LBINT x=a..b. f (g x) * g' x)" + \ (LBINT x=a..b. f (g x) * g' x)" apply (rule interval_integral_Icc_approx_integrable [OF \a < b\ approx]) by (rule assms) - hence 2: "(\i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. f (g x) * g' x)" + hence 2: "(\i. (LBINT y=g (l i)..g (u i). f y)) \ (LBINT x=a..b. f (g x) * g' x)" by (simp add: eq1) have incseq: "incseq (\i. {g (l i)<..a. F b - F a) ---> emeasure ?F {a..b}) (at_left a)" proof (rule tendsto_at_left_sequentially) show "a - 1 < a" by simp - fix X assume "\n. X n < a" "incseq X" "X ----> a" - with \a \ b\ have "(\n. emeasure ?F {X n<..b}) ----> emeasure ?F (\n. {X n <..b})" + fix X assume "\n. X n < a" "incseq X" "X \ a" + with \a \ b\ have "(\n. emeasure ?F {X n<..b}) \ emeasure ?F (\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 "(\n. {X n <..b}) = {a..b}" using \\n. X n < a\ apply auto - apply (rule LIMSEQ_le_const2[OF \X ----> a\]) + apply (rule LIMSEQ_le_const2[OF \X \ a\]) apply (auto intro: less_imp_le) apply (auto intro: less_le_trans) done also have "(\n. emeasure ?F {X n<..b}) = (\n. F b - F (X n))" using \\n. X n < a\ \a \ b\ by (subst *) (auto intro: less_imp_le less_le_trans) - finally show "(\n. F b - F (X n)) ----> emeasure ?F {a..b}" . + finally show "(\n. F b - F (X n)) \ emeasure ?F {a..b}" . qed show "((\a. ereal (F b - F a)) ---> F b - F a) (at_left a)" using cont_F @@ -808,7 +808,7 @@ by (intro setsum_mono2) auto from union(1) have *: "\x i j. x \ F i \ x \ F j \ j = i" by (auto simp add: disjoint_family_on_def) - show "\x. (\k. ?f k x) ----> (if x \ UNION UNIV F \ box a b then 1 else 0)" + show "\x. (\k. ?f k x) \ (if x \ UNION UNIV F \ 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 ((\x. F x) \ box a b) \ emeasure lborel (box a b)" by (intro emeasure_mono) auto - with union(1) show "(\k. \i ?M (\i. F i)" + with union(1) show "(\k. \i ?M (\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 "\k x. ?f k x \ ?f (Suc k) x" by (auto simp: box_def) { fix x assume "x \ A" - moreover have "(\k. indicator (A \ ?B k) x :: real) ----> indicator (\k::nat. A \ ?B k) x" + moreover have "(\k. indicator (A \ ?B k) x :: real) \ indicator (\k::nat. A \ ?B k) x" by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def) - ultimately show "(\k. if x \ A \ ?B k then 1 else 0::real) ----> 1" + ultimately show "(\k. if x \ A \ ?B k then 1 else 0::real) \ 1" by (simp add: indicator_def UN_box_eq_UNIV) } - have "(\n. emeasure lborel (A \ ?B n)) ----> emeasure lborel (\n::nat. A \ ?B n)" + have "(\n. emeasure lborel (A \ ?B n)) \ emeasure lborel (\n::nat. A \ ?B n)" by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def) also have "(\n. emeasure lborel (A \ ?B n)) = (\n. measure lborel (A \ ?B n))" proof (intro ext emeasure_eq_ereal_measure) @@ -850,7 +850,7 @@ then show "emeasure lborel (A \ ?B n) \ \" by auto qed - finally show "(\n. measure lborel (A \ ?B n)) ----> measure lborel A" + finally show "(\n. measure lborel (A \ ?B n)) \ 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: "\i. integral UNIV (U i) = p i" using U_int by (rule integral_unique) - have *: "f integrable_on UNIV \ (\k. integral UNIV (U k)) ----> integral UNIV f" + have *: "f integrable_on UNIV \ (\k. integral UNIV (U k)) \ integral UNIV f" proof (rule monotone_convergence_increasing) show "\k. U k integrable_on UNIV" using U_int by auto show "\k. \x\UNIV. U k x \ U (Suc k) x" using \incseq U\ 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 "\x\UNIV. (\k. U k x) ----> f x" + show "\x\UNIV. (\k. U k x) \ f x" using seq by auto qed - moreover have "(\i. (\\<^sup>+x. U i x \lborel)) ----> (\\<^sup>+x. f x \lborel)" + moreover have "(\i. (\\<^sup>+x. U i x \lborel)) \ (\\<^sup>+x. f x \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 "\k. \x\UNIV. norm (s k x) \ norm (2 * f x)" using lim by (auto simp add: abs_mult) - show "\x\UNIV. (\k. s k x) ----> f x" + show "\x\UNIV. (\k. s k x) \ f x" using lim by auto - show "(\k. integral\<^sup>L lborel (s k)) ----> integral\<^sup>L lborel f" + show "(\k. integral\<^sup>L lborel (s k)) \ integral\<^sup>L lborel f" using lim lim(1)[THEN borel_measurable_integrable] by (intro integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) auto qed @@ -1258,7 +1258,7 @@ from reals_Archimedean2[of "x - a"] guess n .. then have "eventually (\n. ?f n x = ?fR x) sequentially" by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator) - then show "(\n. ?f n x) ----> ?fR x" + then show "(\n. ?f n x) \ ?fR x" by (rule Lim_eventually) qed then have "integral\<^sup>N lborel ?fR = (\\<^sup>+ x. (SUP i::nat. ?f i x) \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 "(\x. F (a + real x)) ----> T" + have "(\x. F (a + real x)) \ 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 "(\n. ereal (F (a + real n) - F a)) ----> ereal (T - F a)" + then show "(\n. ereal (F (a + real n) - F a)) \ ereal (T - F a)" unfolding lim_ereal by (intro tendsto_diff) auto qed diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Measure_Space.thy --- 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 "(\n. \i f A + f B" + shows "(\n. \i f A + f B" proof - have "(\n. \i < Suc (Suc n). f (binaryset A B i)) = (\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 "... \ f A + f B" by (rule tendsto_const) ultimately - have "(\n. \i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" + have "(\n. \i< Suc (Suc n). f (binaryset A B i)) \ f A + f B" by metis - hence "(\n. \i< n+2. f (binaryset A B i)) ----> f A + f B" + hence "(\n. \i< n+2. f (binaryset A B i)) \ 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 \ - (\A. range A \ M \ incseq A \ (\i. A i) \ M \ (\i. f (A i)) ----> f (\i. A i))" + (\A. range A \ M \ incseq A \ (\i. A i) \ M \ (\i. f (A i)) \ f (\i. A i))" unfolding countably_additive_def proof safe assume count_sum: "\A. range A \ M \ disjoint_family A \ UNION UNIV A \ M \ (\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: "(\i. f (disjointed A i)) = f (\i. A i)" by (auto simp: UN_disjointed_eq disjoint_family_disjointed) - moreover have "(\n. (\i (\i. f (disjointed A i))" + moreover have "(\n. (\i (\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 "(\n. (\i\n. f (disjointed A i))) ----> (\i. f (disjointed A i))" + have "(\n. (\i\n. f (disjointed A i))) \ (\i. f (disjointed A i))" unfolding lessThan_Suc_atMost . moreover have "\n. (\i\n. f (disjointed A i)) = f (A n)" using disjointed_additive[OF f A(1,2)] . - ultimately show "(\i. f (A i)) ----> f (\i. A i)" by simp + ultimately show "(\i. f (A i)) \ f (\i. A i)" by simp next - assume cont: "\A. range A \ M \ incseq A \ (\i. A i) \ M \ (\i. f (A i)) ----> f (\i. A i)" + assume cont: "\A. range A \ M \ incseq A \ (\i. A i) \ M \ (\i. f (A i)) \ f (\i. A i)" fix A :: "nat \ 'a set" assume A: "range A \ M" "disjoint_family A" "(\i. A i) \ M" have *: "(\n. (\ii. A i)" by auto - have "(\n. f (\i f (\i. A i)" + have "(\n. f (\i f (\i. A i)" proof (unfold *[symmetric], intro cont[rule_format]) show "range (\i. \i M" "(\i. \i 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 "(\A. range A \ M \ decseq A \ (\i. A i) \ M \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> f (\i. A i)) - \ (\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> 0)" + shows "(\A. range A \ M \ decseq A \ (\i. A i) \ M \ (\i. f (A i) \ \) \ (\i. f (A i)) \ f (\i. A i)) + \ (\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i) \ \) \ (\i. f (A i)) \ 0)" proof safe - assume cont: "(\A. range A \ M \ decseq A \ (\i. A i) \ M \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> f (\i. A i))" + assume cont: "(\A. range A \ M \ decseq A \ (\i. A i) \ M \ (\i. f (A i) \ \) \ (\i. f (A i)) \ f (\i. A i))" fix A :: "nat \ 'a set" assume A: "range A \ M" "decseq A" "(\i. A i) = {}" "\i. f (A i) \ \" - with cont[THEN spec, of A] show "(\i. f (A i)) ----> 0" + with cont[THEN spec, of A] show "(\i. f (A i)) \ 0" using \positive M f\[unfolded positive_def] by auto next - assume cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> 0" + assume cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i) \ \) \ (\i. f (A i)) \ 0" fix A :: "nat \ 'a set" assume A: "range A \ M" "decseq A" "(\i. A i) \ M" "\i. f (A i) \ \" have f_mono: "\a b. a \ M \ b \ M \ a \ b \ f a \ f b" @@ -350,7 +350,7 @@ then have "f (A i - (\i. A i)) \ \" using A by auto } note f_fin = this - have "(\i. f (A i - (\i. A i))) ----> 0" + have "(\i. f (A i - (\i. A i))) \ 0" proof (intro cont[rule_format, OF _ decseq _ f_fin]) show "range (\i. A i - (\i. A i)) \ M" "(\i. A i - (\i. A i)) = {}" using A by auto @@ -372,14 +372,14 @@ ultimately have "(INF n. f (A n)) = f (\i. A i)" by simp with LIMSEQ_INF[OF decseq_fA] - show "(\i. f (A i)) ----> f (\i. A i)" by simp + show "(\i. f (A i)) \ f (\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" "\A\M. f A \ \" - assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) ----> 0" + assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 0" assumes A: "range A \ M" "incseq A" "(\i. A i) \ M" - shows "(\i. f (A i)) ----> f (\i. A i)" + shows "(\i. f (A i)) \ f (\i. A i)" proof - have "\A\M. \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 "(\i. f ((\i. A i) - A i)) ----> 0" + from A have "(\i. f ((\i. A i) - A i)) \ 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 ((\i. A i) - A i) = ereal (f' (\i. A i) - f' (A i))" using A f' by auto } - ultimately have "(\i. f' (\i. A i) - f' (A i)) ----> 0" + ultimately have "(\i. f' (\i. A i) - f' (A i)) \ 0" by (simp add: zero_ereal_def) - then have "(\i. f' (A i)) ----> f' (\i. A i)" + then have "(\i. f' (A i)) \ f' (\i. A i)" by (rule Lim_transform2[OF tendsto_const]) - then show "(\i. f (A i)) ----> f (\i. A i)" + then show "(\i. f (A i)) \ f (\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: "\A\M. f A \ \" - assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) ----> 0" + assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 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 \ sets M \ incseq A \ (\i. (emeasure M (A i))) ----> emeasure M (\i. A i)" + "range A \ sets M \ incseq A \ (\i. (emeasure M (A i))) \ emeasure M (\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 \ sets M" "decseq A" and fin: "\i. emeasure M (A i) \ \" - shows "(\i. emeasure M (A i)) ----> emeasure M (\i. A i)" + shows "(\i. emeasure M (A i)) \ emeasure M (\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 \ sets M" "incseq A" and fin: "emeasure M (\i. A i) \ \" - shows "(\i. (measure M (A i))) ----> (measure M (\i. A i))" + shows "(\i. (measure M (A i))) \ (measure M (\i. A i))" proof - have "ereal ((measure M (\i. A i))) = emeasure M (\i. A i)" using fin by (auto simp: emeasure_eq_ereal_measure) @@ -1537,7 +1537,7 @@ lemma Lim_measure_decseq: assumes A: "range A \ sets M" "decseq A" and fin: "\i. emeasure M (A i) \ \" - shows "(\n. measure M (A n)) ----> measure M (\i. A i)" + shows "(\n. measure M (A n)) \ measure M (\i. A i)" proof - have "emeasure M (\i. A i) \ 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 \ sets M" "incseq A" - shows "(\i. measure M (A i)) ----> measure M (\i. A i)" + shows "(\i. measure M (A i)) \ measure M (\i. A i)" using Lim_measure_incseq[OF A] by simp lemma (in finite_measure) finite_Lim_measure_decseq: assumes A: "range A \ sets M" "decseq A" - shows "(\n. measure M (A n)) ----> measure M (\i. A i)" + shows "(\n. measure M (A n)) \ measure M (\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 \ 'a set" assume "incseq F" - show "(\i. ?M (F i)) ----> ?M (\i. F i)" + show "(\i. ?M (F i)) \ ?M (\i. F i)" proof cases assume "\i. \j\i. F i = F j" then guess i .. note i = this @@ -1823,7 +1823,7 @@ have "incseq (\i. ?M (F i))" using \incseq F\ unfolding incseq_def by (auto simp: card_mono dest: finite_subset) - then have "(\i. ?M (F i)) ----> (SUP n. ?M (F n))" + then have "(\i. ?M (F i)) \ (SUP n. ?M (F n))" by (rule LIMSEQ_SUP) moreover have "(SUP n. ?M (F n)) = \" diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- 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" "\i. f i \ borel_measurable M" "\n x. 0 \ f n x" - and u: "\x. (\i. f i x) ----> u x" - shows "(\n. integral\<^sup>N M (f n)) ----> integral\<^sup>N M u" + and u: "\x. (\i. f i x) \ u x" + shows "(\n. integral\<^sup>N M (f n)) \ integral\<^sup>N M u" proof - - have "(\n. integral\<^sup>N M (f n)) ----> (SUP n. integral\<^sup>N M (f n))" + have "(\n. integral\<^sup>N M (f n)) \ (SUP n. integral\<^sup>N M (f n))" using f by (intro LIMSEQ_SUP[of "\n. integral\<^sup>N M (f n)"] incseq_nn_integral) also have "(SUP n. integral\<^sup>N M (f n)) = integral\<^sup>N M (\x. SUP n. f n x)" using f by (intro nn_integral_monotone_convergence_SUP[symmetric]) @@ -1467,8 +1467,8 @@ "\i. u i \ borel_measurable M" "u' \ borel_measurable M" "w \ borel_measurable M" and bound: "\j. AE x in M. 0 \ u j x" "\j. AE x in M. u j x \ w x" and w: "(\\<^sup>+x. w x \M) < \" - and u': "AE x in M. (\i. u i x) ----> u' x" - shows "(\i. (\\<^sup>+x. u i x \M)) ----> (\\<^sup>+x. u' x \M)" + and u': "AE x in M. (\i. u i x) \ u' x" + shows "(\i. (\\<^sup>+x. u i x \M)) \ (\\<^sup>+x. u' x \M)" proof - have "limsup (\n. integral\<^sup>N M (u n)) \ (\\<^sup>+ x. limsup (\n. u n x) \M)" by (intro nn_integral_limsup[OF _ _ bound w]) auto @@ -1489,9 +1489,9 @@ assumes "(\\<^sup>+ x. f 0 x \M) < \" and nn: "\x i. 0 \ f i x" shows "(\\<^sup>+ x. (INF i. f i x) \M) = (INF i. integral\<^sup>N M (f i))" proof (rule LIMSEQ_unique) - show "(\i. integral\<^sup>N M (f i)) ----> (INF i. integral\<^sup>N M (f i))" + show "(\i. integral\<^sup>N M (f i)) \ (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 "(\i. integral\<^sup>N M (f i)) ----> \\<^sup>+ x. (INF i. f i x) \M" + show "(\i. integral\<^sup>N M (f i)) \ \\<^sup>+ x. (INF i. f i x) \M" proof (rule nn_integral_dominated_convergence) show "(\\<^sup>+ x. f 0 x \M) < \" "\i. f i \ borel_measurable M" "f 0 \ borel_measurable M" by fact+ @@ -1499,7 +1499,7 @@ using nn by auto show "\j. AE x in M. f j x \ f 0 x" using f by (auto simp: decseq_def le_fun_def) - show "AE x in M. (\i. f i x) ----> (INF i. f i x)" + show "AE x in M. (\i. f i x) \ (INF i. f i x)" using f by (auto intro!: LIMSEQ_INF simp: decseq_def le_fun_def) show "(\x. INF i. f i x) \ borel_measurable M" by auto diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Projective_Family.thy --- 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 \(\i. A i) = {}\ * show False by (subst (asm) prod_emb_trans) (auto simp: A[abs_def]) qed - moreover have "(\i. P (J i) (X i)) ----> (INF i. P (J i) (X i))" + moreover have "(\i. P (J i) (X i)) \ (INF i. P (J i) (X i))" proof (intro LIMSEQ_INF antimonoI) fix x y :: nat assume "x \ y" have "P (J y \ J x) (emb (J y \ J x) (J y) (X y)) \ P (J y \ J x) (emb (J y \ J x) (J x) (X x))" @@ -217,7 +217,7 @@ then show "P (J y) (X y) \ P (J x) (X x)" using * by (simp add: emeasure_P) qed - ultimately show "(\i. \G (A i)) ----> 0" + ultimately show "(\i. \G (A i)) \ 0" by (auto simp: A[abs_def] mu_G_spec *) qed then obtain \ where eq: "\s\generator. \ s = \G s" diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Projective_Limit.thy --- 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 "\n. (f o (\i. m + i)) n \ S" using assms by auto from seq_compactE[OF \compact S\[unfolded compact_eq_seq_compact_metric] this] guess l r . - hence "l \ S" "subseq ((\i. m + i) o r) \ (f \ ((\i. m + i) o r)) ----> l" + hence "l \ S" "subseq ((\i. m + i) o r) \ (f \ ((\i. m + i) o r)) \ l" using subseq_o[OF \subseq (op + m)\ \subseq r\] by (auto simp: o_def) - thus "\l r. l \ S \ subseq r \ (f \ r) ----> l" by blast + thus "\l r. l \ S \ subseq r \ (f \ r) \ l" by blast qed -sublocale finmap_seqs_into_compact \ subseqs "\n s. (\l. (\i. ((f o s) i)\<^sub>F n) ----> l)" +sublocale finmap_seqs_into_compact \ subseqs "\n s. (\l. (\i. ((f o s) i)\<^sub>F n) \ 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 "\r'. subseq r' \ (\l. (\i. ((f \ (s \ r')) i)\<^sub>F n) ----> l)" by (auto simp: o_def) + thus "\r'. subseq r' \ (\l. (\i. ((f \ (s \ r')) i)\<^sub>F n) \ l)" by (auto simp: o_def) qed -lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\l. (\i. (f (diagseq i))\<^sub>F n) ----> l" +lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\l. (\i. (f (diagseq i))\<^sub>F n) \ l" proof - - obtain l where "(\i. ((f o (diagseq o op + (Suc n))) i)\<^sub>F n) ----> l" + obtain l where "(\i. ((f o (diagseq o op + (Suc n))) i)\<^sub>F n) \ l" proof (atomize_elim, rule diagseq_holds) fix r s n assume "subseq r" - assume "\l. (\i. ((f \ s) i)\<^sub>F n) ----> l" - then obtain l where "((\i. (f i)\<^sub>F n) o s) ----> l" + assume "\l. (\i. ((f \ s) i)\<^sub>F n) \ l" + then obtain l where "((\i. (f i)\<^sub>F n) o s) \ l" by (auto simp: o_def) - hence "((\i. (f i)\<^sub>F n) o s o r) ----> l" using \subseq r\ + hence "((\i. (f i)\<^sub>F n) o s o r) \ l" using \subseq r\ by (rule LIMSEQ_subseq_LIMSEQ) - thus "\l. (\i. ((f \ (s \ r)) i)\<^sub>F n) ----> l" by (auto simp add: o_def) + thus "\l. (\i. ((f \ (s \ r)) i)\<^sub>F n) \ l" by (auto simp add: o_def) qed - hence "(\i. ((f (diagseq (i + Suc n))))\<^sub>F n) ----> l" by (simp add: ac_simps) - hence "(\i. (f (diagseq i))\<^sub>F n) ----> l" by (rule LIMSEQ_offset) + hence "(\i. ((f (diagseq (i + Suc n))))\<^sub>F n) \ l" by (simp add: ac_simps) + hence "(\i. (f (diagseq i))\<^sub>F n) \ l" by (rule LIMSEQ_offset) thus ?thesis .. qed @@ -362,10 +362,10 @@ using \j \ J (Suc n)\ \j \ J (Suc m)\ unfolding j by (subst proj_fm, auto)+ qed - have "\t. \z. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z" + have "\t. \z. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) \ z" using diagonal_tendsto .. then obtain z where z: - "\t. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z t" + "\t. (\i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) \ z t" unfolding choice_iff by blast { fix n :: nat assume "n \ 1" @@ -377,7 +377,7 @@ assume t: "t \ domain (finmap_of (Utn ` J n) z)" hence "t \ Utn ` J n" by simp then obtain j where j: "t = Utn j" "j \ J n" by auto - have "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> z t" + have "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) \ 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 "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> (finmap_of (Utn ` J n) z)\<^sub>F t" + hence "(\i. (fm n (y (Suc (diagseq i))))\<^sub>F t) \ (finmap_of (Utn ` J n) z)\<^sub>F t" by (simp add: tendsto_intros) } ultimately - have "(\i. fm n (y (Suc (diagseq i)))) ----> finmap_of (Utn ` J n) z" + have "(\i. fm n (y (Suc (diagseq i)))) \ finmap_of (Utn ` J n) z" by (rule tendsto_finmap) - hence "((\i. fm n (y (Suc (diagseq i)))) o (\i. i + n)) ----> finmap_of (Utn ` J n) z" + hence "((\i. fm n (y (Suc (diagseq i)))) o (\i. i + n)) \ finmap_of (Utn ` J n) z" by (intro lim_subseq) (simp add: subseq_def) moreover have "(\i. ((\i. fm n (y (Suc (diagseq i)))) o (\i. i + n)) i \ K' n)" diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Radon_Nikodym.thy --- 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] \range A \ sets M\ M'.finite_Lim_measure_incseq[OF _ A] - have convergent: "(\i. ?d (A i)) ----> ?d (\i. A i)" + have convergent: "(\i. ?d (A i)) \ ?d (\i. A i)" by (auto intro!: tendsto_diff simp: sets_eq) obtain n :: nat where "- ?d (\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 "(\i. A i) \ sets M" using \\n. A n \ sets M\ 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 "(\i. ?d (A i)) ----> ?d (\i. A i)" by (auto intro!: tendsto_diff simp: sets_eq) + have "(\i. ?d (A i)) \ ?d (\i. A i)" by (auto intro!: tendsto_diff simp: sets_eq) thus "?d (space M) \ ?d (\i. A i)" using mono_dA[THEN monoD, of 0 _] by (rule_tac LIMSEQ_le_const) auto next diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Regularity.thy --- 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 = (\x\X. cball x r)" by (auto simp add: sU) (metis dist_commute order_less_imp_le) let ?U = "\k. (\n\{0..k}. cball (from_nat_into X n) r)" - have "(\k. emeasure M (\n\{0..k}. cball (from_nat_into X n) r)) ----> M ?U" + have "(\k. emeasure M (\n\{0..k}. cball (from_nat_into X n) r)) \ 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 \ ?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 "(\k. M (\n\{0..k}. cball (from_nat_into X n) r)) ----> M (space M)" . + finally have "(\k. M (\n\{0..k}. cball (from_nat_into X n) r)) \ 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 \1/n>0\] - have "(\k. measure M (\i\{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)" + have "(\k. measure M (\i\{0..k}. cball (from_nat_into X i) (1/real n))) \ measure M (space M)" unfolding emeasure_eq_measure by simp from metric_LIMSEQ_D[OF this \0 < e * 2 powr -n\] obtain k where "dist (measure M (\i\{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 \ sets M" by (auto simp: sb borel_eq_closed) with union have M[symmetric]: "(\i. M (D i)) = M (\i. D i)" by (intro suminf_emeasure) - also have "(\n. \i (\i. M (D i))" + also have "(\n. \i (\i. M (D i))" by (intro summable_LIMSEQ summable_ereal_pos emeasure_nonneg) - finally have measure_LIMSEQ: "(\n. \i measure M (\i. D i)" + finally have measure_LIMSEQ: "(\n. \i measure M (\i. D i)" by (simp add: emeasure_eq_measure) have "(\i. D i) \ sets M" using \range D \ sets M\ by auto diff -r e13e70f32407 -r e01015e49041 src/HOL/Probability/Set_Integral.thy --- 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 "\i. A i \ sets M" "mono A" assumes nneg: "\x i. x \ A i \ 0 \ f x" and intgbl: "\i::nat. set_integrable M (A i) f" - and lim: "(\i::nat. LINT x:A i|M. f x) ----> l" + and lim: "(\i::nat. LINT x:A i|M. f x) \ l" shows "set_integrable M (\i. A i) f" apply (rule integrable_monotone_convergence[where f = "\i::nat. \x. indicator (A i) x *\<^sub>R f x" and x = l]) apply (rule intgbl) @@ -336,7 +336,7 @@ using \mono A\ apply (auto simp: mono_def nneg split: split_indicator) [] proof (rule AE_I2) { fix x assume "x \ space M" - show "(\i. indicator (A i) x *\<^sub>R f x) ----> indicator (\i. A i) x *\<^sub>R f x" + show "(\i. indicator (A i) x *\<^sub>R f x) \ indicator (\i. A i) x *\<^sub>R f x" proof cases assume "\i. x \ A i" then guess i .. @@ -409,7 +409,7 @@ fixes f :: "_ \ 'a :: {banach, second_countable_topology}" assumes [measurable]: "\i. A i \ sets M" and A: "incseq A" and intgbl: "set_integrable M (\i. A i) f" - shows "(\i. LINT x:(A i)|M. f x) ----> LINT x:(\i. A i)|M. f x" + shows "(\i. LINT x:(A i)|M. f x) \ LINT x:(\i. A i)|M. f x" proof (intro integral_dominated_convergence[where w="\x. indicator (\i. A i) x *\<^sub>R norm (f x)"]) have int_A: "\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 \ A i" - with A have "(\xa. indicator (A xa) x::real) ----> 1 \ (\xa. 1::real) ----> 1" + with A have "(\xa. indicator (A xa) x::real) \ 1 \ (\xa. 1::real) \ 1" by (intro filterlim_cong refl) (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) } - then show "AE x in M. (\i. indicator (A i) x *\<^sub>R f x) ----> indicator (\i. A i) x *\<^sub>R f x" + then show "AE x in M. (\i. indicator (A i) x *\<^sub>R f x) \ indicator (\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 :: "_ \ 'a :: {banach, second_countable_topology}" assumes [measurable]: "\i. A i \ sets M" and A: "decseq A" and int0: "set_integrable M (A 0) f" - shows "(\i::nat. LINT x:(A i)|M. f x) ----> LINT x:(\i. A i)|M. f x" + shows "(\i::nat. LINT x:(A i)|M. f x) \ LINT x:(\i. A i)|M. f x" proof (rule integral_dominated_convergence) have int_A: "\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 "\i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \ indicator (A 0) x *\<^sub>R norm (f x)" using A by (auto split: split_indicator simp: decseq_def) { fix x i assume "x \ space M" "x \ A i" - with A have "(\i. indicator (A i) x::real) ----> 0 \ (\i. 0::real) ----> 0" + with A have "(\i. indicator (A i) x::real) \ 0 \ (\i. 0::real) \ 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. (\i. indicator (A i) x *\<^sub>R f x) ----> indicator (\i. A i) x *\<^sub>R f x" + then show "AE x in M. (\i. indicator (A i) x *\<^sub>R f x) \ indicator (\i. A i) x *\<^sub>R f x" by (intro AE_I2 tendsto_intros) (auto split: split_indicator) qed diff -r e13e70f32407 -r e01015e49041 src/HOL/Real_Vector_Spaces.thy --- 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 \Limits of Sequences\ -lemma lim_sequentially: "X ----> (L::'a::metric_space) \ (\r>0. \no. \n\no. dist (X n) L < r)" +lemma lim_sequentially: "X \ (L::'a::metric_space) \ (\r>0. \no. \n\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) = (\r>0. \no>0. \n\no. dist (X n) L < r)" +lemma LIMSEQ_iff_nz: "X \ (L::'a::metric_space) = (\r>0. \no>0. \n\no. dist (X n) L < r)" unfolding lim_sequentially by (metis Suc_leD zero_less_Suc) lemma metric_LIMSEQ_I: - "(\r. 0 < r \ \no. \n\no. dist (X n) L < r) \ X ----> (L::'a::metric_space)" + "(\r. 0 < r \ \no. \n\no. dist (X n) L < r) \ X \ (L::'a::metric_space)" by (simp add: lim_sequentially) lemma metric_LIMSEQ_D: - "\X ----> (L::'a::metric_space); 0 < r\ \ \no. \n\no. dist (X n) L < r" + "\X \ (L::'a::metric_space); 0 < r\ \ \no. \n\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 \ 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: "\n. f n \ f (Suc n)" and bdd: "\n. f n \ l" and en: "\e. 0 < e \ \n. l \ f n + e" - shows "f ----> l" + shows "f \ 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 "\s. s \ S \ s \ X N + 1" by (rule bound_isUb) qed - have "X ----> Sup S" + have "X \ 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 \ 'b::first_countable_topology" - assumes *: "\X. filterlim X at_top sequentially \ (\n. f (X n)) ----> y" + assumes *: "\X. filterlim X at_top sequentially \ (\n. f (X n)) \ 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 \ real" assumes mono: "mono f" - assumes limseq: "(\n. f (real n)) ----> y" + assumes limseq: "(\n. f (real n)) \ y" shows "(f ---> y) at_top" proof (rule tendstoI) fix e :: real assume "0 < e" diff -r e13e70f32407 -r e01015e49041 src/HOL/Series.thy --- 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 \ 'a::{topological_space, comm_monoid_add}) \ 'a \ bool" (infixr "sums" 80) where - "f sums s \ (\n. \i s" + "f sums s \ (\n. \i s" definition summable :: "(nat \ 'a::{topological_space, comm_monoid_add}) \ bool" where "summable f \ (\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 \ (\n. \i suminf f" +lemma summable_LIMSEQ: "summable f \ (\n. \i suminf f" by (rule summable_sums [unfolded sums_def]) lemma sums_unique: "f sums s \ s = suminf f" @@ -223,7 +223,7 @@ lemma suminf_eq_zero_iff: "summable f \ \n. 0 \ f n \ suminf f = 0 \ (\n. f n = 0)" proof assume "summable f" "suminf f = 0" and pos: "\n. 0 \ f n" - then have f: "(\n. \i 0" + then have f: "(\n. \i 0" using summable_LIMSEQ[of f] by simp then have "\i. (\n\{i}. f n) \ 0" proof (rule LIMSEQ_le_const) @@ -268,13 +268,13 @@ fixes f :: "nat \ 'a::real_normed_vector" shows "(\n. f (Suc n)) sums s \ f sums (s + f 0)" proof - - have "f sums (s + f 0) \ (\i. \j s + f 0" + have "f sums (s + f 0) \ (\i. \j s + f 0" by (subst LIMSEQ_Suc_iff) (simp add: sums_def) - also have "\ \ (\i. (\j s + f 0" + also have "\ \ (\i. (\j s + f 0" by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0) also have "\ \ (\n. f (Suc n)) sums s" proof - assume "(\i. (\j s + f 0" + assume "(\i. (\j s + f 0" with tendsto_add[OF this tendsto_const, of "- f 0"] show "(\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 \summable f\]) qed -lemma summable_LIMSEQ_zero: "summable f \ f ----> 0" +lemma summable_LIMSEQ_zero: "summable f \ f \ 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 \ 1" by auto hence neq_0: "c - 1 \ 0" by simp - from less_1 have lim_0: "(\n. c^n) ----> 0" + from less_1 have lim_0: "(\n. c^n) \ 0" by (rule LIMSEQ_power_zero) - hence "(\n. c ^ n / (c - 1) - 1 / (c - 1)) ----> 0 / (c - 1) - 1 / (c - 1)" + hence "(\n. c ^ n / (c - 1) - 1 / (c - 1)) \ 0 / (c - 1) - 1 / (c - 1)" using neq_0 by (intro tendsto_intros) - hence "(\n. (c ^ n - 1) / (c - 1)) ----> 1 / (1 - c)" + hence "(\n. (c ^ n - 1) / (c - 1)) \ 1 / (1 - c)" by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) thus "(\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 (\n. c ^ n) \ norm c < 1" proof assume "summable (\n. c ^ n :: 'a :: real_normed_field)" - hence "(\n. norm c ^ n) ----> 0" + hence "(\n. norm c ^ n) \ 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 \Telescoping\ lemma telescope_sums: - assumes "f ----> (c :: 'a :: real_normed_vector)" + assumes "f \ (c :: 'a :: real_normed_vector)" shows "(\n. f (Suc n) - f n) sums (c - f 0)" unfolding sums_def proof (subst LIMSEQ_Suc_iff [symmetric]) have "(\n. \kn. f (Suc n) - f 0)" by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff) - also have "\ ----> c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const) - finally show "(\n. \n c - f 0" . + also have "\ \ c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const) + finally show "(\n. \n c - f 0" . qed lemma telescope_sums': - assumes "f ----> (c :: 'a :: real_normed_vector)" + assumes "f \ (c :: 'a :: real_normed_vector)" shows "(\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 \ (c :: 'a :: real_normed_vector)" shows "summable (\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 \ (c :: 'a :: real_normed_vector)" shows "summable (\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 "(\n. (\kk (\k. a k) * (\k. b k)" + have "(\n. (\kk (\k. a k) * (\k. b k)" by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b]) - hence 1: "(\n. setsum ?g (?S1 n)) ----> (\k. a k) * (\k. b k)" + hence 1: "(\n. setsum ?g (?S1 n)) \ (\k. a k) * (\k. b k)" by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) - have "(\n. (\kk (\k. norm (a k)) * (\k. norm (b k))" + have "(\n. (\kk (\k. norm (a k)) * (\k. norm (b k))" using a b by (intro tendsto_mult summable_LIMSEQ) - hence "(\n. setsum ?f (?S1 n)) ----> (\k. norm (a k)) * (\k. norm (b k))" + hence "(\n. setsum ?f (?S1 n)) \ (\k. norm (a k)) * (\k. norm (b k))" by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) hence "convergent (\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: "(\n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0" + hence 2: "(\n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) \ 0" unfolding tendsto_Zfun_iff diff_0_right by (simp only: setsum_diff finite_S1 S2_le_S1) - with 1 have "(\n. setsum ?g (?S2 n)) ----> (\k. a k) * (\k. b k)" + with 1 have "(\n. setsum ?g (?S2 n)) \ (\k. a k) * (\k. b k)" by (rule Lim_transform2) thus ?thesis by (simp only: sums_def setsum_triangle_reindex) qed @@ -933,12 +933,12 @@ have "incseq (\n. \i g) i)" by (rule incseq_SucI) (auto simp add: pos) - then obtain L where L: "(\ n. \i g) i) ----> L" + then obtain L where L: "(\ n. \i g) i) \ L" using smaller by(rule incseq_convergent) hence "(f \ g) sums L" by (simp add: sums_def) thus "summable (f o g)" by (auto simp add: sums_iff) - hence "(\n. \i g) i) ----> suminf (f \ g)" + hence "(\n. \i g) i) \ suminf (f \ g)" by(rule summable_LIMSEQ) thus le: "suminf (f \ g) \ suminf f" by(rule LIMSEQ_le_const2)(blast intro: smaller[rule_format]) @@ -971,7 +971,7 @@ shows "(\n. f (g n)) sums c \ f sums c" unfolding sums_def proof - assume lim: "(\n. \k c" + assume lim: "(\n. \k c" have "(\n. \kn. \kkk ----> c" unfolding o_def . - finally show "(\n. \k c" . + also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\ \ c" unfolding o_def . + finally show "(\n. \k c" . next - assume lim: "(\n. \k c" + assume lim: "(\n. \k c" def g_inv \ "\n. LEAST m. g m \ n" from filterlim_subseq[OF subseq] have g_inv_ex: "\m. g m \ 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 "(\n. \k c" by (rule filterlim_compose) - finally show "(\n. \k c" . + from lim and this have "(\n. \k c" by (rule filterlim_compose) + finally show "(\n. \k c" . qed lemma summable_mono_reindex: diff -r e13e70f32407 -r e01015e49041 src/HOL/Topological_Spaces.thy --- 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 \ 'a, 'a] \ bool" - ("((_)/ ----> (_))" [60, 60] 60) where - "X ----> L \ (X ---> L) sequentially" + ("((_)/ \ (_))" [60, 60] 60) where + "X \ L \ (X ---> L) sequentially" abbreviation (in t2_space) lim :: "(nat \ 'a) \ 'a" where "lim X \ Lim sequentially X" definition (in topological_space) convergent :: "(nat \ 'a) \ bool" where - "convergent X = (\L. X ----> L)" + "convergent X = (\L. X \ L)" -lemma lim_def: "lim X = (THE L. X ----> L)" +lemma lim_def: "lim X = (THE L. X \ L)" unfolding Lim_def .. subsubsection \Monotone sequences and subsequences\ @@ -996,81 +996,81 @@ lemma LIMSEQ_const_iff: fixes k l :: "'a::t2_space" - shows "(\n. k) ----> l \ k = l" + shows "(\n. k) \ l \ k = l" using trivial_limit_sequentially by (rule tendsto_const_iff) lemma LIMSEQ_SUP: - "incseq X \ X ----> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})" + "incseq X \ X \ (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 \ X ----> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})" + "decseq X \ X \ (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 \ (\n. f (n + k)) ----> a" + "f \ a \ (\n. f (n + k)) \ a" unfolding tendsto_def by (subst eventually_sequentially_seg[where k=k]) lemma LIMSEQ_offset: - "(\n. f (n + k)) ----> a \ f ----> a" + "(\n. f (n + k)) \ a \ f \ a" unfolding tendsto_def by (subst (asm) eventually_sequentially_seg[where k=k]) -lemma LIMSEQ_Suc: "f ----> l \ (\n. f (Suc n)) ----> l" +lemma LIMSEQ_Suc: "f \ l \ (\n. f (Suc n)) \ l" by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) -lemma LIMSEQ_imp_Suc: "(\n. f (Suc n)) ----> l \ f ----> l" +lemma LIMSEQ_imp_Suc: "(\n. f (Suc n)) \ l \ f \ l" by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) -lemma LIMSEQ_Suc_iff: "(\n. f (Suc n)) ----> l = f ----> l" +lemma LIMSEQ_Suc_iff: "(\n. f (Suc n)) \ l = f \ l" by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) lemma LIMSEQ_unique: fixes a b :: "'a::t2_space" - shows "\X ----> a; X ----> b\ \ a = b" + shows "\X \ a; X \ b\ \ a = b" using trivial_limit_sequentially by (rule tendsto_unique) lemma LIMSEQ_le_const: - "\X ----> (x::'a::linorder_topology); \N. \n\N. a \ X n\ \ a \ x" + "\X \ (x::'a::linorder_topology); \N. \n\N. a \ X n\ \ a \ x" using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially) lemma LIMSEQ_le: - "\X ----> x; Y ----> y; \N. \n\N. X n \ Y n\ \ x \ (y::'a::linorder_topology)" + "\X \ x; Y \ y; \N. \n\N. X n \ Y n\ \ x \ (y::'a::linorder_topology)" using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially) lemma LIMSEQ_le_const2: - "\X ----> (x::'a::linorder_topology); \N. \n\N. X n \ a\ \ x \ a" + "\X \ (x::'a::linorder_topology); \N. \n\N. X n \ a\ \ x \ a" by (rule LIMSEQ_le[of X x "\n. a"]) auto -lemma convergentD: "convergent X ==> \L. (X ----> L)" +lemma convergentD: "convergent X ==> \L. (X \ L)" by (simp add: convergent_def) -lemma convergentI: "(X ----> L) ==> convergent X" +lemma convergentI: "(X \ 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 \ lim X)" by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) lemma convergent_const: "convergent (\n. c)" by (rule convergentI, rule tendsto_const) lemma monoseq_le: - "monoseq a \ a ----> (x::'a::linorder_topology) \ + "monoseq a \ a \ (x::'a::linorder_topology) \ ((\ n. a n \ x) \ (\m. \n\m. a m \ a n)) \ ((\ n. x \ a n) \ (\m. \n\m. a n \ a m))" by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff) lemma LIMSEQ_subseq_LIMSEQ: - "\ X ----> L; subseq f \ \ (X o f) ----> L" + "\ X \ L; subseq f \ \ (X o f) \ L" unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq]) lemma convergent_subseq_convergent: "\convergent X; subseq f\ \ convergent (X o f)" unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ) -lemma limI: "X ----> L ==> lim X = L" +lemma limI: "X \ L ==> lim X = L" by (rule tendsto_Lim) (rule trivial_limit_sequentially) lemma lim_le: "convergent f \ (\n. f n \ (x::'a::linorder_topology)) \ lim f \ x" @@ -1078,10 +1078,10 @@ subsubsection\Increasing and Decreasing Series\ -lemma incseq_le: "incseq X \ X ----> L \ X n \ (L::'a::linorder_topology)" +lemma incseq_le: "incseq X \ X \ L \ X n \ (L::'a::linorder_topology)" by (metis incseq_def LIMSEQ_le_const) -lemma decseq_le: "decseq X \ X ----> L \ (L::'a::linorder_topology) \ X n" +lemma decseq_le: "decseq X \ X \ L \ (L::'a::linorder_topology) \ X n" by (metis decseq_def LIMSEQ_le_const2) subsection \First countable topologies\ @@ -1142,7 +1142,7 @@ lemma (in first_countable_topology) countable_basis: obtains A :: "nat \ 'a set" where "\i. open (A i)" "\i. x \ A i" - "\F. (\n. F n \ A n) \ F ----> x" + "\F. (\n. F n \ A n) \ F \ x" proof atomize_elim obtain A :: "nat \ 'a set" where A: "\i. open (A i)" @@ -1154,25 +1154,25 @@ with A(3)[of S] have "eventually (\n. F n \ S) sequentially" by (auto elim: eventually_mono simp: subset_eq) } - with A show "\A. (\i. open (A i)) \ (\i. x \ A i) \ (\F. (\n. F n \ A n) \ F ----> x)" + with A show "\A. (\i. open (A i)) \ (\i. x \ A i) \ (\F. (\n. F n \ A n) \ F \ x)" by (intro exI[of _ A]) (auto simp: tendsto_def) qed lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within: - assumes "\f. (\n. f n \ s) \ f ----> a \ eventually (\n. P (f n)) sequentially" + assumes "\f. (\n. f n \ s) \ f \ a \ eventually (\n. P (f n)) sequentially" shows "eventually P (inf (nhds a) (principal s))" proof (rule ccontr) obtain A :: "nat \ 'a set" where A: "\i. open (A i)" "\i. a \ A i" - "\F. \n. F n \ A n \ F ----> a" + "\F. \n. F n \ A n \ F \ a" by (rule countable_basis) blast assume "\ ?thesis" with A have P: "\F. \n. F n \ s \ F n \ A n \ \ P (F n)" unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce then obtain F where F0: "\n. F n \ s" and F2: "\n. F n \ A n" and F3: "\n. \ P (F n)" by blast - with A have "F ----> a" by auto + with A have "F \ a" by auto hence "eventually (\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)) \ - (\f. (\n. f n \ s) \ f ----> a \ eventually (\n. P (f n)) sequentially)" + (\f. (\n. f n \ s) \ f \ a \ eventually (\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 \ S" "\x\S. x \ s \ P x" by (auto simp: eventually_inf_principal eventually_nhds) - moreover fix f assume "\n. f n \ s" "f ----> a" + moreover fix f assume "\n. f n \ s" "f \ a" ultimately show "eventually (\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) \ (\f. f ----> a \ eventually (\n. P (f n)) sequentially)" + "eventually P (nhds a) \ (\f. f \ a \ eventually (\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 \ _" - shows "(f ---> a) (at x within s) \ (\X. (\i. X i \ s - {x}) \ X ----> x \ ((f \ X) ----> a))" + shows "(f ---> a) (at x within s) \ (\X. (\i. X i \ s - {x}) \ X \ x \ ((f \ X) \ a))" unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap at_within_def eventually_nhds_within_iff_sequentially comp_def by metis @@ -1269,39 +1269,39 @@ subsubsection \Relation of LIM and LIMSEQ\ lemma (in first_countable_topology) sequentially_imp_eventually_within: - "(\f. (\n. f n \ s \ f n \ a) \ f ----> a \ eventually (\n. P (f n)) sequentially) \ + "(\f. (\n. f n \ s \ f n \ a) \ f \ a \ eventually (\n. P (f n)) sequentially) \ 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: - "(\f. (\n. f n \ a) \ f ----> a \ eventually (\n. P (f n)) sequentially) \ eventually P (at a)" + "(\f. (\n. f n \ a) \ f \ a \ eventually (\n. P (f n)) sequentially) \ eventually P (at a)" using assms sequentially_imp_eventually_within [where s=UNIV] by simp lemma LIMSEQ_SEQ_conv1: fixes f :: "'a::topological_space \ 'b::topological_space" assumes f: "f -- a --> l" - shows "\S. (\n. S n \ a) \ S ----> a \ (\n. f (S n)) ----> l" + shows "\S. (\n. S n \ a) \ S \ a \ (\n. f (S n)) \ l" using tendsto_compose_eventually [OF f, where F=sequentially] by simp lemma LIMSEQ_SEQ_conv2: fixes f :: "'a::first_countable_topology \ 'b::topological_space" - assumes "\S. (\n. S n \ a) \ S ----> a \ (\n. f (S n)) ----> l" + assumes "\S. (\n. S n \ a) \ S \ a \ (\n. f (S n)) \ l" shows "f -- a --> l" using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at) lemma LIMSEQ_SEQ_conv: - "(\S. (\n. S n \ a) \ S ----> (a::'a::first_countable_topology) \ (\n. X (S n)) ----> L) = + "(\S. (\n. S n \ a) \ S \ (a::'a::first_countable_topology) \ (\n. X (S n)) \ 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 *: "\f. (\n. b < f n) \ (\n. f n < a) \ incseq f \ f ----> a \ eventually (\n. P (f n)) sequentially" + assumes *: "\f. (\n. b < f n) \ (\n. f n < a) \ incseq f \ f \ a \ eventually (\n. P (f n)) sequentially" shows "eventually P (at_left a)" proof (safe intro!: sequentially_imp_eventually_within) - fix X assume X: "\n. X n \ {..< a} \ X n \ a" "X ----> a" + fix X assume X: "\n. X n \ {..< a} \ X n \ a" "X \ a" show "eventually (\n. P (X n)) sequentially" proof (rule ccontr) assume neg: "\ eventually (\n. P (X n)) sequentially" @@ -1319,8 +1319,8 @@ by (auto dest!: not_eventuallyD) qed then guess s .. - then have "\n. b < X (s n)" "\n. X (s n) < a" "incseq (\n. X (s n))" "(\n. X (s n)) ----> a" "\n. \ P (X (s n))" - using X by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \X ----> a\, unfolded comp_def]) + then have "\n. b < X (s n)" "\n. X (s n) < a" "incseq (\n. X (s n))" "(\n. X (s n)) \ a" "\n. \ P (X (s n))" + using X by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \X \ a\, 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 *: "\S. (\n. S n < a) \ (\n. b < S n) \ incseq S \ S ----> a \ (\n. X (S n)) ----> L" + assumes *: "\S. (\n. S n < a) \ (\n. b < S n) \ incseq S \ S \ a \ (\n. X (S n)) \ L" shows "(X ---> L) (at_left a)" 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 *: "\f. (\n. a < f n) \ (\n. f n < b) \ decseq f \ f ----> a \ eventually (\n. P (f n)) sequentially" + assumes *: "\f. (\n. a < f n) \ (\n. f n < b) \ decseq f \ f \ a \ eventually (\n. P (f n)) sequentially" shows "eventually P (at_right a)" proof (safe intro!: sequentially_imp_eventually_within) - fix X assume X: "\n. X n \ {a <..} \ X n \ a" "X ----> a" + fix X assume X: "\n. X n \ {a <..} \ X n \ a" "X \ a" show "eventually (\n. P (X n)) sequentially" proof (rule ccontr) assume neg: "\ eventually (\n. P (X n)) sequentially" @@ -1357,8 +1357,8 @@ by (auto dest!: not_eventuallyD) qed then guess s .. - then have "\n. a < X (s n)" "\n. X (s n) < b" "decseq (\n. X (s n))" "(\n. X (s n)) ----> a" "\n. \ P (X (s n))" - using X by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \X ----> a\, unfolded comp_def]) + then have "\n. a < X (s n)" "\n. X (s n) < b" "decseq (\n. X (s n))" "(\n. X (s n)) \ a" "\n. \ P (X (s n))" + using X by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \X \ a\, 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 *: "\S. (\n. a < S n) \ (\n. S n < b) \ decseq S \ S ----> a \ (\n. X (S n)) ----> L" + assumes *: "\S. (\n. a < S n) \ (\n. S n < b) \ decseq S \ S \ a \ (\n. X (S n)) \ L" shows "(X ---> L) (at_right a)" using assms unfolding tendsto_def [where l=L] by (simp add: sequentially_imp_eventually_at_right) diff -r e13e70f32407 -r e01015e49041 src/HOL/Transcendental.thy --- 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 \ 'a::banach" - assumes f: "(\n. root n (norm (f n))) ----> x" \ "could be weakened to lim sup" + assumes f: "(\n. root n (norm (f n))) \ x" \ "could be weakened to lim sup" assumes "x < 1" shows "summable f" proof - @@ -92,7 +92,7 @@ shows "summable (\n. norm (f n * z ^ n))" proof - from 2 have x_neq_0: "x \ 0" by clarsimp - from 1 have "(\n. f n * x^n) ----> 0" + from 1 have "(\n. f n * x^n) \ 0" by (rule summable_LIMSEQ_zero) hence "convergent (\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 "(\n. of_nat n * x ^ n) ----> 0" + shows "(\n. of_nat n * x ^ n) \ 0" proof - have "norm x / (1 - norm x) \ 0" using assms @@ -270,9 +270,9 @@ lemma sums_alternating_upper_lower: fixes a :: "nat \ real" - assumes mono: "\n. a (Suc n) \ a n" and a_pos: "\n. 0 \ a n" and "a ----> 0" - shows "\l. ((\n. (\i<2*n. (- 1)^i*a i) \ l) \ (\ n. \i<2*n. (- 1)^i*a i) ----> l) \ - ((\n. l \ (\i<2*n + 1. (- 1)^i*a i)) \ (\ n. \i<2*n + 1. (- 1)^i*a i) ----> l)" + assumes mono: "\n. a (Suc n) \ a n" and a_pos: "\n. 0 \ a n" and "a \ 0" + shows "\l. ((\n. (\i<2*n. (- 1)^i*a i) \ l) \ (\ n. \i<2*n. (- 1)^i*a i) \ l) \ + ((\n. l \ (\i<2*n + 1. (- 1)^i*a i)) \ (\ n. \i<2*n + 1. (- 1)^i*a i) \ l)" (is "\l. ((\n. ?f n \ l) \ _) \ ((\n. l \ ?g n) \ _)") proof (rule nested_sequence_unique) have fg_diff: "\n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto @@ -294,11 +294,11 @@ show "?f n \ ?g n" using fg_diff a_pos unfolding One_nat_def by auto qed - show "(\n. ?f n - ?g n) ----> 0" unfolding fg_diff + show "(\n. ?f n - ?g n) \ 0" unfolding fg_diff proof (rule LIMSEQ_I) fix r :: real assume "0 < r" - with \a ----> 0\[THEN LIMSEQ_D] obtain N where "\ n. n \ N \ norm (a n - 0) < r" + with \a \ 0\[THEN LIMSEQ_D] obtain N where "\ n. n \ N \ norm (a n - 0) < r" by auto hence "\n \ N. norm (- a (2 * n) - 0) < r" by auto thus "\N. \n \ N. norm (- a (2 * n) - 0) < r" by auto @@ -307,14 +307,14 @@ lemma summable_Leibniz': fixes a :: "nat \ real" - assumes a_zero: "a ----> 0" + assumes a_zero: "a \ 0" and a_pos: "\ n. 0 \ a n" and a_monotone: "\ n. a (Suc n) \ a n" shows summable: "summable (\ n. (-1)^n * a n)" and "\n. (\i<2*n. (-1)^i*a i) \ (\i. (-1)^i*a i)" - and "(\n. \i<2*n. (-1)^i*a i) ----> (\i. (-1)^i*a i)" + and "(\n. \i<2*n. (-1)^i*a i) \ (\i. (-1)^i*a i)" and "\n. (\i. (-1)^i*a i) \ (\i<2*n+1. (-1)^i*a i)" - and "(\n. \i<2*n+1. (-1)^i*a i) ----> (\i. (-1)^i*a i)" + and "(\n. \i<2*n+1. (-1)^i*a i) \ (\i. (-1)^i*a i)" proof - let ?S = "\n. (-1)^n * a n" let ?P = "\n. \i n. ?f n \ l" - and "?f ----> l" + and "?f \ l" and above_l: "\ n. l \ ?g n" - and "?g ----> l" + and "?g \ l" using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast let ?Sa = "\m. \n l" + have "?Sa \ l" proof (rule LIMSEQ_I) fix r :: real assume "0 < r" - with \?f ----> l\[THEN LIMSEQ_D] + with \?f \ l\[THEN LIMSEQ_D] obtain f_no where f: "\ n. n \ f_no \ norm (?f n - l) < r" by auto - from \0 < r\ \?g ----> l\[THEN LIMSEQ_D] + from \0 < r\ \?g \ l\[THEN LIMSEQ_D] obtain g_no where g: "\ n. n \ g_no \ 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 \ suminf ?S" unfolding sums_unique[OF sums_l, symmetric] using below_l by auto - show "?g ----> suminf ?S" - using \?g ----> l\ \l = suminf ?S\ by auto - show "?f ----> suminf ?S" - using \?f ----> l\ \l = suminf ?S\ by auto + show "?g \ suminf ?S" + using \?g \ l\ \l = suminf ?S\ by auto + show "?f \ suminf ?S" + using \?f \ l\ \l = suminf ?S\ by auto qed theorem summable_Leibniz: fixes a :: "nat \ real" - assumes a_zero: "a ----> 0" and "monoseq a" + assumes a_zero: "a \ 0" and "monoseq a" shows "summable (\ n. (-1)^n * a n)" (is "?summable") and "0 < a 0 \ (\n. (\i. (- 1)^i*a i) \ { \i<2*n. (- 1)^i * a i .. \i<2*n+1. (- 1)^i * a i})" (is "?pos") and "a 0 < 0 \ (\n. (\i. (- 1)^i*a i) \ { \i<2*n+1. (- 1)^i * a i .. \i<2*n. (- 1)^i * a i})" (is "?neg") - and "(\n. \i<2*n. (- 1)^i*a i) ----> (\i. (- 1)^i*a i)" (is "?f") - and "(\n. \i<2*n+1. (- 1)^i*a i) ----> (\i. (- 1)^i*a i)" (is "?g") + and "(\n. \i<2*n. (- 1)^i*a i) \ (\i. (- 1)^i*a i)" (is "?f") + and "(\n. \i<2*n+1. (- 1)^i*a i) \ (\i. (- 1)^i*a i)" (is "?g") proof - have "?summable \ ?pos \ ?neg \ ?f \ ?g" proof (cases "(\ n. 0 \ a n) \ (\m. \n\m. a n \ a m)") @@ -404,13 +404,13 @@ have "a (Suc n) \ a n" using ord[where n="Suc n" and m=n] by auto } note mono = this - note leibniz = summable_Leibniz'[OF \a ----> 0\ ge0] + note leibniz = summable_Leibniz'[OF \a \ 0\ ge0] from leibniz[OF mono] show ?thesis using \0 \ a 0\ by auto next let ?a = "\ n. - a n" case False - with monoseq_le[OF \monoseq a\ \a ----> 0\] + with monoseq_le[OF \monoseq a\ \a \ 0\] have "(\ n. a n \ 0) \ (\m. \n\m. a m \ a n)" by auto hence ord: "\n m. m \ n \ ?a n \ ?a m" and ge0: "\ n. 0 \ ?a n" by auto @@ -421,7 +421,7 @@ } note monotone = this note leibniz = summable_Leibniz'[OF _ ge0, of "\x. x", - OF tendsto_minus[OF \a ----> 0\, unfolded minus_zero] monotone] + OF tendsto_minus[OF \a \ 0\, unfolded minus_zero] monotone] have "summable (\ n. (-1)^n * ?a n)" using leibniz(1) by auto then obtain l where "(\ 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 "(\n. of_nat n * (x / of_real r) ^ n) ----> 0" + have "(\n. of_nat n * (x / of_real r) ^ n) \ 0" using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"]) then obtain N where N: "\n. n\N \ 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 "(\n. (1 + x / n) ^ n) ----> exp x" + shows "(\n. (1 + x / n) ^ n) \ exp x" proof (rule filterlim_mono_eventually) from reals_Archimedean2 [of "\x\"] obtain n :: nat where *: "real n > \x\" .. hence "eventually (\n :: nat. 0 < 1 + x / real n) at_top" @@ -2658,7 +2658,7 @@ done then show "eventually (\n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top" by (rule eventually_mono) (erule powr_realpow) - show "(\n. (1 + x / real n) powr real n) ----> exp x" + show "(\n. (1 + x / real n) powr real n) \ 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 "\x\ \ 1" - shows "(\ n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0") + shows "(\ n. 1 / real (n*2+1) * x^(n*2+1)) \ 0" (is "?a \ 0") proof (cases "x = 0") case True thus ?thesis @@ -4994,12 +4994,12 @@ next case False have "norm x \ 1" and "x \ 1" and "-1 \ x" using assms by auto - show "?a ----> 0" + show "?a \ 0" proof (cases "\x\ < 1") case True hence "norm x < 1" by auto from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF \norm x < 1\, THEN LIMSEQ_Suc]] - have "(\n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0" + have "(\n. 1 / real (n + 1) * x ^ (n + 1)) \ 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 \ ?a 1 n" by auto } - have "?a 1 ----> 0" + have "?a 1 \ 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 \ 0" proof (rule LIMSEQ_I) fix r :: real assume "0 < r" obtain N :: nat where N_I: "\n. N \ n \ ?a 1 n < r" - using LIMSEQ_D[OF \?a 1 ----> 0\ \0 < r\] by auto + using LIMSEQ_D[OF \?a 1 \ 0\ \0 < r\] by auto { fix n assume "N \ n" from \?diff 1 n \ ?a 1 n\ N_I[OF this]