75 thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^isub>F n) ----> l)" by (auto simp: o_def) |
75 thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^isub>F n) ----> l)" by (auto simp: o_def) |
76 qed |
76 qed |
77 |
77 |
78 lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l" |
78 lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l" |
79 proof - |
79 proof - |
80 have "\<And>i n0. (f o seqseq i) i = f (diagseq i)" unfolding diagseq_def by simp |
80 obtain l where "(\<lambda>i. ((f o (diagseq o op + (Suc n))) i)\<^isub>F n) ----> l" |
81 from reducer_reduces obtain l where l: "(\<lambda>i. ((f \<circ> seqseq (Suc n)) i)\<^isub>F n) ----> l" |
81 proof (atomize_elim, rule diagseq_holds) |
82 unfolding seqseq_reducer |
82 fix r s n |
83 by auto |
83 assume "subseq r" |
84 have "(\<lambda>i. (f (diagseq (i + Suc n)))\<^isub>F n) = |
84 assume "\<exists>l. (\<lambda>i. ((f \<circ> s) i)\<^isub>F n) ----> l" |
85 (\<lambda>i. ((f o (diagseq o (op + (Suc n)))) i)\<^isub>F n)" by (simp add: add_commute) |
85 then obtain l where "((\<lambda>i. (f i)\<^isub>F n) o s) ----> l" |
86 also have "\<dots> = |
86 by (auto simp: o_def) |
87 (\<lambda>i. ((f o ((seqseq (Suc n) o (\<lambda>x. fold_reduce (Suc n) x (Suc n + x))))) i)\<^isub>F n)" |
87 hence "((\<lambda>i. (f i)\<^isub>F n) o s o r) ----> l" using `subseq r` |
88 unfolding diagseq_seqseq by simp |
88 by (rule LIMSEQ_subseq_LIMSEQ) |
89 also have "\<dots> = (\<lambda>i. ((f o ((seqseq (Suc n)))) i)\<^isub>F n) o (\<lambda>x. fold_reduce (Suc n) x (Suc n + x))" |
89 thus "\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r)) i)\<^isub>F n) ----> l" by (auto simp add: o_def) |
90 by (simp add: o_def) |
|
91 also have "\<dots> ----> l" |
|
92 proof (rule LIMSEQ_subseq_LIMSEQ[OF _ subseq_diagonal_rest], rule tendstoI) |
|
93 fix e::real assume "0 < e" |
|
94 from tendstoD[OF l `0 < e`] |
|
95 show "eventually (\<lambda>x. dist (((f \<circ> seqseq (Suc n)) x)\<^isub>F n) l < e) |
|
96 sequentially" . |
|
97 qed |
90 qed |
98 finally show ?thesis by (intro exI) (rule LIMSEQ_offset) |
91 hence "(\<lambda>i. ((f (diagseq (i + Suc n))))\<^isub>F n) ----> l" by (simp add: ac_simps) |
|
92 hence "(\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l" by (rule LIMSEQ_offset) |
|
93 thus ?thesis .. |
99 qed |
94 qed |
100 |
95 |
101 subsection {* Daniell-Kolmogorov Theorem *} |
96 subsection {* Daniell-Kolmogorov Theorem *} |
102 |
97 |
103 text {* Existence of Projective Limit *} |
98 text {* Existence of Projective Limit *} |