src/HOL/Series.thy
changeset 60758 d8d85a8172b5
parent 60141 833adf7db7d8
child 60867 86e7560e07d0
     1.1 --- a/src/HOL/Series.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Series.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -7,13 +7,13 @@
     1.4  Additional contributions by Jeremy Avigad
     1.5  *)
     1.6  
     1.7 -section {* Infinite Series *}
     1.8 +section \<open>Infinite Series\<close>
     1.9  
    1.10  theory Series
    1.11  imports Limits Inequalities
    1.12  begin 
    1.13  
    1.14 -subsection {* Definition of infinite summability *}
    1.15 +subsection \<open>Definition of infinite summability\<close>
    1.16  
    1.17  definition
    1.18    sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
    1.19 @@ -30,7 +30,7 @@
    1.20  where
    1.21    "suminf f = (THE s. f sums s)"
    1.22  
    1.23 -subsection {* Infinite summability on topological monoids *}
    1.24 +subsection \<open>Infinite summability on topological monoids\<close>
    1.25  
    1.26  lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
    1.27    by simp
    1.28 @@ -141,7 +141,7 @@
    1.29    by (rule sums_zero [THEN sums_unique, symmetric])
    1.30  
    1.31  
    1.32 -subsection {* Infinite summability on ordered, topological monoids *}
    1.33 +subsection \<open>Infinite summability on ordered, topological monoids\<close>
    1.34  
    1.35  lemma sums_le:
    1.36    fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    1.37 @@ -221,7 +221,7 @@
    1.38        by (auto intro: le_less_trans simp: eventually_sequentially) }
    1.39  qed
    1.40  
    1.41 -subsection {* Infinite summability on real normed vector spaces *}
    1.42 +subsection \<open>Infinite summability on real normed vector spaces\<close>
    1.43  
    1.44  lemma sums_Suc_iff:
    1.45    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.46 @@ -303,10 +303,10 @@
    1.47    fixes r :: real assumes "0 < r" and "summable f"
    1.48    shows "\<exists>N. \<forall>n\<ge>N. norm (\<Sum>i. f (i + n)) < r"
    1.49  proof -
    1.50 -  from LIMSEQ_D[OF summable_LIMSEQ[OF `summable f`] `0 < r`]
    1.51 +  from LIMSEQ_D[OF summable_LIMSEQ[OF \<open>summable f\<close>] \<open>0 < r\<close>]
    1.52    obtain N :: nat where "\<forall> n \<ge> N. norm (setsum f {..<n} - suminf f) < r" by auto
    1.53    thus ?thesis
    1.54 -    by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF `summable f`])
    1.55 +    by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF \<open>summable f\<close>])
    1.56  qed
    1.57  
    1.58  lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
    1.59 @@ -324,7 +324,7 @@
    1.60  lemma summable_minus_iff:
    1.61    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.62    shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
    1.63 -  by (auto dest: summable_minus) --{*used two ways, hence must be outside the context above*}
    1.64 +  by (auto dest: summable_minus) --\<open>used two ways, hence must be outside the context above\<close>
    1.65  
    1.66  
    1.67  context
    1.68 @@ -363,7 +363,7 @@
    1.69  lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
    1.70  lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
    1.71  
    1.72 -subsection {* Infinite summability on real normed algebras *}
    1.73 +subsection \<open>Infinite summability on real normed algebras\<close>
    1.74  
    1.75  context
    1.76    fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra"
    1.77 @@ -389,7 +389,7 @@
    1.78  
    1.79  end
    1.80  
    1.81 -subsection {* Infinite summability on real normed fields *}
    1.82 +subsection \<open>Infinite summability on real normed fields\<close>
    1.83  
    1.84  context
    1.85    fixes c :: "'a::real_normed_field"
    1.86 @@ -404,7 +404,7 @@
    1.87  lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
    1.88    by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
    1.89  
    1.90 -text{*Sum of a geometric progression.*}
    1.91 +text\<open>Sum of a geometric progression.\<close>
    1.92  
    1.93  lemma geometric_sums: "norm c < 1 \<Longrightarrow> (\<lambda>n. c^n) sums (1 / (1 - c))"
    1.94  proof -
    1.95 @@ -439,9 +439,9 @@
    1.96      by simp
    1.97  qed
    1.98  
    1.99 -subsection {* Infinite summability on Banach spaces *}
   1.100 +subsection \<open>Infinite summability on Banach spaces\<close>
   1.101  
   1.102 -text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   1.103 +text\<open>Cauchy-type criterion for convergence of series (c.f. Harrison)\<close>
   1.104  
   1.105  lemma summable_Cauchy:
   1.106    fixes f :: "nat \<Rightarrow> 'a::banach"
   1.107 @@ -465,7 +465,7 @@
   1.108    fixes f :: "nat \<Rightarrow> 'a::banach"
   1.109  begin  
   1.110  
   1.111 -text{*Absolute convergence imples normal convergence*}
   1.112 +text\<open>Absolute convergence imples normal convergence\<close>
   1.113  
   1.114  lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
   1.115    apply (simp only: summable_Cauchy, safe)
   1.116 @@ -480,7 +480,7 @@
   1.117  lemma summable_norm: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
   1.118    by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_LIMSEQ norm_setsum)
   1.119  
   1.120 -text {* Comparison tests *}
   1.121 +text \<open>Comparison tests\<close>
   1.122  
   1.123  lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f"
   1.124    apply (simp add: summable_Cauchy, safe)
   1.125 @@ -499,7 +499,7 @@
   1.126  lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
   1.127    by (rule summable_comparison_test) auto
   1.128  
   1.129 -subsection {* The Ratio Test*}
   1.130 +subsection \<open>The Ratio Test\<close>
   1.131  
   1.132  lemma summable_ratio_test: 
   1.133    assumes "c < 1" "\<And>n. n \<ge> N \<Longrightarrow> norm (f (Suc n)) \<le> c * norm (f n)"
   1.134 @@ -514,12 +514,12 @@
   1.135        proof (induct rule: inc_induct)
   1.136          case (step m)
   1.137          moreover have "norm (f (Suc m)) / c ^ Suc m * c ^ n \<le> norm (f m) / c ^ m * c ^ n"
   1.138 -          using `0 < c` `c < 1` assms(2)[OF `N \<le> m`] by (simp add: field_simps)
   1.139 +          using \<open>0 < c\<close> \<open>c < 1\<close> assms(2)[OF \<open>N \<le> m\<close>] by (simp add: field_simps)
   1.140          ultimately show ?case by simp
   1.141 -      qed (insert `0 < c`, simp)
   1.142 +      qed (insert \<open>0 < c\<close>, simp)
   1.143      qed
   1.144      show "summable (\<lambda>n. norm (f N) / c ^ N * c ^ n)"
   1.145 -      using `0 < c` `c < 1` by (intro summable_mult summable_geometric) simp
   1.146 +      using \<open>0 < c\<close> \<open>c < 1\<close> by (intro summable_mult summable_geometric) simp
   1.147    qed
   1.148  next
   1.149    assume c: "\<not> 0 < c"
   1.150 @@ -536,7 +536,7 @@
   1.151  
   1.152  end
   1.153  
   1.154 -text{*Relations among convergence and absolute convergence for power series.*}
   1.155 +text\<open>Relations among convergence and absolute convergence for power series.\<close>
   1.156  
   1.157  lemma abel_lemma:
   1.158    fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.159 @@ -557,7 +557,7 @@
   1.160  qed
   1.161  
   1.162  
   1.163 -text{*Summability of geometric series for real algebras*}
   1.164 +text\<open>Summability of geometric series for real algebras\<close>
   1.165  
   1.166  lemma complete_algebra_summable_geometric:
   1.167    fixes x :: "'a::{real_normed_algebra_1,banach}"
   1.168 @@ -569,12 +569,12 @@
   1.169      by (simp add: summable_geometric)
   1.170  qed
   1.171  
   1.172 -subsection {* Cauchy Product Formula *}
   1.173 +subsection \<open>Cauchy Product Formula\<close>
   1.174  
   1.175 -text {*
   1.176 +text \<open>
   1.177    Proof based on Analysis WebNotes: Chapter 07, Class 41
   1.178    @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
   1.179 -*}
   1.180 +\<close>
   1.181  
   1.182  lemma Cauchy_product_sums:
   1.183    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.184 @@ -655,7 +655,7 @@
   1.185    using a b
   1.186    by (rule Cauchy_product_sums [THEN sums_unique])
   1.187  
   1.188 -subsection {* Series on @{typ real}s *}
   1.189 +subsection \<open>Series on @{typ real}s\<close>
   1.190  
   1.191  lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
   1.192    by (rule summable_comparison_test) auto
   1.193 @@ -702,7 +702,7 @@
   1.194      also have "\<dots> \<le> (\<Sum>i<m. f i)"
   1.195        by (rule setsum_mono3) (auto simp add: pos n[rule_format])
   1.196      also have "\<dots> \<le> suminf f"
   1.197 -      using `summable f` 
   1.198 +      using \<open>summable f\<close> 
   1.199        by (rule setsum_le_suminf) (simp add: pos)
   1.200      finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f" by simp
   1.201    qed