equal
deleted
inserted
replaced
3702 thus ?thesis .. |
3702 thus ?thesis .. |
3703 qed |
3703 qed |
3704 |
3704 |
3705 text{* Cauchy-type criteria for uniform convergence. *} |
3705 text{* Cauchy-type criteria for uniform convergence. *} |
3706 |
3706 |
3707 lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::heine_borel" shows |
3707 lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space" shows |
3708 "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow> |
3708 "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow> |
3709 (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs") |
3709 (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs") |
3710 proof(rule) |
3710 proof(rule) |
3711 assume ?lhs |
3711 assume ?lhs |
3712 then obtain l where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e" by auto |
3712 then obtain l where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e" by auto |
3736 hence "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e" by auto } |
3736 hence "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e" by auto } |
3737 thus ?lhs by auto |
3737 thus ?lhs by auto |
3738 qed |
3738 qed |
3739 |
3739 |
3740 lemma uniformly_cauchy_imp_uniformly_convergent: |
3740 lemma uniformly_cauchy_imp_uniformly_convergent: |
3741 fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::heine_borel" |
3741 fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space" |
3742 assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e" |
3742 assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e" |
3743 "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)" |
3743 "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)" |
3744 shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e" |
3744 shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e" |
3745 proof- |
3745 proof- |
3746 obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e" |
3746 obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e" |