src/HOL/Multivariate_Analysis/Integral_Test.thy

--- a/src/HOL/Multivariate_Analysis/Integral_Test.thy	Thu Aug 04 18:45:28 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integral_Test.thy	Thu Aug 04 19:36:31 2016 +0200
@@ -1,18 +1,18 @@
 (*  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
+imports Henstock_Kurzweil_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 
+  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.
-  
+
   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)
@@ -33,7 +33,7 @@
 proof -
   note int = integrable_continuous_real[OF continuous_on_subset[OF cont]]
   let ?int = "\<lambda>a b. integral {of_nat a..of_nat b} f"
-  have "-sum_integral_diff_series n = ?int 0 n - (\<Sum>k\<le>n. f (of_nat k))" 
+  have "-sum_integral_diff_series n = ?int 0 n - (\<Sum>k\<le>n. f (of_nat k))"
     by (simp add: sum_integral_diff_series_def)
   also have "?int 0 n = (\<Sum>k<n. ?int k (Suc k))"
   proof (induction n)
@@ -60,7 +60,7 @@
   have d_mono: "sum_integral_diff_series (Suc n) \<le> sum_integral_diff_series n" for n
   proof -
     fix n :: nat
-    have "sum_integral_diff_series (Suc n) - sum_integral_diff_series n = 
+    have "sum_integral_diff_series (Suc n) - sum_integral_diff_series n =
             f (of_nat (Suc n)) + (?int 0 n - ?int 0 (Suc n))"
       unfolding sum_integral_diff_series_def by (simp add: algebra_simps)
     also have "?int 0 n - ?int 0 (Suc n) = -?int n (Suc n)"
@@ -77,7 +77,7 @@
 
 lemma sum_integral_diff_series_Bseq: "Bseq sum_integral_diff_series"
 proof -
-  from sum_integral_diff_series_nonneg and sum_integral_diff_series_antimono 
+  from sum_integral_diff_series_nonneg and sum_integral_diff_series_antimono
     have "norm (sum_integral_diff_series n) \<le> sum_integral_diff_series 0" for n by simp
   thus "Bseq sum_integral_diff_series" by (rule BseqI')
 qed
@@ -97,12 +97,12 @@
   also have "... \<longleftrightarrow> convergent (\<lambda>n. integral {0..of_nat n} f)"
   proof
     assume "convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))"
-    from convergent_diff[OF this sum_integral_diff_series_convergent] 
-      show "convergent (\<lambda>n. integral {0..of_nat n} f)" 
+    from convergent_diff[OF this sum_integral_diff_series_convergent]
+      show "convergent (\<lambda>n. integral {0..of_nat n} f)"
         unfolding sum_integral_diff_series_def by simp
   next
     assume "convergent (\<lambda>n. integral {0..of_nat n} f)"
-    from convergent_add[OF this sum_integral_diff_series_convergent] 
+    from convergent_add[OF this sum_integral_diff_series_convergent]
       show "convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))" unfolding sum_integral_diff_series_def by simp
   qed
   finally show ?thesis by simp