generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 514741e9e68247ad1
parent 51473 1210309fddab
child 51475 ebf9d4fd00ba
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
src/HOL/Limits.thy
src/HOL/Metric_Spaces.thy
src/HOL/NSA/HSEQ.thy
src/HOL/RealVector.thy
src/HOL/SEQ.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -49,8 +49,18 @@
     1.4  
     1.5  subsection {* Boundedness *}
     1.6  
     1.7 -definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
     1.8 -  where "Bfun f F = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)"
     1.9 +lemma Bfun_def:
    1.10 +  "Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)"
    1.11 +  unfolding Bfun_metric_def norm_conv_dist
    1.12 +proof safe
    1.13 +  fix y K assume "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F"
    1.14 +  moreover have "eventually (\<lambda>x. dist (f x) 0 \<le> dist (f x) y + dist 0 y) F"
    1.15 +    by (intro always_eventually) (metis dist_commute dist_triangle)
    1.16 +  with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F"
    1.17 +    by eventually_elim auto
    1.18 +  with `0 < K` show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F"
    1.19 +    by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto
    1.20 +qed auto
    1.21  
    1.22  lemma BfunI:
    1.23    assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F"
    1.24 @@ -67,7 +77,6 @@
    1.25    obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"
    1.26  using assms unfolding Bfun_def by fast
    1.27  
    1.28 -
    1.29  subsection {* Convergence to Zero *}
    1.30  
    1.31  definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.32 @@ -223,9 +232,6 @@
    1.33  
    1.34  subsubsection {* Distance and norms *}
    1.35  
    1.36 -lemma norm_conv_dist: "norm x = dist x 0"
    1.37 -  unfolding dist_norm by simp
    1.38 -
    1.39  lemma tendsto_norm [tendsto_intros]:
    1.40    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
    1.41    unfolding norm_conv_dist by (intro tendsto_intros)
     2.1 --- a/src/HOL/Metric_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     2.2 +++ b/src/HOL/Metric_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -285,6 +285,22 @@
     2.4    shows "(\<lambda>x. g (f x)) -- a --> l"
     2.5  by (rule metric_LIM_compose2 [OF f g inj])
     2.6  
     2.7 +subsubsection {* Boundedness *}
     2.8 +
     2.9 +definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    2.10 +  Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)"
    2.11 +
    2.12 +abbreviation Bseq :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    2.13 +  "Bseq X \<equiv> Bfun X sequentially"
    2.14 +
    2.15 +lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" ..
    2.16 +
    2.17 +lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))"
    2.18 +  unfolding Bfun_metric_def by (subst eventually_sequentially_seg)
    2.19 +
    2.20 +lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
    2.21 +  unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg)
    2.22 +
    2.23  subsection {* Complete metric spaces *}
    2.24  
    2.25  subsection {* Cauchy sequences *}
    2.26 @@ -320,6 +336,18 @@
    2.27  apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
    2.28  done
    2.29  
    2.30 +lemma Cauchy_Bseq: "Cauchy X \<Longrightarrow> Bseq X"
    2.31 +  unfolding Cauchy_def Bfun_metric_def eventually_sequentially
    2.32 +  apply (erule_tac x=1 in allE)
    2.33 +  apply simp
    2.34 +  apply safe
    2.35 +  apply (rule_tac x="X M" in exI)
    2.36 +  apply (rule_tac x=1 in exI)
    2.37 +  apply (erule_tac x=M in allE)
    2.38 +  apply simp
    2.39 +  apply (rule_tac x=M in exI)
    2.40 +  apply (auto simp: dist_commute)
    2.41 +  done
    2.42  
    2.43  subsubsection {* Cauchy Sequences are Convergent *}
    2.44  
     3.1 --- a/src/HOL/NSA/HSEQ.thy	Fri Mar 22 10:41:43 2013 +0100
     3.2 +++ b/src/HOL/NSA/HSEQ.thy	Fri Mar 22 10:41:43 2013 +0100
     3.3 @@ -343,7 +343,7 @@
     3.4  text{*Standard Version: easily now proved using equivalence of NS and
     3.5   standard definitions *}
     3.6  
     3.7 -lemma convergent_Bseq: "convergent X ==> Bseq X"
     3.8 +lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)"
     3.9  by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
    3.10  
    3.11  subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
     4.1 --- a/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     4.2 +++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     4.3 @@ -665,7 +665,6 @@
     4.4      using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
     4.5  qed
     4.6  
     4.7 -
     4.8  subsection {* Class instances for real numbers *}
     4.9  
    4.10  instantiation real :: real_normed_field
    4.11 @@ -743,6 +742,8 @@
    4.12  lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
    4.13  unfolding real_sgn_eq by simp
    4.14  
    4.15 +lemma norm_conv_dist: "norm x = dist x 0"
    4.16 +  unfolding dist_norm by simp
    4.17  
    4.18  subsection {* Bounded Linear and Bilinear Operators *}
    4.19  
     5.1 --- a/src/HOL/SEQ.thy	Fri Mar 22 10:41:43 2013 +0100
     5.2 +++ b/src/HOL/SEQ.thy	Fri Mar 22 10:41:43 2013 +0100
     5.3 @@ -13,64 +13,6 @@
     5.4  imports Limits
     5.5  begin
     5.6  
     5.7 -subsection {* Defintions of limits *}
     5.8 -
     5.9 -definition
    5.10 -  Bseq :: "(nat => 'a::real_normed_vector) => bool" where
    5.11 -    --{*Standard definition for bounded sequence*}
    5.12 -  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    5.13 -
    5.14 -subsection {* Bounded Sequences *}
    5.15 -
    5.16 -lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
    5.17 -unfolding Bseq_def
    5.18 -proof (intro exI conjI allI)
    5.19 -  show "0 < max K 1" by simp
    5.20 -next
    5.21 -  fix n::nat
    5.22 -  have "norm (X n) \<le> K" by (rule K)
    5.23 -  thus "norm (X n) \<le> max K 1" by simp
    5.24 -qed
    5.25 -
    5.26 -lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    5.27 -unfolding Bseq_def by auto
    5.28 -
    5.29 -lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
    5.30 -proof (rule BseqI')
    5.31 -  let ?A = "norm ` X ` {..N}"
    5.32 -  have 1: "finite ?A" by simp
    5.33 -  fix n::nat
    5.34 -  show "norm (X n) \<le> max K (Max ?A)"
    5.35 -  proof (cases rule: linorder_le_cases)
    5.36 -    assume "n \<ge> N"
    5.37 -    hence "norm (X n) \<le> K" using K by simp
    5.38 -    thus "norm (X n) \<le> max K (Max ?A)" by simp
    5.39 -  next
    5.40 -    assume "n \<le> N"
    5.41 -    hence "norm (X n) \<in> ?A" by simp
    5.42 -    with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge)
    5.43 -    thus "norm (X n) \<le> max K (Max ?A)" by simp
    5.44 -  qed
    5.45 -qed
    5.46 -
    5.47 -lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))"
    5.48 -unfolding Bseq_def by auto
    5.49 -
    5.50 -lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
    5.51 -apply (erule BseqE)
    5.52 -apply (rule_tac N="k" and K="K" in BseqI2')
    5.53 -apply clarify
    5.54 -apply (drule_tac x="n - k" in spec, simp)
    5.55 -done
    5.56 -
    5.57 -lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
    5.58 -unfolding Bfun_def eventually_sequentially
    5.59 -apply (rule iffI)
    5.60 -apply (simp add: Bseq_def)
    5.61 -apply (auto intro: BseqI2')
    5.62 -done
    5.63 -
    5.64 -
    5.65  subsection {* Limits of Sequences *}
    5.66  
    5.67  lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
    5.68 @@ -105,7 +47,7 @@
    5.69  lemma Bseq_inverse:
    5.70    fixes a :: "'a::real_normed_div_algebra"
    5.71    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
    5.72 -unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
    5.73 +  by (rule Bfun_inverse)
    5.74  
    5.75  lemma LIMSEQ_diff_approach_zero:
    5.76    fixes L :: "'a::real_normed_vector"
    5.77 @@ -188,7 +130,25 @@
    5.78  
    5.79  subsection {* Bounded Monotonic Sequences *}
    5.80  
    5.81 -text{*Bounded Sequence*}
    5.82 +subsubsection {* Bounded Sequences *}
    5.83 +
    5.84 +lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
    5.85 +  by (intro BfunI) (auto simp: eventually_sequentially)
    5.86 +
    5.87 +lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
    5.88 +  by (intro BfunI) (auto simp: eventually_sequentially)
    5.89 +
    5.90 +lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
    5.91 +  unfolding Bfun_def eventually_sequentially
    5.92 +proof safe
    5.93 +  fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
    5.94 +  then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
    5.95 +    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
    5.96 +       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
    5.97 +qed auto
    5.98 +
    5.99 +lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   5.100 +unfolding Bseq_def by auto
   5.101  
   5.102  lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
   5.103  by (simp add: Bseq_def)
   5.104 @@ -280,11 +240,11 @@
   5.105  (* TODO: delete *)
   5.106  (* FIXME: one use in NSA/HSEQ.thy *)
   5.107  lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
   5.108 -unfolding tendsto_def eventually_sequentially
   5.109 -apply (rule_tac x = "X m" in exI, safe)
   5.110 -apply (rule_tac x = m in exI, safe)
   5.111 -apply (drule spec, erule impE, auto)
   5.112 -done
   5.113 +  apply (rule_tac x="X m" in exI)
   5.114 +  apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
   5.115 +  unfolding eventually_sequentially
   5.116 +  apply blast
   5.117 +  done
   5.118  
   5.119  text {* A monotone sequence converges to its least upper bound. *}
   5.120  
   5.121 @@ -317,7 +277,7 @@
   5.122     "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
   5.123    by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
   5.124  
   5.125 -lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
   5.126 +lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   5.127    by (simp add: Bseq_def)
   5.128  
   5.129  text{*Main monotonicity theorem*}
   5.130 @@ -354,18 +314,6 @@
   5.131  apply simp
   5.132  done
   5.133  
   5.134 -lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
   5.135 -apply (simp add: Cauchy_iff)
   5.136 -apply (drule spec, drule mp, rule zero_less_one, safe)
   5.137 -apply (drule_tac x="M" in spec, simp)
   5.138 -apply (drule lemmaCauchy)
   5.139 -apply (rule_tac k="M" in Bseq_offset)
   5.140 -apply (simp add: Bseq_def)
   5.141 -apply (rule_tac x="1 + norm (X M)" in exI)
   5.142 -apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp)
   5.143 -apply (simp add: order_less_imp_le)
   5.144 -done
   5.145 -
   5.146  class banach = real_normed_vector + complete_space
   5.147  
   5.148  instance real :: banach by default
     6.1 --- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     6.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     6.3 @@ -643,6 +643,17 @@
     6.4    shows "eventually P sequentially"
     6.5  using assms by (auto simp: eventually_sequentially)
     6.6  
     6.7 +lemma eventually_sequentially_seg:
     6.8 +  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
     6.9 +  unfolding eventually_sequentially
    6.10 +  apply safe
    6.11 +   apply (rule_tac x="N + k" in exI)
    6.12 +   apply rule
    6.13 +   apply (erule_tac x="n - k" in allE)
    6.14 +   apply auto []
    6.15 +  apply (rule_tac x=N in exI)
    6.16 +  apply auto []
    6.17 +  done
    6.18  
    6.19  subsubsection {* Standard filters *}
    6.20  
    6.21 @@ -1354,25 +1365,13 @@
    6.22  
    6.23  lemma LIMSEQ_ignore_initial_segment:
    6.24    "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
    6.25 -apply (rule topological_tendstoI)
    6.26 -apply (drule (2) topological_tendstoD)
    6.27 -apply (simp only: eventually_sequentially)
    6.28 -apply (erule exE, rename_tac N)
    6.29 -apply (rule_tac x=N in exI)
    6.30 -apply simp
    6.31 -done
    6.32 +  unfolding tendsto_def
    6.33 +  by (subst eventually_sequentially_seg[where k=k])
    6.34  
    6.35  lemma LIMSEQ_offset:
    6.36    "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
    6.37 -apply (rule topological_tendstoI)
    6.38 -apply (drule (2) topological_tendstoD)
    6.39 -apply (simp only: eventually_sequentially)
    6.40 -apply (erule exE, rename_tac N)
    6.41 -apply (rule_tac x="N + k" in exI)
    6.42 -apply clarify
    6.43 -apply (drule_tac x="n - k" in spec)
    6.44 -apply (simp add: le_diff_conv2)
    6.45 -done
    6.46 +  unfolding tendsto_def
    6.47 +  by (subst (asm) eventually_sequentially_seg[where k=k])
    6.48  
    6.49  lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
    6.50  by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)