author hoelzl Tue, 05 Jan 2016 13:35:06 +0100 changeset 62055 755fda743c49 parent 62054 cff7114e4572 child 62057 af58628952f0
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
```--- a/src/HOL/Library/Nonpos_Ints.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Library/Nonpos_Ints.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,15 +1,17 @@
-(*
-  Title:    HOL/Library/Nonpos_Ints.thy
-  Author:   Manuel Eberl, TU München
-
-  The set of non-positive integers on a ring. (in analogy to the set of non-negative
-  integers @{term "\<nat>"}) This is useful e.g. for the Gamma function.
+(*  Title:    HOL/Library/Nonpos_Ints.thy
+    Author:   Manuel Eberl, TU München
*)
+
+section \<open>Non-positive integers\<close>
+
theory Nonpos_Ints
imports Complex_Main
begin

-subsection \<open>Non-positive integers\<close>
+text \<open>
+  The set of non-positive integers on a ring. (in analogy to the set of non-negative
+  integers @{term "\<nat>"}) This is useful e.g. for the Gamma function.
+\<close>

definition nonpos_Ints ("\<int>\<^sub>\<le>\<^sub>0") where "\<int>\<^sub>\<le>\<^sub>0 = {of_int n |n. n \<le> 0}"
```
```--- a/src/HOL/Library/Periodic_Fun.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Library/Periodic_Fun.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,16 +1,18 @@
-(*
-  Title:    HOL/Library/Periodic_Fun.thy
-  Author:   Manuel Eberl, TU München
-
-  A locale for periodic functions. The idea is that one proves \$f(x + p) = f(x)\$
-  for some period \$p\$ and gets derived results like \$f(x - p) = f(x)\$ and \$f(x + 2p) = f(x)\$
+(*  Title:    HOL/Library/Periodic_Fun.thy
+    Author:   Manuel Eberl, TU München
*)
+
+section \<open>Periodic Functions\<close>
+
theory Periodic_Fun
imports Complex_Main
begin

text \<open>
+  A locale for periodic functions. The idea is that one proves \$f(x + p) = f(x)\$
+  for some period \$p\$ and gets derived results like \$f(x - p) = f(x)\$ and \$f(x + 2p) = f(x)\$
+
@{term g} and @{term gm} are ``plus/minus k periods'' functions.
@{term g1} and @{term gn1} are ``plus/minus one period'' functions.
This is useful e.g. if the period is one; the lemmas one gets are then ```
```--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,15 +1,9 @@
-(*
-  Title:    HOL/Multivariate_Analysis/Gamma.thy
-  Author:   Manuel Eberl, TU München
-
-  Several equivalent definitions of the Gamma function and its
-  most important properties. Also contains the definition and some properties
-  of the log-Gamma function and the Digamma function and the other Polygamma functions.
-
-  Based on the Gamma function, we also prove the Weierstraß product form of the
-  sin function and, based on this, the solution of the Basel problem (the
-  sum over all @{term "1 / (n::nat)^2"}.
+(*  Title:    HOL/Multivariate_Analysis/Gamma.thy
+    Author:   Manuel Eberl, TU München
*)
+
+section \<open>The Gamma Function\<close>
+
theory Gamma
imports
Complex_Transcendental
@@ -19,6 +13,16 @@
"~~/src/HOL/Library/Periodic_Fun"
begin

+text \<open>
+  Several equivalent definitions of the Gamma function and its
+  most important properties. Also contains the definition and some properties
+  of the log-Gamma function and the Digamma function and the other Polygamma functions.
+
+  Based on the Gamma function, we also prove the Weierstraß product form of the
+  sin function and, based on this, the solution of the Basel problem (the
+  sum over all @{term "1 / (n::nat)^2"}.
+\<close>
+
lemma pochhammer_eq_0_imp_nonpos_Int:
"pochhammer (x::'a::field_char_0) n = 0 \<Longrightarrow> x \<in> \<int>\<^sub>\<le>\<^sub>0"
by (auto simp: pochhammer_eq_0_iff)```
```--- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,9 +1,15 @@
-(*
-  Title:    HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy
-  Author:   Manuel Eberl, TU München
-
+(*  Title:    HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy
+    Author:   Manuel Eberl, TU München
+*)
+
+section \<open>Generalised Binomial Theorem\<close>
+
+text \<open>
The proof of the Generalised Binomial Theorem and related results.
-*)
+  We prove the generalised binomial theorem for complex numbers, following the proof at:
+  \url{https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem}
+\<close>
+
theory Generalised_Binomial_Theorem
imports
Complex_Main
@@ -11,13 +17,6 @@
Summation
begin

-subsection \<open>The generalised binomial theorem\<close>
-
-text \<open>
-  We prove the generalised binomial theorem for complex numbers, following the proof at:
-  https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem
-\<close>
-
lemma gbinomial_ratio_limit:
fixes a :: "'a :: real_normed_field"
assumes "a \<notin> \<nat>"```
```--- a/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,11 +1,9 @@
-(*
-  Title:    HOL/Multivariate_Analysis/Harmonic_Numbers.thy
-  Author:   Manuel Eberl, TU München
-
-  The definition of the Harmonic Numbers and the Euler–Mascheroni constant.
-  Also provides a reasonably accurate approximation of @{term "ln 2 :: real"}
-  and the Euler–Mascheroni constant.
+(*  Title:    HOL/Multivariate_Analysis/Harmonic_Numbers.thy
+    Author:   Manuel Eberl, TU München
*)
+
+section \<open>Harmonic Numbers\<close>
+
theory Harmonic_Numbers
imports
Complex_Transcendental
@@ -13,6 +11,12 @@
Integral_Test
begin

+text \<open>
+  The definition of the Harmonic Numbers and the Euler–Mascheroni constant.
+  Also provides a reasonably accurate approximation of @{term "ln 2 :: real"}
+  and the Euler–Mascheroni constant.
+\<close>
+
lemma ln_2_less_1: "ln 2 < (1::real)"
proof -
have "2 < 5/(2::real)" by simp```
```--- a/src/HOL/Multivariate_Analysis/Integral_Test.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integral_Test.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,7 +1,14 @@
-(*
-  Title:    HOL/Multivariate_Analysis/Integral_Test.thy
-  Author:   Manuel Eberl, TU München
+(*  Title:    HOL/Multivariate_Analysis/Integral_Test.thy
+    Author:   Manuel Eberl, TU München
+*)

+section \<open>Integral Test for Summability\<close>
+
+theory Integral_Test
+imports Integration
+begin
+
+text \<open>
The integral test for summability. We show here that for a decreasing non-negative
function, the infinite sum over that function evaluated at the natural numbers
converges iff the corresponding integral converges.
@@ -9,12 +16,7 @@
As a useful side result, we also provide some results on the difference between
the integral and the partial sum. (This is useful e.g. for the definition of the
Euler–Mascheroni constant)
-*)
-theory Integral_Test
-imports Integration
-begin
-
-subsubsection \<open>Integral test\<close>
+\<close>

(* TODO: continuous_in \<rightarrow> integrable_on *)
locale antimono_fun_sum_integral_diff =```
```--- a/src/HOL/Multivariate_Analysis/Summation.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Summation.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,10 +1,9 @@
-(*
-  Title:    HOL/Multivariate_Analysis/Summation.thy
-  Author:   Manuel Eberl, TU München
+(*  Title:    HOL/Multivariate_Analysis/Summation.thy
+    Author:   Manuel Eberl, TU München
+*)

-  The definition of the radius of convergence of a power series,
-  various summability tests, lemmas to compute the radius of convergence etc.
-*)
+section \<open>Rounded dual logarithm\<close>
+
theory Summation
imports
Complex_Main
@@ -12,7 +11,10 @@
"~~/src/HOL/Library/Liminf_Limsup"
begin

-subsection \<open>Rounded dual logarithm\<close>
+text \<open>
+  The definition of the radius of convergence of a power series,
+  various summability tests, lemmas to compute the radius of convergence etc.
+\<close>

(* This is required for the Cauchy condensation criterion *)
```