src/HOL/Real_Vector_Spaces.thy
changeset 61531 ab2e862263e7
parent 61524 f2e51e704a96
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Oct 29 15:40:52 2015 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Nov 02 11:56:28 2015 +0100
     1.3 @@ -228,6 +228,14 @@
     1.4  apply (erule (1) nonzero_inverse_scaleR_distrib)
     1.5  done
     1.6  
     1.7 +lemma setsum_constant_scaleR:
     1.8 +  fixes y :: "'a::real_vector"
     1.9 +  shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
    1.10 +  apply (cases "finite A")
    1.11 +  apply (induct set: finite)
    1.12 +  apply (simp_all add: algebra_simps)
    1.13 +  done
    1.14 +
    1.15  lemma real_vector_affinity_eq:
    1.16    fixes x :: "'a :: real_vector"
    1.17    assumes m0: "m \<noteq> 0"
    1.18 @@ -1614,6 +1622,12 @@
    1.19    apply auto
    1.20    done
    1.21  
    1.22 +lemma eventually_at_left_real: "a > (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {b<..<a}) (at_left a)"
    1.23 +  by (subst eventually_at, rule exI[of _ "a - b"]) (force simp: dist_real_def)
    1.24 +
    1.25 +lemma eventually_at_right_real: "a < (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {a<..<b}) (at_right a)"
    1.26 +  by (subst eventually_at, rule exI[of _ "b - a"]) (force simp: dist_real_def)
    1.27 +
    1.28  lemma metric_tendsto_imp_tendsto:
    1.29    fixes a :: "'a :: metric_space" and b :: "'b :: metric_space"
    1.30    assumes f: "(f ---> a) F"
    1.31 @@ -1709,12 +1723,36 @@
    1.32  definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
    1.33    "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
    1.34  
    1.35 -subsection \<open>Cauchy Sequences\<close>
    1.36 +lemma Cauchy_altdef:
    1.37 +  "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
    1.38 +proof
    1.39 +  assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
    1.40 +  show "Cauchy f" unfolding Cauchy_def
    1.41 +  proof (intro allI impI)
    1.42 +    fix e :: real assume e: "e > 0"
    1.43 +    with A obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n > m \<Longrightarrow> dist (f m) (f n) < e" by blast
    1.44 +    have "dist (f m) (f n) < e" if "m \<ge> M" "n \<ge> M" for m n
    1.45 +      using M[of m n] M[of n m] e that by (cases m n rule: linorder_cases) (auto simp: dist_commute)
    1.46 +    thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m) (f n) < e" by blast
    1.47 +  qed
    1.48 +next
    1.49 +  assume "Cauchy f"
    1.50 +  show "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" 
    1.51 +  proof (intro allI impI)
    1.52 +    fix e :: real assume e: "e > 0"
    1.53 +    with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
    1.54 +      unfolding Cauchy_def by fast
    1.55 +    thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
    1.56 +  qed
    1.57 +qed
    1.58  
    1.59  lemma metric_CauchyI:
    1.60    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
    1.61    by (simp add: Cauchy_def)
    1.62  
    1.63 +lemma CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
    1.64 +  unfolding Cauchy_altdef by blast
    1.65 +
    1.66  lemma metric_CauchyD:
    1.67    "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
    1.68    by (simp add: Cauchy_def)