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.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.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
```