author hoelzl Tue Jan 05 13:35:06 2016 +0100 (2016-01-05) changeset 62055 755fda743c49 parent 62054 cff7114e4572 child 62057 af58628952f0
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
```     1.1 --- a/src/HOL/Library/Nonpos_Ints.thy	Mon Jan 04 22:13:53 2016 +0100
1.2 +++ b/src/HOL/Library/Nonpos_Ints.thy	Tue Jan 05 13:35:06 2016 +0100
1.3 @@ -1,15 +1,17 @@
1.4 -(*
1.5 -  Title:    HOL/Library/Nonpos_Ints.thy
1.6 -  Author:   Manuel Eberl, TU München
1.7 -
1.8 -  The set of non-positive integers on a ring. (in analogy to the set of non-negative
1.9 -  integers @{term "\<nat>"}) This is useful e.g. for the Gamma function.
1.10 +(*  Title:    HOL/Library/Nonpos_Ints.thy
1.11 +    Author:   Manuel Eberl, TU München
1.12  *)
1.13 +
1.14 +section \<open>Non-positive integers\<close>
1.15 +
1.16  theory Nonpos_Ints
1.17  imports Complex_Main
1.18  begin
1.19
1.20 -subsection \<open>Non-positive integers\<close>
1.21 +text \<open>
1.22 +  The set of non-positive integers on a ring. (in analogy to the set of non-negative
1.23 +  integers @{term "\<nat>"}) This is useful e.g. for the Gamma function.
1.24 +\<close>
1.25
1.26  definition nonpos_Ints ("\<int>\<^sub>\<le>\<^sub>0") where "\<int>\<^sub>\<le>\<^sub>0 = {of_int n |n. n \<le> 0}"
1.27
```
```     2.1 --- a/src/HOL/Library/Periodic_Fun.thy	Mon Jan 04 22:13:53 2016 +0100
2.2 +++ b/src/HOL/Library/Periodic_Fun.thy	Tue Jan 05 13:35:06 2016 +0100
2.3 @@ -1,16 +1,18 @@
2.4 -(*
2.5 -  Title:    HOL/Library/Periodic_Fun.thy
2.6 -  Author:   Manuel Eberl, TU München
2.7 -
2.8 -  A locale for periodic functions. The idea is that one proves \$f(x + p) = f(x)\$
2.9 -  for some period \$p\$ and gets derived results like \$f(x - p) = f(x)\$ and \$f(x + 2p) = f(x)\$
2.11 +(*  Title:    HOL/Library/Periodic_Fun.thy
2.12 +    Author:   Manuel Eberl, TU München
2.13  *)
2.14 +
2.15 +section \<open>Periodic Functions\<close>
2.16 +
2.17  theory Periodic_Fun
2.18  imports Complex_Main
2.19  begin
2.20
2.21  text \<open>
2.22 +  A locale for periodic functions. The idea is that one proves \$f(x + p) = f(x)\$
2.23 +  for some period \$p\$ and gets derived results like \$f(x - p) = f(x)\$ and \$f(x + 2p) = f(x)\$
2.25 +
2.26    @{term g} and @{term gm} are ``plus/minus k periods'' functions.
2.27    @{term g1} and @{term gn1} are ``plus/minus one period'' functions.
2.28    This is useful e.g. if the period is one; the lemmas one gets are then
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jan 04 22:13:53 2016 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Tue Jan 05 13:35:06 2016 +0100
3.3 @@ -1,15 +1,9 @@
3.4 -(*
3.5 -  Title:    HOL/Multivariate_Analysis/Gamma.thy
3.6 -  Author:   Manuel Eberl, TU München
3.7 -
3.8 -  Several equivalent definitions of the Gamma function and its
3.9 -  most important properties. Also contains the definition and some properties
3.10 -  of the log-Gamma function and the Digamma function and the other Polygamma functions.
3.11 -
3.12 -  Based on the Gamma function, we also prove the Weierstraß product form of the
3.13 -  sin function and, based on this, the solution of the Basel problem (the
3.14 -  sum over all @{term "1 / (n::nat)^2"}.
3.15 +(*  Title:    HOL/Multivariate_Analysis/Gamma.thy
3.16 +    Author:   Manuel Eberl, TU München
3.17  *)
3.18 +
3.19 +section \<open>The Gamma Function\<close>
3.20 +
3.21  theory Gamma
3.22  imports
3.23    Complex_Transcendental
3.24 @@ -19,6 +13,16 @@
3.25    "~~/src/HOL/Library/Periodic_Fun"
3.26  begin
3.27
3.28 +text \<open>
3.29 +  Several equivalent definitions of the Gamma function and its
3.30 +  most important properties. Also contains the definition and some properties
3.31 +  of the log-Gamma function and the Digamma function and the other Polygamma functions.
3.32 +
3.33 +  Based on the Gamma function, we also prove the Weierstraß product form of the
3.34 +  sin function and, based on this, the solution of the Basel problem (the
3.35 +  sum over all @{term "1 / (n::nat)^2"}.
3.36 +\<close>
3.37 +
3.38  lemma pochhammer_eq_0_imp_nonpos_Int:
3.39    "pochhammer (x::'a::field_char_0) n = 0 \<Longrightarrow> x \<in> \<int>\<^sub>\<le>\<^sub>0"
3.40    by (auto simp: pochhammer_eq_0_iff)
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Mon Jan 04 22:13:53 2016 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Tue Jan 05 13:35:06 2016 +0100
4.3 @@ -1,9 +1,15 @@
4.4 -(*
4.5 -  Title:    HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy
4.6 -  Author:   Manuel Eberl, TU München
4.7 -
4.8 +(*  Title:    HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy
4.9 +    Author:   Manuel Eberl, TU München
4.10 +*)
4.11 +
4.12 +section \<open>Generalised Binomial Theorem\<close>
4.13 +
4.14 +text \<open>
4.15    The proof of the Generalised Binomial Theorem and related results.
4.16 -*)
4.17 +  We prove the generalised binomial theorem for complex numbers, following the proof at:
4.18 +  \url{https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem}
4.19 +\<close>
4.20 +
4.21  theory Generalised_Binomial_Theorem
4.22  imports
4.23    Complex_Main
4.24 @@ -11,13 +17,6 @@
4.25    Summation
4.26  begin
4.27
4.28 -subsection \<open>The generalised binomial theorem\<close>
4.29 -
4.30 -text \<open>
4.31 -  We prove the generalised binomial theorem for complex numbers, following the proof at:
4.32 -  https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem
4.33 -\<close>
4.34 -
4.35  lemma gbinomial_ratio_limit:
4.36    fixes a :: "'a :: real_normed_field"
4.37    assumes "a \<notin> \<nat>"
```
```     5.1 --- a/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Mon Jan 04 22:13:53 2016 +0100
5.2 +++ b/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Tue Jan 05 13:35:06 2016 +0100
5.3 @@ -1,11 +1,9 @@
5.4 -(*
5.5 -  Title:    HOL/Multivariate_Analysis/Harmonic_Numbers.thy
5.6 -  Author:   Manuel Eberl, TU München
5.7 -
5.8 -  The definition of the Harmonic Numbers and the Euler–Mascheroni constant.
5.9 -  Also provides a reasonably accurate approximation of @{term "ln 2 :: real"}
5.10 -  and the Euler–Mascheroni constant.
5.11 +(*  Title:    HOL/Multivariate_Analysis/Harmonic_Numbers.thy
5.12 +    Author:   Manuel Eberl, TU München
5.13  *)
5.14 +
5.15 +section \<open>Harmonic Numbers\<close>
5.16 +
5.17  theory Harmonic_Numbers
5.18  imports
5.19    Complex_Transcendental
5.20 @@ -13,6 +11,12 @@
5.21    Integral_Test
5.22  begin
5.23
5.24 +text \<open>
5.25 +  The definition of the Harmonic Numbers and the Euler–Mascheroni constant.
5.26 +  Also provides a reasonably accurate approximation of @{term "ln 2 :: real"}
5.27 +  and the Euler–Mascheroni constant.
5.28 +\<close>
5.29 +
5.30  lemma ln_2_less_1: "ln 2 < (1::real)"
5.31  proof -
5.32    have "2 < 5/(2::real)" by simp
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Integral_Test.thy	Mon Jan 04 22:13:53 2016 +0100
6.2 +++ b/src/HOL/Multivariate_Analysis/Integral_Test.thy	Tue Jan 05 13:35:06 2016 +0100
6.3 @@ -1,7 +1,14 @@
6.4 -(*
6.5 -  Title:    HOL/Multivariate_Analysis/Integral_Test.thy
6.6 -  Author:   Manuel Eberl, TU München
6.7 +(*  Title:    HOL/Multivariate_Analysis/Integral_Test.thy
6.8 +    Author:   Manuel Eberl, TU München
6.9 +*)
6.10
6.11 +section \<open>Integral Test for Summability\<close>
6.12 +
6.13 +theory Integral_Test
6.14 +imports Integration
6.15 +begin
6.16 +
6.17 +text \<open>
6.18    The integral test for summability. We show here that for a decreasing non-negative
6.19    function, the infinite sum over that function evaluated at the natural numbers
6.20    converges iff the corresponding integral converges.
6.21 @@ -9,12 +16,7 @@
6.22    As a useful side result, we also provide some results on the difference between
6.23    the integral and the partial sum. (This is useful e.g. for the definition of the
6.24    Euler–Mascheroni constant)
6.25 -*)
6.26 -theory Integral_Test
6.27 -imports Integration
6.28 -begin
6.29 -
6.30 -subsubsection \<open>Integral test\<close>
6.31 +\<close>
6.32
6.33  (* TODO: continuous_in \<rightarrow> integrable_on *)
6.34  locale antimono_fun_sum_integral_diff =
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Summation.thy	Mon Jan 04 22:13:53 2016 +0100
7.2 +++ b/src/HOL/Multivariate_Analysis/Summation.thy	Tue Jan 05 13:35:06 2016 +0100
7.3 @@ -1,10 +1,9 @@
7.4 -(*
7.5 -  Title:    HOL/Multivariate_Analysis/Summation.thy
7.6 -  Author:   Manuel Eberl, TU München
7.7 +(*  Title:    HOL/Multivariate_Analysis/Summation.thy
7.8 +    Author:   Manuel Eberl, TU München
7.9 +*)
7.10
7.11 -  The definition of the radius of convergence of a power series,
7.12 -  various summability tests, lemmas to compute the radius of convergence etc.
7.13 -*)
7.14 +section \<open>Rounded dual logarithm\<close>
7.15 +
7.16  theory Summation
7.17  imports
7.18    Complex_Main
7.19 @@ -12,7 +11,10 @@
7.20    "~~/src/HOL/Library/Liminf_Limsup"
7.21  begin
7.22
7.23 -subsection \<open>Rounded dual logarithm\<close>
7.24 +text \<open>
7.25 +  The definition of the radius of convergence of a power series,
7.26 +  various summability tests, lemmas to compute the radius of convergence etc.
7.27 +\<close>
7.28
7.29  (* This is required for the Cauchy condensation criterion *)
7.30
```