--- a/src/HOL/Analysis/Bochner_Integration.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Aug 17 14:52:56 2017 +0200
@@ -2128,7 +2128,7 @@
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes [measurable]: "\<And>n. integrable M (u n)"
and "(\<lambda>n. (\<integral>x. norm(u n x) \<partial>M)) \<longlonglongrightarrow> 0"
- shows "\<exists>r. subseq r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
proof -
{
fix k
@@ -2140,13 +2140,13 @@
}
then have "\<exists>r. \<forall>n. True \<and> (r (Suc n) > r n \<and> (\<integral>x. norm(u (r (Suc n)) x) \<partial>M) < (1/2)^(r n))"
by (intro dependent_nat_choice, auto)
- then obtain r0 where r0: "subseq r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
- by (auto simp: subseq_Suc_iff)
+ then obtain r0 where r0: "strict_mono r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
+ by (auto simp: strict_mono_Suc_iff)
define r where "r = (\<lambda>n. r0(n+1))"
- have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
+ have "strict_mono r" unfolding r_def using r0(1) by (simp add: strict_mono_Suc_iff)
have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
proof -
- have "r0 n \<ge> n" using \<open>subseq r0\<close> by (simp add: seq_suble)
+ have "r0 n \<ge> n" using \<open>strict_mono r0\<close> by (simp add: seq_suble)
have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
@@ -2219,7 +2219,7 @@
by (simp add: tendsto_norm_zero_iff)
}
ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
- then show ?thesis using \<open>subseq r\<close> by auto
+ then show ?thesis using \<open>strict_mono r\<close> by auto
qed
subsection \<open>Restricted measure spaces\<close>
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Aug 17 14:52:56 2017 +0200
@@ -476,8 +476,8 @@
lemma compact_blinfun_lemma:
fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
assumes "bounded (range f)"
- shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
- subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
+ shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r::nat\<Rightarrow>nat.
+ strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"])
(auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta sum.delta'
@@ -501,7 +501,7 @@
proof
fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
assume f: "bounded (range f)"
- then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "subseq r"
+ then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "strict_mono r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e) sequentially"
using compact_blinfun_lemma [OF f] by blast
{
@@ -545,7 +545,7 @@
}
then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
by auto
qed
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Aug 17 14:52:56 2017 +0200
@@ -957,7 +957,7 @@
lemma compact_lemma_cart:
fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
assumes f: "bounded (range f)"
- shows "\<exists>l r. subseq r \<and>
+ shows "\<exists>l r. strict_mono r \<and>
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
(is "?th d")
proof -
@@ -971,7 +971,7 @@
proof
fix f :: "nat \<Rightarrow> 'a ^ 'b"
assume f: "bounded (range f)"
- then obtain l r where r: "subseq r"
+ then obtain l r where r: "strict_mono r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
using compact_lemma_cart [OF f] by blast
let ?d = "UNIV::'b set"
@@ -993,7 +993,7 @@
by (rule eventually_mono)
}
hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
+ with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
qed
lemma interval_cart:
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Aug 17 14:52:56 2017 +0200
@@ -2420,7 +2420,7 @@
intro!: mult_pos_pos divide_pos_pos always_eventually)
thus "summable (\<lambda>n. g n * u^n)"
by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
- (auto simp: power_mult subseq_def g_def h_def elim!: oddE)
+ (auto simp: power_mult strict_mono_def g_def h_def elim!: oddE)
qed (simp add: h_def)
have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
@@ -2436,7 +2436,7 @@
by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
- (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
+ (auto elim!: evenE simp: strict_mono_def power_mult power_mult_distrib)
also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
@@ -2450,7 +2450,7 @@
with c z have "Arctan z = G z" by simp
with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
- (auto elim!: oddE simp: subseq_def power_mult g_def h_def)
+ (auto elim!: oddE simp: strict_mono_def power_mult g_def h_def)
qed
text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>
--- a/src/HOL/Analysis/Gamma_Function.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Thu Aug 17 14:52:56 2017 +0200
@@ -101,7 +101,7 @@
also have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z \<longleftrightarrow>
(\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z"
by (subst sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
- (auto simp: sin_coeff_def subseq_def ac_simps elim!: oddE)
+ (auto simp: sin_coeff_def strict_mono_def ac_simps elim!: oddE)
finally show ?thesis .
qed
@@ -111,7 +111,7 @@
also have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z \<longleftrightarrow>
(\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z"
by (subst sums_mono_reindex[of "\<lambda>n. 2*n", symmetric])
- (auto simp: cos_coeff_def subseq_def ac_simps elim!: evenE)
+ (auto simp: cos_coeff_def strict_mono_def ac_simps elim!: evenE)
finally show ?thesis .
qed
@@ -2038,7 +2038,7 @@
hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"]
by (intro tendsto_intros Gamma_series'_LIMSEQ)
- (simp_all add: o_def subseq_def Gamma_eq_zero_iff)
+ (simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
by (rule Lim_transform_eventually)
} note lim = this
--- a/src/HOL/Analysis/Great_Picard.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy Thu Aug 17 14:52:56 2017 +0200
@@ -618,22 +618,22 @@
lemma subsequence_diagonalization_lemma:
fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
- assumes sub: "\<And>i r. \<exists>k. subseq k \<and> P i (r \<circ> k)"
+ assumes sub: "\<And>i r. \<exists>k. strict_mono (k :: nat \<Rightarrow> nat) \<and> P i (r \<circ> k)"
and P_P: "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N.
\<lbrakk>P i (r \<circ> k1); \<And>j. N \<le> j \<Longrightarrow> \<exists>j'. j \<le> j' \<and> k2 j = k1 j'\<rbrakk> \<Longrightarrow> P i (r \<circ> k2)"
- obtains k where "subseq k" "\<And>i. P i (r \<circ> k)"
+ obtains k where "strict_mono (k :: nat \<Rightarrow> nat)" "\<And>i. P i (r \<circ> k)"
proof -
- obtain kk where "\<And>i r. subseq (kk i r) \<and> P i (r \<circ> (kk i r))"
+ obtain kk where "\<And>i r. strict_mono (kk i r :: nat \<Rightarrow> nat) \<and> P i (r \<circ> (kk i r))"
using sub by metis
- then have sub_kk: "\<And>i r. subseq (kk i r)" and P_kk: "\<And>i r. P i (r \<circ> (kk i r))"
+ then have sub_kk: "\<And>i r. strict_mono (kk i r)" and P_kk: "\<And>i r. P i (r \<circ> (kk i r))"
by auto
define rr where "rr \<equiv> rec_nat (kk 0 r) (\<lambda>n x. x \<circ> kk (Suc n) (r \<circ> x))"
then have [simp]: "rr 0 = kk 0 r" "\<And>n. rr(Suc n) = rr n \<circ> kk (Suc n) (r \<circ> rr n)"
by auto
show thesis
proof
- have sub_rr: "subseq (rr i)" for i
- using sub_kk by (induction i) (auto simp: subseq_def o_def)
+ have sub_rr: "strict_mono (rr i)" for i
+ using sub_kk by (induction i) (auto simp: strict_mono_def o_def)
have P_rr: "P i (r \<circ> rr i)" for i
using P_kk by (induction i) (auto simp: o_def)
have "i \<le> i+d \<Longrightarrow> rr i n \<le> rr (i+d) n" for d i n
@@ -643,13 +643,13 @@
next
case (Suc d) then show ?case
apply simp
- using seq_suble [OF sub_kk] order_trans subseq_le_mono [OF sub_rr] by blast
+ using seq_suble [OF sub_kk] order_trans strict_mono_less_eq [OF sub_rr] by blast
qed
then have "\<And>i j n. i \<le> j \<Longrightarrow> rr i n \<le> rr j n"
by (metis le_iff_add)
- show "subseq (\<lambda>n. rr n n)"
- apply (simp add: subseq_Suc_iff)
- by (meson Suc_le_eq seq_suble sub_kk sub_rr subseq_mono)
+ show "strict_mono (\<lambda>n. rr n n)"
+ apply (simp add: strict_mono_Suc_iff)
+ by (meson lessI less_le_trans seq_suble strict_monoD sub_kk sub_rr)
have "\<exists>j. i \<le> j \<and> rr (n+d) i = rr n j" for d n i
apply (induction d arbitrary: i, auto)
by (meson order_trans seq_suble sub_kk)
@@ -663,19 +663,19 @@
lemma function_convergent_subsequence:
fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M"
- obtains k where "subseq k" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
+ obtains k where "strict_mono (k::nat\<Rightarrow>nat)" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
proof (cases "S = {}")
case True
then show ?thesis
- using subseq_id that by fastforce
+ using strict_mono_id that by fastforce
next
case False
with \<open>countable S\<close> obtain \<sigma> :: "nat \<Rightarrow> 'a" where \<sigma>: "S = range \<sigma>"
using uncountable_def by blast
- obtain k where "subseq k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l"
+ obtain k where "strict_mono k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l"
proof (rule subsequence_diagonalization_lemma
[of "\<lambda>i r. \<exists>l. ((\<lambda>n. (f \<circ> r) n (\<sigma> i)) \<longlongrightarrow> l) sequentially" id])
- show "\<exists>k. subseq k \<and> (\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k)) n (\<sigma> i)) \<longlonglongrightarrow> l)" for i r
+ show "\<exists>k::nat\<Rightarrow>nat. strict_mono k \<and> (\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k)) n (\<sigma> i)) \<longlonglongrightarrow> l)" for i r
proof -
have "f (r n) (\<sigma> i) \<in> cball 0 M" for n
by (simp add: \<sigma> M)
@@ -705,7 +705,7 @@
and equicont:
"\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk>
\<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n y. y \<in> S \<and> norm(x - y) < d \<longrightarrow> norm(\<F> n x - \<F> n y) < e)"
- obtains g k where "continuous_on S g" "subseq k"
+ obtains g k where "continuous_on S g" "strict_mono (k :: nat \<Rightarrow> nat)"
"\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(k n) x - g x) < e"
proof -
have UEQ: "\<And>e. 0 < e \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n. \<forall>x \<in> S. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (\<F> n x') (\<F> n x) < e)"
@@ -727,7 +727,7 @@
moreover
obtain R where "countable R" "R \<subseteq> S" and SR: "S \<subseteq> closure R"
by (metis separable that)
- obtain k where "subseq k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
+ obtain k where "strict_mono k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
apply (rule function_convergent_subsequence [OF \<open>countable R\<close> M])
using \<open>R \<subseteq> S\<close> apply force+
done
@@ -783,7 +783,7 @@
apply (simp add: o_def dist_norm)
by meson
ultimately show thesis
- by (metis that \<open>subseq k\<close>)
+ by (metis that \<open>strict_mono k\<close>)
qed
@@ -802,7 +802,7 @@
and bounded: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>B. \<forall>h \<in> \<H>. \<forall> z \<in> K. norm(h z) \<le> B"
and rng_f: "range \<F> \<subseteq> \<H>"
obtains g r
- where "g holomorphic_on S" "subseq r"
+ where "g holomorphic_on S" "strict_mono (r :: nat \<Rightarrow> nat)"
"\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially"
"\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially"
proof -
@@ -813,10 +813,10 @@
by (simp add: bounded)
then obtain B where B: "\<And>i h z. \<lbrakk>h \<in> \<H>; z \<in> K i\<rbrakk> \<Longrightarrow> norm(h z) \<le> B i"
by metis
- have *: "\<exists>r g. subseq r \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r) n x - g x) < e)"
+ have *: "\<exists>r g. strict_mono (r::nat\<Rightarrow>nat) \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r) n x - g x) < e)"
if "\<And>n. \<F> n \<in> \<H>" for \<F> i
proof -
- obtain g k where "continuous_on (K i) g" "subseq k"
+ obtain g k where "continuous_on (K i) g" "strict_mono (k::nat\<Rightarrow>nat)"
"\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm(\<F>(k n) x - g x) < e"
proof (rule Arzela_Ascoli [of "K i" "\<F>" "B i"])
show "\<exists>d>0. \<forall>n y. y \<in> K i \<and> cmod (z - y) < d \<longrightarrow> cmod (\<F> n z - \<F> n y) < e"
@@ -925,13 +925,13 @@
then show ?thesis
by fastforce
qed
- have "\<exists>k g. subseq k \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r \<circ> k) n x - g x) < e)"
+ have "\<exists>k g. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r \<circ> k) n x - g x) < e)"
for i r
apply (rule *)
using rng_f by auto
- then have **: "\<And>i r. \<exists>k. subseq k \<and> (\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> (r \<circ> k)) n x - g x) < e)"
+ then have **: "\<And>i r. \<exists>k. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> (r \<circ> k)) n x - g x) < e)"
by (force simp: o_assoc)
- obtain k where "subseq k"
+ obtain k :: "nat \<Rightarrow> nat" where "strict_mono k"
and "\<And>i. \<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> (id \<circ> k)) n x - g x) < e"
apply (rule subsequence_diagonalization_lemma [OF **, of id])
apply (erule ex_forward all_forward imp_forward)+
@@ -988,7 +988,7 @@
with d show ?thesis by blast
qed
qed
- qed (auto simp: \<open>subseq k\<close>)
+ qed (auto simp: \<open>strict_mono k\<close>)
qed
@@ -1332,7 +1332,7 @@
using hol\<G> \<G>not0 \<G>not1 \<G>_le1 by (force simp: W_def)+
then obtain e where "e > 0" and e: "ball v e \<subseteq> Z"
by (meson open_contains_ball)
- obtain h j where holh: "h holomorphic_on ball v e" and "subseq j"
+ obtain h j where holh: "h holomorphic_on ball v e" and "strict_mono j"
and lim: "\<And>x. x \<in> ball v e \<Longrightarrow> (\<lambda>n. \<G> (j n) x) \<longlonglongrightarrow> h x"
and ulim: "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk>
\<Longrightarrow> uniform_limit K (\<G> \<circ> j) h sequentially"
@@ -1347,7 +1347,7 @@
show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> h v"
using \<open>e > 0\<close> lim by simp
have lt_Fj: "real x \<le> cmod (\<F> (j x) v)" for x
- by (metis of_nat_Suc ltF \<open>subseq j\<close> add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble)
+ by (metis of_nat_Suc ltF \<open>strict_mono j\<close> add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble)
show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> 0"
proof (rule Lim_null_comparison [OF eventually_sequentiallyI seq_harmonic])
show "cmod (\<G> (j x) v) \<le> inverse (real x)" if "1 \<le> x" for x
@@ -1428,8 +1428,8 @@
qed
with that show ?thesis by metis
qed
-
-
+
+
lemma GPicard4:
assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})"
and AE: "\<And>e. \<lbrakk>0 < e; e < k\<rbrakk> \<Longrightarrow> \<exists>d. 0 < d \<and> d < e \<and> (\<forall>z \<in> sphere 0 d. norm(f z) \<le> B)"
@@ -1500,7 +1500,8 @@
then show ?thesis
proof cases
case 1
- with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}"
+ with infinite_enumerate obtain r :: "nat \<Rightarrow> nat"
+ where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}"
by blast
obtain B where B: "\<And>j z. \<lbrakk>norm z = 1/2; j \<in> range (h \<circ> r)\<rbrakk> \<Longrightarrow> norm(j z) \<le> B"
proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])
@@ -1529,7 +1530,7 @@
obtain n where "(1/e - 2) / 2 < real n"
using reals_Archimedean2 by blast
also have "... \<le> r n"
- using \<open>subseq r\<close> by (simp add: seq_suble)
+ using \<open>strict_mono r\<close> by (simp add: seq_suble)
finally have "(1/e - 2) / 2 < real (r n)" .
with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
by (simp add: field_simps)
@@ -1546,7 +1547,8 @@
using \<epsilon> by auto
next
case 2
- with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}"
+ with infinite_enumerate obtain r :: "nat \<Rightarrow> nat"
+ where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}"
by blast
obtain B where B: "\<And>j z. \<lbrakk>norm z = 1/2; j \<in> range (\<lambda>n. inverse \<circ> h (r n))\<rbrakk> \<Longrightarrow> norm(j z) \<le> B"
proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])
@@ -1579,7 +1581,7 @@
obtain n where "(1/e - 2) / 2 < real n"
using reals_Archimedean2 by blast
also have "... \<le> r n"
- using \<open>subseq r\<close> by (simp add: seq_suble)
+ using \<open>strict_mono r\<close> by (simp add: seq_suble)
finally have "(1/e - 2) / 2 < real (r n)" .
with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
by (simp add: field_simps)
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Thu Aug 17 14:52:56 2017 +0200
@@ -215,7 +215,7 @@
moreover have "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real))
\<longlonglongrightarrow> euler_mascheroni - euler_mascheroni + ln 2"
by (intro tendsto_intros euler_mascheroni_LIMSEQ filterlim_compose[OF euler_mascheroni_LIMSEQ]
- filterlim_subseq) (auto simp: subseq_def)
+ filterlim_subseq) (auto simp: strict_mono_def)
hence "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) \<longlonglongrightarrow> ln 2" by simp
ultimately have "(\<lambda>n. (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2"
by (rule Lim_transform_eventually)
@@ -227,7 +227,7 @@
by (simp add: summable_sums_iff divide_inverse sums_def)
from filterlim_compose[OF this filterlim_subseq[of "op * (2::nat)"]]
have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
- by (simp add: subseq_def)
+ by (simp add: strict_mono_def)
ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
with A show ?thesis by (simp add: sums_def)
qed
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Aug 17 14:52:56 2017 +0200
@@ -1757,8 +1757,8 @@
lemma infinite_enumerate:
assumes fS: "infinite S"
- shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
- unfolding subseq_def
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
+ unfolding strict_mono_def
using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
--- a/src/HOL/Analysis/Path_Connected.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Aug 17 14:52:56 2017 +0200
@@ -3305,7 +3305,8 @@
then have "\<And>n. \<exists>x \<in> S. \<xi> n = f x" by force
then obtain z where zs: "\<And>n. z n \<in> S" and fz: "\<And>n. \<xi> n = f (z n)"
by metis
- then obtain y K where y: "y \<in> closure S" and "subseq K" and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
+ then obtain y K where y: "y \<in> closure S" and "strict_mono (K :: nat \<Rightarrow> nat)"
+ and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
using \<open>bounded S\<close>
apply (simp add: compact_closure [symmetric] compact_def)
apply (drule_tac x=z in spec)
--- a/src/HOL/Analysis/Set_Integral.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Thu Aug 17 14:52:56 2017 +0200
@@ -193,22 +193,22 @@
lemma limsup_subseq_lim:
fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
- shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> limsup u"
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> limsup u"
proof (cases)
assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
by (intro dependent_nat_choice) (auto simp: conj_commute)
- then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
- by (auto simp: subseq_Suc_iff)
+ then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
+ by (auto simp: strict_mono_Suc_iff)
define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
- then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
+ then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
then have "umax o r = u o r" unfolding o_def by simp
then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
- then show ?thesis using \<open>subseq r\<close> by blast
+ then show ?thesis using \<open>strict_mono r\<close> by blast
next
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
@@ -262,16 +262,16 @@
then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
qed (auto)
then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))" by auto
- have "subseq r" using r by (auto simp: subseq_Suc_iff)
+ have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
- moreover have "limsup (u o r) \<le> limsup u" using \<open>subseq r\<close> by (simp add: limsup_subseq_mono)
+ moreover have "limsup (u o r) \<le> limsup u" using \<open>strict_mono r\<close> by (simp add: limsup_subseq_mono)
ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
{
fix i assume i: "i \<in> {N<..}"
- obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
+ obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
then have "i \<in> {N<..r(Suc n)}" using i by simp
then have "u i \<le> u (r(Suc n))" using r by simp
then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
@@ -281,27 +281,27 @@
by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
- then show ?thesis using \<open>subseq r\<close> by auto
+ then show ?thesis using \<open>strict_mono r\<close> by auto
qed
lemma liminf_subseq_lim:
fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
- shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> liminf u"
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> liminf u"
proof (cases)
assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
by (intro dependent_nat_choice) (auto simp: conj_commute)
- then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
- by (auto simp: subseq_Suc_iff)
+ then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
+ by (auto simp: strict_mono_Suc_iff)
define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
- then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
+ then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
then have "umin o r = u o r" unfolding o_def by simp
then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
- then show ?thesis using \<open>subseq r\<close> by blast
+ then show ?thesis using \<open>strict_mono r\<close> by blast
next
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
@@ -354,17 +354,18 @@
then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
qed (auto)
- then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
- have "subseq r" using r by (auto simp: subseq_Suc_iff)
+ then obtain r :: "nat \<Rightarrow> nat"
+ where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
+ have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
- moreover have "liminf (u o r) \<ge> liminf u" using \<open>subseq r\<close> by (simp add: liminf_subseq_mono)
+ moreover have "liminf (u o r) \<ge> liminf u" using \<open>strict_mono r\<close> by (simp add: liminf_subseq_mono)
ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
{
fix i assume i: "i \<in> {N<..}"
- obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
+ obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
then have "i \<in> {N<..r(Suc n)}" using i by simp
then have "u i \<ge> u (r(Suc n))" using r by simp
then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
@@ -374,7 +375,7 @@
by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
- then show ?thesis using \<open>subseq r\<close> by auto
+ then show ?thesis using \<open>strict_mono r\<close> by auto
qed
@@ -1076,12 +1077,12 @@
then have "limsup u < \<infinity>" "limsup v < \<infinity>" by auto
define w where "w = (\<lambda>n. u n + v n)"
- obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
- obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
- obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
+ obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
+ obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
+ obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
define a where "a = r o s o t"
- have "subseq a" using r s t by (simp add: a_def subseq_o)
+ have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
have l:"(w o a) \<longlonglongrightarrow> limsup w"
"(u o a) \<longlonglongrightarrow> limsup (u o r)"
"(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
@@ -1092,7 +1093,8 @@
have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
- have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
+ have "limsup (v o r o s) \<le> limsup v"
+ by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
@@ -1122,12 +1124,12 @@
then have "liminf u > -\<infinity>" "liminf v > -\<infinity>" by auto
define w where "w = (\<lambda>n. u n + v n)"
- obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
- obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
- obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> liminf (v o r o s)" using liminf_subseq_lim by auto
+ obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
+ obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
+ obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> liminf (v o r o s)" using liminf_subseq_lim by auto
define a where "a = r o s o t"
- have "subseq a" using r s t by (simp add: a_def subseq_o)
+ have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
have l:"(w o a) \<longlonglongrightarrow> liminf w"
"(u o a) \<longlonglongrightarrow> liminf (u o r)"
"(v o a) \<longlonglongrightarrow> liminf (v o r o s)"
@@ -1138,7 +1140,8 @@
have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
- have "liminf (v o r o s) \<ge> liminf v" by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) subseq_o)
+ have "liminf (v o r o s) \<ge> liminf v"
+ by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) strict_mono_o)
then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
@@ -1188,7 +1191,7 @@
shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
proof -
define w where "w = (\<lambda>n. u n * v n)"
- obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
+ obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * limsup v" using assms(2) assms(3) by auto
moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
@@ -1196,7 +1199,7 @@
then have "limsup (w o r) = a * limsup v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
then have I: "limsup w \<ge> a * limsup v" by (metis limsup_subseq_mono r(1))
- obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
+ obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
@@ -1218,7 +1221,7 @@
shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
proof -
define w where "w = (\<lambda>n. u n * v n)"
- obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
+ obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * liminf v" using assms(2) assms(3) by auto
moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
@@ -1226,7 +1229,7 @@
then have "liminf (w o r) = a * liminf v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
then have I: "liminf w \<le> a * liminf v" by (metis liminf_subseq_mono r(1))
- obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
+ obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
@@ -1286,12 +1289,12 @@
then have "limsup v < \<infinity>" "liminf u < \<infinity>" by auto
define w where "w = (\<lambda>n. u n + v n)"
- obtain r where r: "subseq r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
- obtain s where s: "subseq s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
- obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
+ obtain r where r: "strict_mono r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
+ obtain s where s: "strict_mono s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
+ obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
define a where "a = r o s o t"
- have "subseq a" using r s t by (simp add: a_def subseq_o)
+ have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
have l:"(u o a) \<longlonglongrightarrow> liminf u"
"(w o a) \<longlonglongrightarrow> liminf (w o r)"
"(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
@@ -1301,7 +1304,8 @@
done
have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
- have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
+ have "limsup (v o r o s) \<le> limsup v"
+ by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
--- a/src/HOL/Analysis/Summation_Tests.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy Thu Aug 17 14:52:56 2017 +0200
@@ -189,7 +189,7 @@
also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<n. f k)" unfolding f'_def by simp
also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
by (rule nonneg_incseq_Bseq_subseq_iff[symmetric])
- (auto intro!: sum_nonneg incseq_SucI nonneg simp: subseq_def)
+ (auto intro!: sum_nonneg incseq_SucI nonneg simp: strict_mono_def)
also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k<n. 2^k * f (2^k))"
proof (intro iffI)
assume A: "Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Aug 17 14:52:56 2017 +0200
@@ -4468,7 +4468,7 @@
lemma acc_point_range_imp_convergent_subsequence:
fixes l :: "'a :: first_countable_topology"
assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
- shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
proof -
from countable_basis_at_decseq[of l]
obtain A where A:
@@ -4492,8 +4492,8 @@
}
note s = this
define r where "r = rec_nat (s 0 0) s"
- have "subseq r"
- by (auto simp: r_def s subseq_Suc_iff)
+ have "strict_mono r"
+ by (auto simp: r_def s strict_mono_Suc_iff)
moreover
have "(\<lambda>n. f (r n)) \<longlonglongrightarrow> l"
proof (rule topological_tendstoI)
@@ -4513,7 +4513,7 @@
ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
by eventually_elim auto
qed
- ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+ ultimately show "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
by (auto simp: convergent_def comp_def)
qed
@@ -4616,7 +4616,7 @@
lemma islimpt_range_imp_convergent_subsequence:
fixes l :: "'a :: {t1_space, first_countable_topology}"
assumes l: "l islimpt (range f)"
- shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
using l unfolding islimpt_eq_acc_point
by (rule acc_point_range_imp_convergent_subsequence)
@@ -4949,16 +4949,16 @@
definition seq_compact :: "'a::topological_space set \<Rightarrow> bool"
where "seq_compact S \<longleftrightarrow>
- (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
+ (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
lemma seq_compactI:
- assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
shows "seq_compact S"
unfolding seq_compact_def using assms by fast
lemma seq_compactE:
assumes "seq_compact S" "\<forall>n. f n \<in> S"
- obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
using assms unfolding seq_compact_def by fast
lemma closed_sequentially: (* TODO: move upwards *)
@@ -4980,13 +4980,13 @@
hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
by simp_all
from \<open>seq_compact s\<close> and \<open>\<forall>n. f n \<in> s\<close>
- obtain l r where "l \<in> s" and r: "subseq r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
+ obtain l r where "l \<in> s" and r: "strict_mono r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
by (rule seq_compactE)
from \<open>\<forall>n. f n \<in> t\<close> have "\<forall>n. (f \<circ> r) n \<in> t"
by simp
from \<open>closed t\<close> and this and l have "l \<in> t"
by (rule closed_sequentially)
- with \<open>l \<in> s\<close> and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+ with \<open>l \<in> s\<close> and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
by fast
qed
@@ -5002,7 +5002,7 @@
proof (safe intro!: countably_compactI)
fix A
assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
- have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
+ have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> strict_mono (r :: nat \<Rightarrow> nat) \<and> (X \<circ> r) \<longlonglongrightarrow> x"
using \<open>seq_compact U\<close> by (fastforce simp: seq_compact_def subset_eq)
show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
proof cases
@@ -5023,7 +5023,7 @@
using \<open>A \<noteq> {}\<close> unfolding X_def by (intro T) (auto intro: from_nat_into)
then have "range X \<subseteq> U"
by auto
- with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) \<longlonglongrightarrow> x"
+ with subseq[of X] obtain r x where "x \<in> U" and r: "strict_mono r" "(X \<circ> r) \<longlonglongrightarrow> x"
by auto
from \<open>x\<in>U\<close> \<open>U \<subseteq> \<Union>A\<close> from_nat_into_surj[OF \<open>countable A\<close>]
obtain n where "x \<in> from_nat_into A n" by auto
@@ -5034,7 +5034,7 @@
by (auto simp: eventually_sequentially)
moreover from X have "\<And>i. n \<le> r i \<Longrightarrow> X (r i) \<notin> from_nat_into A n"
by auto
- moreover from \<open>subseq r\<close>[THEN seq_suble, of "max n N"] have "\<exists>i. n \<le> r i \<and> N \<le> i"
+ moreover from \<open>strict_mono r\<close>[THEN seq_suble, of "max n N"] have "\<exists>i. n \<le> r i \<and> N \<le> i"
by (auto intro!: exI[of _ "max n N"])
ultimately show False
by auto
@@ -5087,8 +5087,8 @@
}
note s = this
define r where "r = rec_nat (s 0 0) s"
- have "subseq r"
- by (auto simp: r_def s subseq_Suc_iff)
+ have "strict_mono r"
+ by (auto simp: r_def s strict_mono_Suc_iff)
moreover
have "(\<lambda>n. X (r n)) \<longlonglongrightarrow> x"
proof (rule topological_tendstoI)
@@ -5108,7 +5108,7 @@
ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
by eventually_elim auto
qed
- ultimately show "\<exists>x \<in> U. \<exists>r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
+ ultimately show "\<exists>x \<in> U. \<exists>r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
using \<open>x \<in> U\<close> by (auto simp: convergent_def comp_def)
qed
@@ -5159,25 +5159,25 @@
{
fix f :: "nat \<Rightarrow> 'a"
assume f: "\<forall>n. f n \<in> s"
- have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ have "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
proof (cases "finite (range f)")
case True
obtain l where "infinite {n. f n = f l}"
using pigeonhole_infinite[OF _ True] by auto
- then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l"
+ then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and fr: "\<forall>n. f (r n) = f l"
using infinite_enumerate by blast
- then have "subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
+ then have "strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
by (simp add: fr o_def)
- with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+ with f show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
by auto
next
case False
with f assms have "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)"
by auto
then obtain l where "l \<in> s" "\<forall>U. l\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" ..
- from this(2) have "\<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ from this(2) have "\<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
using acc_point_range_imp_convergent_subsequence[of l f] by auto
- with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
+ with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
qed
}
then show ?thesis
@@ -5237,14 +5237,14 @@
qed simp
then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
by blast
- then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
+ then obtain l r where "l \<in> s" and r:"strict_mono r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
using assms by (metis seq_compact_def)
from this(3) have "Cauchy (x \<circ> r)"
using LIMSEQ_imp_Cauchy by auto
then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
unfolding cauchy_def using \<open>e > 0\<close> by blast
then have False
- using x[of "r N" "r (N+1)"] r by (auto simp: subseq_def) }
+ using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
then show ?thesis
by metis
qed
@@ -5302,7 +5302,7 @@
lemma compact_def: \<comment>\<open>this is the definition of compactness in HOL Light\<close>
"compact (S :: 'a::metric_space set) \<longleftrightarrow>
- (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
+ (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
unfolding compact_eq_seq_compact_metric seq_compact_def by auto
subsubsection \<open>Complete the chain of compactness variants\<close>
@@ -5335,7 +5335,7 @@
class heine_borel = metric_space +
assumes bounded_imp_convergent_subsequence:
- "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
lemma bounded_closed_imp_seq_compact:
fixes s::"'a::heine_borel set"
@@ -5347,13 +5347,13 @@
assume f: "\<forall>n. f n \<in> s"
with \<open>bounded s\<close> have "bounded (range f)"
by (auto intro: bounded_subset)
- obtain l r where r: "subseq r" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"
by simp
have "l \<in> s" using \<open>closed s\<close> fr l
by (rule closed_sequentially)
- show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
using \<open>l \<in> s\<close> r l by blast
qed
@@ -5393,11 +5393,11 @@
proof
fix f :: "nat \<Rightarrow> real"
assume f: "bounded (range f)"
- obtain r where r: "subseq r" "monoseq (f \<circ> r)"
+ obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
unfolding comp_def by (metis seq_monosub)
then have "Bseq (f \<circ> r)"
unfolding Bseq_eq_bounded using f by (force intro: bounded_subset)
- with r show "\<exists>l r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+ with r show "\<exists>l r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
qed
@@ -5409,19 +5409,19 @@
assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)"
assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"
assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"
- shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r.
- subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
+ shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r::nat\<Rightarrow>nat.
+ strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
proof safe
fix d :: "'b set"
assume d: "d \<subseteq> basis"
with finite_basis have "finite d"
by (blast intro: finite_subset)
- from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
+ from this d show "\<exists>l::'a. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and>
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
proof (induct d)
case empty
then show ?case
- unfolding subseq_def by auto
+ unfolding strict_mono_def by auto
next
case (insert k d)
have k[intro]: "k \<in> basis"
@@ -5429,19 +5429,19 @@
have s': "bounded ((\<lambda>x. x proj k) ` range f)"
using k
by (rule bounded_proj)
- obtain l1::"'a" and r1 where r1: "subseq r1"
+ obtain l1::"'a" and r1 where r1: "strict_mono r1"
and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
using insert(3) using insert(4) by auto
have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f"
by simp
have "bounded (range (\<lambda>i. f (r1 i) proj k))"
by (metis (lifting) bounded_subset f' image_subsetI s')
- then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
+ then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]
by (auto simp: o_def)
define r where "r = r1 \<circ> r2"
- have r:"subseq r"
- using r1 and r2 unfolding r_def o_def subseq_def by auto
+ have r:"strict_mono r"
+ using r1 and r2 unfolding r_def o_def strict_mono_def by auto
moreover
define l where "l = unproj (\<lambda>i. if i = k then l2 else l1 proj i)"
{
@@ -5465,7 +5465,7 @@
fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
assumes "bounded (range f)"
shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
- subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+ strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
(auto intro!: assms bounded_linear_inner_left bounded_linear_image
simp: euclidean_representation)
@@ -5474,7 +5474,7 @@
proof
fix f :: "nat \<Rightarrow> 'a"
assume f: "bounded (range f)"
- then obtain l::'a and r where r: "subseq r"
+ then obtain l::'a and r where r: "strict_mono r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
using compact_lemma [OF f] by blast
{
@@ -5505,7 +5505,7 @@
}
then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
by auto
qed
@@ -5525,20 +5525,20 @@
by (rule bounded_fst)
then have s1: "bounded (range (fst \<circ> f))"
by (simp add: image_comp)
- obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
+ obtain l1 r1 where r1: "strict_mono r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
by (auto simp add: image_comp intro: bounded_snd bounded_subset)
- obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
+ obtain l2 r2 where r2: "strict_mono r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
using bounded_imp_convergent_subsequence [OF s2]
unfolding o_def by fast
have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially"
using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
have l: "((f \<circ> (r1 \<circ> r2)) \<longlongrightarrow> (l1, l2)) sequentially"
using tendsto_Pair [OF l1' l2] unfolding o_def by simp
- have r: "subseq (r1 \<circ> r2)"
- using r1 r2 unfolding subseq_def by simp
- show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ have r: "strict_mono (r1 \<circ> r2)"
+ using r1 r2 unfolding strict_mono_def by simp
+ show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
using l r by fast
qed
@@ -5641,7 +5641,7 @@
{
fix f
assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
- from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) \<longlonglongrightarrow> l"
+ from as(1) obtain l r where lr: "l\<in>s" "strict_mono r" "(f \<circ> r) \<longlonglongrightarrow> l"
using assms unfolding compact_def by blast
note lr' = seq_suble [OF lr(2)]
@@ -5752,8 +5752,8 @@
qed
define t where "t = rec_nat (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
- have "subseq t"
- unfolding subseq_Suc_iff by (simp add: t_def sel)
+ have "strict_mono t"
+ unfolding strict_mono_Suc_iff by (simp add: t_def sel)
moreover have "\<forall>i. (f \<circ> t) i \<in> s"
using f by auto
moreover
@@ -5777,7 +5777,7 @@
by (simp add: dist_commute)
qed
- ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+ ultimately show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
using assms unfolding complete_def by blast
qed
qed
@@ -5974,7 +5974,7 @@
using choice[of "\<lambda>n x. x \<in> s n"] by auto
from assms(4,1) have "seq_compact (s 0)"
by (simp add: bounded_closed_imp_seq_compact)
- then obtain l r where lr: "l \<in> s 0" "subseq r" "(x \<circ> r) \<longlonglongrightarrow> l"
+ then obtain l r where lr: "l \<in> s 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"
using x and assms(3) unfolding seq_compact_def by blast
have "\<forall>n. l \<in> s n"
proof
@@ -7670,7 +7670,7 @@
using neg by simp
then obtain f where "\<And>n. f n \<in> S" and fG: "\<And>G n. G \<in> \<G> \<Longrightarrow> \<not> ball (f n) (1 / Suc n) \<subseteq> G"
by metis
- then obtain l r where "l \<in> S" "subseq r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"
+ then obtain l r where "l \<in> S" "strict_mono r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"
using \<open>compact S\<close> compact_def that by metis
then obtain G where "l \<in> G" "G \<in> \<G>"
using Ssub by auto
@@ -7687,7 +7687,7 @@
by simp
also have "... \<le> 1 / real (Suc (max N1 N2))"
apply (simp add: divide_simps del: max.bounded_iff)
- using \<open>subseq r\<close> seq_suble by blast
+ using \<open>strict_mono r\<close> seq_suble by blast
also have "... \<le> 1 / real (Suc N2)"
by (simp add: field_simps)
also have "... < e/2"
@@ -7851,7 +7851,7 @@
apply (clarify, rename_tac l2 r2)
apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
apply (rule_tac x="r1 \<circ> r2" in exI)
- apply (rule conjI, simp add: subseq_def)
+ apply (rule conjI, simp add: strict_mono_def)
apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
apply (drule (1) tendsto_Pair) back
apply (simp add: o_def)
@@ -8287,7 +8287,7 @@
assume as: "\<forall>n. x n \<in> ?S" "(x \<longlongrightarrow> l) sequentially"
from as(1) obtain f where f: "\<forall>n. x n = fst (f n) + snd (f n)" "\<forall>n. fst (f n) \<in> S" "\<forall>n. snd (f n) \<in> T"
using choice[of "\<lambda>n y. x n = (fst y) + (snd y) \<and> fst y \<in> S \<and> snd y \<in> T"] by auto
- obtain l' r where "l'\<in>S" and r: "subseq r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially"
+ obtain l' r where "l'\<in>S" and r: "strict_mono r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially"
using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
have "((\<lambda>n. snd (f (r n))) \<longlongrightarrow> l - l') sequentially"
using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1)
--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Thu Aug 17 14:52:56 2017 +0200
@@ -236,13 +236,13 @@
lemma bolzano_weierstrass_complex_disc:
assumes r: "\<forall>n. cmod (s n) \<le> r"
- shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
+ shows "\<exists>f z. strict_mono (f :: nat \<Rightarrow> nat) \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
proof -
from seq_monosub[of "Re \<circ> s"]
- obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
+ obtain f where f: "strict_mono f" "monoseq (\<lambda>n. Re (s (f n)))"
unfolding o_def by blast
from seq_monosub[of "Im \<circ> s \<circ> f"]
- obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s (f (g n))))"
+ obtain g where g: "strict_mono g" "monoseq (\<lambda>n. Im (s (f (g n))))"
unfolding o_def by blast
let ?h = "f \<circ> g"
from r[rule_format, of 0] have rp: "r \<ge> 0"
@@ -284,8 +284,8 @@
then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Im (s (f (g n))) - y\<bar> < r"
unfolding LIMSEQ_iff real_norm_def .
let ?w = "Complex x y"
- from f(1) g(1) have hs: "subseq ?h"
- unfolding subseq_def by auto
+ from f(1) g(1) have hs: "strict_mono ?h"
+ unfolding strict_mono_def by auto
have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" if "e > 0" for e
proof -
from that have e2: "e/2 > 0"
@@ -400,7 +400,7 @@
g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
by blast
from bolzano_weierstrass_complex_disc[OF g(1)]
- obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
+ obtain f z where fz: "strict_mono (f :: nat \<Rightarrow> nat)" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
by blast
{
fix w
--- a/src/HOL/Library/Diagonal_Subsequence.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Library/Diagonal_Subsequence.thy Thu Aug 17 14:52:56 2017 +0200
@@ -8,28 +8,28 @@
locale subseqs =
fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool"
- assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')"
+ assumes ex_subseq: "\<And>n s. strict_mono (s::nat\<Rightarrow>nat) \<Longrightarrow> \<exists>r'. strict_mono r' \<and> P n (s o r')"
begin
-definition reduce where "reduce s n = (SOME r'. subseq r' \<and> P n (s o r'))"
+definition reduce where "reduce s n = (SOME r'::nat\<Rightarrow>nat. strict_mono r' \<and> P n (s o r'))"
lemma subseq_reduce[intro, simp]:
- "subseq s \<Longrightarrow> subseq (reduce s n)"
+ "strict_mono s \<Longrightarrow> strict_mono (reduce s n)"
unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto
lemma reduce_holds:
- "subseq s \<Longrightarrow> P n (s o reduce s n)"
+ "strict_mono s \<Longrightarrow> P n (s o reduce s n)"
unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def)
-primrec seqseq where
+primrec seqseq :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"seqseq 0 = id"
| "seqseq (Suc n) = seqseq n o reduce (seqseq n) n"
-lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
+lemma subseq_seqseq[intro, simp]: "strict_mono (seqseq n)"
proof (induct n)
- case 0 thus ?case by (simp add: subseq_def)
+ case 0 thus ?case by (simp add: strict_mono_def)
next
- case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
+ case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: strict_mono_o)
qed
lemma seqseq_holds:
@@ -40,35 +40,29 @@
thus ?thesis by simp
qed
-definition diagseq where "diagseq i = seqseq i i"
-
-lemma subseq_mono: "subseq f \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
- by (metis le_eq_less_or_eq subseq_mono)
-
-lemma subseq_strict_mono: "subseq f \<Longrightarrow> a < b \<Longrightarrow> f a < f b"
- by (simp add: subseq_def)
+definition diagseq :: "nat \<Rightarrow> nat" where "diagseq i = seqseq i i"
lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
proof -
have "diagseq n < seqseq n (Suc n)"
- using subseq_seqseq[of n] by (simp add: diagseq_def subseq_def)
+ using subseq_seqseq[of n] by (simp add: diagseq_def strict_mono_def)
also have "\<dots> \<le> seqseq n (reduce (seqseq n) n (Suc n))"
- by (auto intro: subseq_mono seq_suble)
+ using strict_mono_less_eq seq_suble by blast
also have "\<dots> = diagseq (Suc n)" by (simp add: diagseq_def)
finally show ?thesis .
qed
-lemma subseq_diagseq: "subseq diagseq"
- using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
+lemma subseq_diagseq: "strict_mono diagseq"
+ using diagseq_mono by (simp add: strict_mono_Suc_iff diagseq_def)
primrec fold_reduce where
"fold_reduce n 0 = id"
| "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)"
-lemma subseq_fold_reduce[intro, simp]: "subseq (fold_reduce n k)"
+lemma subseq_fold_reduce[intro, simp]: "strict_mono (fold_reduce n k)"
proof (induct k)
- case (Suc k) from subseq_o[OF this subseq_reduce] show ?case by (simp add: o_def)
-qed (simp add: subseq_def)
+ case (Suc k) from strict_mono_o[OF this subseq_reduce] show ?case by (simp add: o_def)
+qed (simp add: strict_mono_def)
lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
by (induct k) simp_all
@@ -95,14 +89,14 @@
assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
using diagseq_add[of m "n - m"] assms by simp
-lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
- unfolding subseq_Suc_iff fold_reduce.simps o_def
+lemma subseq_diagonal_rest: "strict_mono (\<lambda>x. fold_reduce k x (k + x))"
+ unfolding strict_mono_Suc_iff fold_reduce.simps o_def
proof
fix n
have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _")
- by (auto intro: subseq_strict_mono)
+ by (auto intro: strict_monoD)
also have "\<dots> \<le> fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))"
- by (rule subseq_mono) (auto intro!: seq_suble subseq_mono)
+ by (auto intro: less_mono_imp_le_mono seq_suble strict_monoD)
finally show "?lhs < \<dots>" .
qed
@@ -110,7 +104,7 @@
by (auto simp: o_def diagseq_add)
lemma diagseq_holds:
- assumes subseq_stable: "\<And>r s n. subseq r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)"
+ assumes subseq_stable: "\<And>r s n. strict_mono r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)"
shows "P k (diagseq o (op + (Suc k)))"
unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds)
--- a/src/HOL/Library/Liminf_Limsup.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Thu Aug 17 14:52:56 2017 +0200
@@ -379,20 +379,20 @@
lemma liminf_subseq_mono:
fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
- assumes "subseq r"
+ assumes "strict_mono r"
shows "liminf X \<le> liminf (X \<circ> r) "
proof-
have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
proof (safe intro!: INF_mono)
fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
- using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
+ using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
qed
then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
qed
lemma limsup_subseq_mono:
fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
- assumes "subseq r"
+ assumes "strict_mono r"
shows "limsup (X \<circ> r) \<le> limsup X"
proof-
have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
@@ -400,7 +400,7 @@
fix m :: nat
assume "n \<le> m"
then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
- using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
+ using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
qed
then show ?thesis
by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
@@ -587,9 +587,9 @@
lemma compact_complete_linorder:
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
+ shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
proof -
- obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
+ obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"
using seq_monosub[of X]
unfolding comp_def
by auto
@@ -599,7 +599,7 @@
using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
by auto
then show ?thesis
- using \<open>subseq r\<close> by auto
+ using \<open>strict_mono r\<close> by auto
qed
lemma tendsto_Limsup:
--- a/src/HOL/Limits.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Limits.thy Thu Aug 17 14:52:56 2017 +0200
@@ -325,7 +325,7 @@
using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)
lemma increasing_Bseq_subseq_iff:
- assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "subseq g"
+ assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "strict_mono g"
shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
proof
assume "Bseq (\<lambda>x. f (g x))"
@@ -346,7 +346,7 @@
lemma nonneg_incseq_Bseq_subseq_iff:
fixes f :: "nat \<Rightarrow> real"
and g :: "nat \<Rightarrow> nat"
- assumes "\<And>x. f x \<ge> 0" "incseq f" "subseq g"
+ assumes "\<And>x. f x \<ge> 0" "incseq f" "strict_mono g"
shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)
@@ -1398,11 +1398,11 @@
lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x) at_top sequentially"
for c :: nat
- by (rule filterlim_subseq) (auto simp: subseq_def)
+ by (rule filterlim_subseq) (auto simp: strict_mono_def)
lemma mult_nat_right_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. x * c) at_top sequentially"
for c :: nat
- by (rule filterlim_subseq) (auto simp: subseq_def)
+ by (rule filterlim_subseq) (auto simp: strict_mono_def)
lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
proof (rule antisym)
--- a/src/HOL/Probability/Helly_Selection.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Probability/Helly_Selection.thy Thu Aug 17 14:52:56 2017 +0200
@@ -19,7 +19,7 @@
assumes rcont: "\<And>n x. continuous (at_right x) (f n)"
assumes mono: "\<And>n. mono (f n)"
assumes bdd: "\<And>n x. \<bar>f n x\<bar> \<le> M"
- shows "\<exists>s. subseq s \<and> (\<exists>F. (\<forall>x. continuous (at_right x) F) \<and> mono F \<and> (\<forall>x. \<bar>F x\<bar> \<le> M) \<and>
+ shows "\<exists>s. strict_mono (s::nat \<Rightarrow> nat) \<and> (\<exists>F. (\<forall>x. continuous (at_right x) F) \<and> mono F \<and> (\<forall>x. \<bar>F x\<bar> \<le> M) \<and>
(\<forall>x. continuous (at x) F \<longrightarrow> (\<lambda>n. f (s n) x) \<longlonglongrightarrow> F x))"
proof -
obtain m :: "real \<Rightarrow> nat" where "bij_betw m \<rat> UNIV"
@@ -33,18 +33,18 @@
let ?P = "\<lambda>n. \<lambda>s. convergent (\<lambda>k. f (s k) (r n))"
interpret nat: subseqs ?P
proof (unfold convergent_def, unfold subseqs_def, auto)
- fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "subseq s"
+ fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "strict_mono s"
have "bounded {-M..M}"
using bounded_closed_interval by auto
moreover have "\<And>k. f (s k) (r n) \<in> {-M..M}"
using bdd by (simp add: abs_le_iff minus_le_iff)
- ultimately have "\<exists>l s'. subseq s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
+ ultimately have "\<exists>l s'. strict_mono s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
using compact_Icc compact_imp_seq_compact seq_compactE by metis
- thus "\<exists>s'. subseq s' \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
+ thus "\<exists>s'. strict_mono (s'::nat\<Rightarrow>nat) \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
by (auto simp: comp_def)
qed
define d where "d = nat.diagseq"
- have subseq: "subseq d"
+ have subseq: "strict_mono d"
unfolding d_def using nat.subseq_diagseq by auto
have rat_cnv: "?P n d" for n
proof -
@@ -157,8 +157,8 @@
(* Can strengthen to equivalence. *)
theorem tight_imp_convergent_subsubsequence:
- assumes \<mu>: "tight \<mu>" "subseq s"
- shows "\<exists>r M. subseq r \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
+ assumes \<mu>: "tight \<mu>" "strict_mono s"
+ shows "\<exists>r M. strict_mono (r :: nat \<Rightarrow> nat) \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
proof -
define f where "f k = cdf (\<mu> (s k))" for k
interpret \<mu>: real_distribution "\<mu> k" for k
@@ -174,7 +174,7 @@
by (auto simp add: abs_le_iff minus_le_iff f_def \<mu>.cdf_nonneg \<mu>.cdf_bounded_prob)
from Helly_selection[OF rcont mono bdd, of "\<lambda>x. x"] obtain r F
- where F: "subseq r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1"
+ where F: "strict_mono r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1"
and lim_F: "\<And>x. continuous (at x) F \<Longrightarrow> (\<lambda>n. f (r n) x) \<longlonglongrightarrow> F x"
by blast
@@ -265,14 +265,14 @@
using F by (auto intro!: real_distribution_interval_measure cdf_interval_measure simp: mono_def)
with lim_F LIMSEQ_subseq_LIMSEQ M have "weak_conv_m (\<mu> \<circ> s \<circ> r) (interval_measure F)"
by (auto simp: weak_conv_def weak_conv_m_def f_def comp_def)
- then show "\<exists>r M. subseq r \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)"
+ then show "\<exists>r M. strict_mono (r :: nat \<Rightarrow> nat) \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)"
using F M by auto
qed
corollary tight_subseq_weak_converge:
fixes \<mu> :: "nat \<Rightarrow> real measure" and M :: "real measure"
assumes "\<And>n. real_distribution (\<mu> n)" "real_distribution M" and tight: "tight \<mu>" and
- subseq: "\<And>s \<nu>. subseq s \<Longrightarrow> real_distribution \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) M"
+ subseq: "\<And>s \<nu>. strict_mono s \<Longrightarrow> real_distribution \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) M"
shows "weak_conv_m \<mu> M"
proof (rule ccontr)
define f where "f n = cdf (\<mu> n)" for n
@@ -283,12 +283,12 @@
by (auto simp: weak_conv_m_def weak_conv_def f_def F_def)
then obtain \<epsilon> where "\<epsilon> > 0" and "infinite {n. \<not> dist (f n x) (F x) < \<epsilon>}"
by (auto simp: tendsto_iff not_eventually INFM_iff_infinite cofinite_eq_sequentially[symmetric])
- then obtain s where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "subseq s"
- using enumerate_in_set enumerate_mono by (fastforce simp: subseq_def)
- then obtain r \<nu> where r: "subseq r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
+ then obtain s :: "nat \<Rightarrow> nat" where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "strict_mono s"
+ using enumerate_in_set enumerate_mono by (fastforce simp: strict_mono_def)
+ then obtain r \<nu> where r: "strict_mono r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
using tight_imp_convergent_subsubsequence[OF tight] by blast
then have "weak_conv_m (\<mu> \<circ> (s \<circ> r)) M"
- using \<open>subseq s\<close> r by (intro subseq subseq_o) (auto simp: comp_assoc)
+ using \<open>strict_mono s\<close> r by (intro subseq strict_mono_o) (auto simp: comp_assoc)
then have "(\<lambda>n. f (s (r n)) x) \<longlonglongrightarrow> F x"
using x by (auto simp: weak_conv_m_def weak_conv_def F_def f_def)
then show False
--- a/src/HOL/Probability/Levy.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Probability/Levy.thy Thu Aug 17 14:52:56 2017 +0200
@@ -500,7 +500,7 @@
show ?thesis
proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight])
fix s \<nu>
- assume s: "subseq s"
+ assume s: "strict_mono (s :: nat \<Rightarrow> nat)"
assume nu: "weak_conv_m (M \<circ> s) \<nu>"
assume *: "real_distribution \<nu>"
have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms)
--- a/src/HOL/Probability/Projective_Limit.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy Thu Aug 17 14:52:56 2017 +0200
@@ -45,20 +45,20 @@
lemma compactE':
fixes S :: "'a :: metric_space set"
assumes "compact S" "\<forall>n\<ge>m. f n \<in> S"
- obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ obtains l r where "l \<in> S" "strict_mono (r::nat\<Rightarrow>nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
proof atomize_elim
- have "subseq (op + m)" by (simp add: subseq_def)
+ have "strict_mono (op + m)" by (simp add: strict_mono_def)
have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this] guess l r .
- hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
- using subseq_o[OF \<open>subseq (op + m)\<close> \<open>subseq r\<close>] by (auto simp: o_def)
- thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
+ hence "l \<in> S" "strict_mono ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
+ using strict_mono_o[OF \<open>strict_mono (op + m)\<close> \<open>strict_mono r\<close>] by (auto simp: o_def)
+ thus "\<exists>l r. l \<in> S \<and> strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
qed
sublocale finmap_seqs_into_compact \<subseteq> subseqs "\<lambda>n s. (\<exists>l. (\<lambda>i. ((f o s) i)\<^sub>F n) \<longlonglongrightarrow> l)"
proof
- fix n s
- assume "subseq s"
+ fix n and s :: "nat \<Rightarrow> nat"
+ assume "strict_mono s"
from proj_in_KE[of n] guess n0 . note n0 = this
have "\<forall>i \<ge> n0. ((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0"
proof safe
@@ -69,7 +69,7 @@
by auto
qed
from compactE'[OF compact_projset this] guess ls rs .
- thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def)
+ thus "\<exists>r'. strict_mono r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def)
qed
lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^sub>F n) \<longlonglongrightarrow> l"
@@ -77,11 +77,11 @@
obtain l where "(\<lambda>i. ((f o (diagseq o op + (Suc n))) i)\<^sub>F n) \<longlonglongrightarrow> l"
proof (atomize_elim, rule diagseq_holds)
fix r s n
- assume "subseq r"
+ assume "strict_mono (r :: nat \<Rightarrow> nat)"
assume "\<exists>l. (\<lambda>i. ((f \<circ> s) i)\<^sub>F n) \<longlonglongrightarrow> l"
then obtain l where "((\<lambda>i. (f i)\<^sub>F n) o s) \<longlonglongrightarrow> l"
by (auto simp: o_def)
- hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>subseq r\<close>
+ hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>strict_mono r\<close>
by (rule LIMSEQ_subseq_LIMSEQ)
thus "\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r)) i)\<^sub>F n) \<longlonglongrightarrow> l" by (auto simp add: o_def)
qed
@@ -406,7 +406,7 @@
have "(\<lambda>i. fm n (y (Suc (diagseq i)))) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
by (rule tendsto_finmap)
hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
- by (rule LIMSEQ_subseq_LIMSEQ) (simp add: subseq_def)
+ by (rule LIMSEQ_subseq_LIMSEQ) (simp add: strict_mono_def)
moreover
have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"
apply (auto simp add: o_def intro!: fm_in_K' \<open>1 \<le> n\<close> le_SucI)
--- a/src/HOL/Series.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Series.thy Thu Aug 17 14:52:56 2017 +0200
@@ -1107,7 +1107,7 @@
qed
lemma sums_mono_reindex:
- assumes subseq: "subseq g"
+ assumes subseq: "strict_mono g"
and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
unfolding sums_def
@@ -1117,10 +1117,10 @@
proof
fix n :: nat
from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
- by (subst sum.reindex) (auto intro: subseq_imp_inj_on)
+ by (subst sum.reindex) (auto intro: strict_mono_imp_inj_on)
also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
by (intro sum.mono_neutral_left ballI zero)
- (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
+ (auto simp: strict_mono_less strict_mono_less_eq)
finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
qed
also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c"
@@ -1150,7 +1150,7 @@
have "g l < g (g_inv n)"
by (rule less_le_trans[OF _ g_inv]) (use k l in simp_all)
with subseq have "l < g_inv n"
- by (simp add: subseq_strict_mono strict_mono_less)
+ by (simp add: strict_mono_less)
with k l show False
by simp
qed
@@ -1160,7 +1160,7 @@
with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
by (intro sum.mono_neutral_right) auto
also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))"
- using subseq_imp_inj_on by (subst sum.reindex) simp_all
+ using strict_mono_imp_inj_on by (subst sum.reindex) simp_all
finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
qed
also {
@@ -1169,7 +1169,7 @@
also have "n \<le> g (g_inv n)"
by (rule g_inv)
finally have "K \<le> g_inv n"
- using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
+ using subseq by (simp add: strict_mono_less_eq)
}
then have "filterlim g_inv at_top sequentially"
by (auto simp: filterlim_at_top eventually_at_top_linorder)
@@ -1179,14 +1179,14 @@
qed
lemma summable_mono_reindex:
- assumes subseq: "subseq g"
+ assumes subseq: "strict_mono g"
and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
lemma suminf_mono_reindex:
fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}"
- assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
+ assumes "strict_mono g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
shows "suminf (\<lambda>n. f (g n)) = suminf f"
proof (cases "summable f")
case True
--- a/src/HOL/Topological_Spaces.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Topological_Spaces.thy Thu Aug 17 14:52:56 2017 +0200
@@ -1069,14 +1069,13 @@
unfolding antimono_def ..
text \<open>Definition of subsequence.\<close>
-definition subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
- where "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
-
-lemma subseq_le_mono: "subseq r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
- by (simp add: less_mono_imp_le_mono subseq_def)
-
-lemma subseq_id: "subseq id"
- by (simp add: subseq_def)
+
+(* For compatibility with the old "subseq" *)
+lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
+ by (erule (1) monoD [OF strict_mono_mono])
+
+lemma strict_mono_id: "strict_mono id"
+ by (simp add: strict_mono_def)
lemma incseq_SucI: "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
using lift_Suc_mono_le[of X] by (auto simp: incseq_def)
@@ -1144,28 +1143,30 @@
text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
-lemma subseq_Suc_iff: "subseq f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
- apply (simp add: subseq_def)
- apply (auto dest!: less_imp_Suc_add)
- apply (induct_tac k)
- apply (auto intro: less_trans)
- done
-
-lemma subseq_add: "subseq (\<lambda>n. n + k)"
- by (auto simp: subseq_Suc_iff)
+lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
+proof (intro iffI strict_monoI)
+ assume *: "\<forall>n. f n < f (Suc n)"
+ fix m n :: nat assume "m < n"
+ thus "f m < f n"
+ by (induction rule: less_Suc_induct) (use * in auto)
+qed (auto simp: strict_mono_def)
+
+lemma strict_mono_add: "strict_mono (\<lambda>n::'a::linordered_semidom. n + k)"
+ by (auto simp: strict_mono_def)
text \<open>For any sequence, there is a monotonic subsequence.\<close>
lemma seq_monosub:
fixes s :: "nat \<Rightarrow> 'a::linorder"
- shows "\<exists>f. subseq f \<and> monoseq (\<lambda>n. (s (f n)))"
+ shows "\<exists>f. strict_mono f \<and> monoseq (\<lambda>n. (s (f n)))"
proof (cases "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. s m \<le> s p")
case True
then have "\<exists>f. \<forall>n. (\<forall>m\<ge>f n. s m \<le> s (f n)) \<and> f n < f (Suc n)"
by (intro dependent_nat_choice) (auto simp: conj_commute)
- then obtain f where f: "subseq f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
- by (auto simp: subseq_Suc_iff)
+ then obtain f :: "nat \<Rightarrow> nat"
+ where f: "strict_mono f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
+ by (auto simp: strict_mono_Suc_iff)
then have "incseq f"
- unfolding subseq_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
+ unfolding strict_mono_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
then have "monoseq (\<lambda>n. s (f n))"
by (auto simp add: incseq_def intro!: mono monoI2)
with f show ?thesis
@@ -1182,29 +1183,29 @@
by (auto intro: less_trans)
qed auto
then show ?thesis
- by (auto simp: monoseq_iff incseq_Suc_iff subseq_Suc_iff)
+ by (auto simp: monoseq_iff incseq_Suc_iff strict_mono_Suc_iff)
qed
lemma seq_suble:
- assumes sf: "subseq f"
+ assumes sf: "strict_mono (f :: nat \<Rightarrow> nat)"
shows "n \<le> f n"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
- with sf [unfolded subseq_Suc_iff, rule_format, of n] have "n < f (Suc n)"
+ with sf [unfolded strict_mono_Suc_iff, rule_format, of n] have "n < f (Suc n)"
by arith
then show ?case by arith
qed
lemma eventually_subseq:
- "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
+ "strict_mono r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
unfolding eventually_sequentially by (metis seq_suble le_trans)
lemma not_eventually_sequentiallyD:
assumes "\<not> eventually P sequentially"
- shows "\<exists>r. subseq r \<and> (\<forall>n. \<not> P (r n))"
+ shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. \<not> P (r n))"
proof -
from assms have "\<forall>n. \<exists>m\<ge>n. \<not> P m"
unfolding eventually_sequentially by (simp add: not_less)
@@ -1212,29 +1213,14 @@
by (auto simp: choice_iff)
then show ?thesis
by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"]
- simp: less_eq_Suc_le subseq_Suc_iff)
+ simp: less_eq_Suc_le strict_mono_Suc_iff)
qed
-lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
+lemma filterlim_subseq: "strict_mono f \<Longrightarrow> filterlim f sequentially sequentially"
unfolding filterlim_iff by (metis eventually_subseq)
-lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
- unfolding subseq_def by simp
-
-lemma subseq_mono: "subseq r \<Longrightarrow> m < n \<Longrightarrow> r m < r n"
- by (auto simp: subseq_def)
-
-lemma subseq_imp_inj_on: "subseq g \<Longrightarrow> inj_on g A"
-proof (rule inj_onI)
- assume g: "subseq g"
- fix x y
- assume "g x = g y"
- with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y"
- by (cases x y rule: linorder_cases) simp_all
-qed
-
-lemma subseq_strict_mono: "subseq g \<Longrightarrow> strict_mono g"
- by (intro strict_monoI subseq_mono[of g])
+lemma strict_mono_o: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (r \<circ> s)"
+ unfolding strict_mono_def by simp
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X"
by (simp add: incseq_def monoseq_def)
@@ -1324,10 +1310,10 @@
for x :: "'a::linorder_topology"
by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
-lemma LIMSEQ_subseq_LIMSEQ: "X \<longlonglongrightarrow> L \<Longrightarrow> subseq f \<Longrightarrow> (X \<circ> f) \<longlonglongrightarrow> L"
+lemma LIMSEQ_subseq_LIMSEQ: "X \<longlonglongrightarrow> L \<Longrightarrow> strict_mono f \<Longrightarrow> (X \<circ> f) \<longlonglongrightarrow> L"
unfolding comp_def by (rule filterlim_compose [of X, OF _ filterlim_subseq])
-lemma convergent_subseq_convergent: "convergent X \<Longrightarrow> subseq f \<Longrightarrow> convergent (X \<circ> f)"
+lemma convergent_subseq_convergent: "convergent X \<Longrightarrow> strict_mono f \<Longrightarrow> convergent (X \<circ> f)"
by (auto simp: convergent_def intro: LIMSEQ_subseq_LIMSEQ)
lemma limI: "X \<longlonglongrightarrow> L \<Longrightarrow> lim X = L"
@@ -1651,7 +1637,7 @@
and "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a"
and "\<not> P (X (s n))"
for n
- by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff
+ by (auto simp: strict_mono_Suc_iff Suc_le_eq incseq_Suc_iff
intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
from *[OF this(1,2,3,4)] this(5) show False
by auto
@@ -1700,7 +1686,7 @@
and "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a"
and "\<not> P (X (s n))"
for n
- by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff
+ by (auto simp: strict_mono_Suc_iff Suc_le_eq decseq_Suc_iff
intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
from *[OF this(1,2,3,4)] this(5) show False
by auto
@@ -3143,11 +3129,11 @@
unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
lemma Cauchy_subseq_Cauchy:
- assumes "Cauchy X" "subseq f"
+ assumes "Cauchy X" "strict_mono f"
shows "Cauchy (X \<circ> f)"
unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
- (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
+ (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>strict_mono f\<close>, unfolded filterlim_def])
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)