equal
deleted
inserted
replaced
5 section \<open>Radius of Convergence and Summation Tests\<close> |
5 section \<open>Radius of Convergence and Summation Tests\<close> |
6 |
6 |
7 theory Summation_Tests |
7 theory Summation_Tests |
8 imports |
8 imports |
9 Complex_Main |
9 Complex_Main |
10 "~~/src/HOL/Library/Discrete" |
10 "HOL-Library.Discrete" |
11 "~~/src/HOL/Library/Extended_Real" |
11 "HOL-Library.Extended_Real" |
12 "~~/src/HOL/Library/Liminf_Limsup" |
12 "HOL-Library.Liminf_Limsup" |
13 begin |
13 begin |
14 |
14 |
15 text \<open> |
15 text \<open> |
16 The definition of the radius of convergence of a power series, |
16 The definition of the radius of convergence of a power series, |
17 various summability tests, lemmas to compute the radius of convergence etc. |
17 various summability tests, lemmas to compute the radius of convergence etc. |