# HG changeset patch
# User hoelzl
# Date 1451997306 -3600
# Node ID 755fda743c49415efc12e963ea0af1a05102206a
# Parent  cff7114e45720a7fcf2f76ea91d248bcde9caeeb
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)

diff -r cff7114e4572 -r 755fda743c49 src/HOL/Library/Nonpos_Ints.thy
--- 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}"
 
diff -r cff7114e4572 -r 755fda743c49 src/HOL/Library/Periodic_Fun.thy
--- 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)$
-  for free.
+(*  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)$
+  for free.
+
   @{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 
diff -r cff7114e4572 -r 755fda743c49 src/HOL/Multivariate_Analysis/Gamma.thy
--- 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)
diff -r cff7114e4572 -r 755fda743c49 src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy
--- 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>"
diff -r cff7114e4572 -r 755fda743c49 src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy
--- 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
diff -r cff7114e4572 -r 755fda743c49 src/HOL/Multivariate_Analysis/Integral_Test.thy
--- 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 =
diff -r cff7114e4572 -r 755fda743c49 src/HOL/Multivariate_Analysis/Summation.thy
--- 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 *)