src/HOL/Analysis/Integral_Test.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 68643 3db6c9338ec1 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Title:    HOL/Analysis/Integral_Test.thy
```
```     2     Author:   Manuel Eberl, TU München
```
```     3 *)
```
```     4
```
```     5 section \<open>Integral Test for Summability\<close>
```
```     6
```
```     7 theory Integral_Test
```
```     8 imports Henstock_Kurzweil_Integration
```
```     9 begin
```
```    10
```
```    11 text \<open>
```
```    12   The integral test for summability. We show here that for a decreasing non-negative
```
```    13   function, the infinite sum over that function evaluated at the natural numbers
```
```    14   converges iff the corresponding integral converges.
```
```    15
```
```    16   As a useful side result, we also provide some results on the difference between
```
```    17   the integral and the partial sum. (This is useful e.g. for the definition of the
```
```    18   Euler-Mascheroni constant)
```
```    19 \<close>
```
```    20
```
```    21 (* TODO: continuous_in \<rightarrow> integrable_on *)
```
```    22 locale%important antimono_fun_sum_integral_diff =
```
```    23   fixes f :: "real \<Rightarrow> real"
```
```    24   assumes dec: "\<And>x y. x \<ge> 0 \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
```
```    25   assumes nonneg: "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
```
```    26   assumes cont: "continuous_on {0..} f"
```
```    27 begin
```
```    28
```
```    29 definition "sum_integral_diff_series n = (\<Sum>k\<le>n. f (of_nat k)) - (integral {0..of_nat n} f)"
```
```    30
```
```    31 lemma sum_integral_diff_series_nonneg:
```
```    32   "sum_integral_diff_series n \<ge> 0"
```
```    33 proof -
```
```    34   note int = integrable_continuous_real[OF continuous_on_subset[OF cont]]
```
```    35   let ?int = "\<lambda>a b. integral {of_nat a..of_nat b} f"
```
```    36   have "-sum_integral_diff_series n = ?int 0 n - (\<Sum>k\<le>n. f (of_nat k))"
```
```    37     by (simp add: sum_integral_diff_series_def)
```
```    38   also have "?int 0 n = (\<Sum>k<n. ?int k (Suc k))"
```
```    39   proof (induction n)
```
```    40     case (Suc n)
```
```    41     have "?int 0 (Suc n) = ?int 0 n + ?int n (Suc n)"
```
```    42       by (intro integral_combine[symmetric] int) simp_all
```
```    43     with Suc show ?case by simp
```
```    44   qed simp_all
```
```    45   also have "... \<le> (\<Sum>k<n. integral {of_nat k..of_nat (Suc k)} (\<lambda>_::real. f (of_nat k)))"
```
```    46     by (intro sum_mono integral_le int) (auto intro: dec)
```
```    47   also have "... = (\<Sum>k<n. f (of_nat k))" by simp
```
```    48   also have "\<dots> - (\<Sum>k\<le>n. f (of_nat k)) = -(\<Sum>k\<in>{..n} - {..<n}. f (of_nat k))"
```
```    49     by (subst sum_diff) auto
```
```    50   also have "\<dots> \<le> 0" by (auto intro!: sum_nonneg nonneg)
```
```    51   finally show "sum_integral_diff_series n \<ge> 0" by simp
```
```    52 qed
```
```    53
```
```    54 lemma sum_integral_diff_series_antimono:
```
```    55   assumes "m \<le> n"
```
```    56   shows   "sum_integral_diff_series m \<ge> sum_integral_diff_series n"
```
```    57 proof -
```
```    58   let ?int = "\<lambda>a b. integral {of_nat a..of_nat b} f"
```
```    59   note int = integrable_continuous_real[OF continuous_on_subset[OF cont]]
```
```    60   have d_mono: "sum_integral_diff_series (Suc n) \<le> sum_integral_diff_series n" for n
```
```    61   proof -
```
```    62     fix n :: nat
```
```    63     have "sum_integral_diff_series (Suc n) - sum_integral_diff_series n =
```
```    64             f (of_nat (Suc n)) + (?int 0 n - ?int 0 (Suc n))"
```
```    65       unfolding sum_integral_diff_series_def by (simp add: algebra_simps)
```
```    66     also have "?int 0 n - ?int 0 (Suc n) = -?int n (Suc n)"
```
```    67       by (subst integral_combine [symmetric, of "of_nat 0" "of_nat n" "of_nat (Suc n)"])
```
```    68          (auto intro!: int simp: algebra_simps)
```
```    69     also have "?int n (Suc n) \<ge> integral {of_nat n..of_nat (Suc n)} (\<lambda>_::real. f (of_nat (Suc n)))"
```
```    70       by (intro integral_le int) (auto intro: dec)
```
```    71     hence "f (of_nat (Suc n)) + -?int n (Suc n) \<le> 0" by (simp add: algebra_simps)
```
```    72     finally show "sum_integral_diff_series (Suc n) \<le> sum_integral_diff_series n" by simp
```
```    73   qed
```
```    74   with assms show ?thesis
```
```    75     by (induction rule: inc_induct) (auto intro: order.trans[OF _ d_mono])
```
```    76 qed
```
```    77
```
```    78 lemma sum_integral_diff_series_Bseq: "Bseq sum_integral_diff_series"
```
```    79 proof -
```
```    80   from sum_integral_diff_series_nonneg and sum_integral_diff_series_antimono
```
```    81     have "norm (sum_integral_diff_series n) \<le> sum_integral_diff_series 0" for n by simp
```
```    82   thus "Bseq sum_integral_diff_series" by (rule BseqI')
```
```    83 qed
```
```    84
```
```    85 lemma sum_integral_diff_series_monoseq: "monoseq sum_integral_diff_series"
```
```    86   using sum_integral_diff_series_antimono unfolding monoseq_def by blast
```
```    87
```
```    88 lemma sum_integral_diff_series_convergent: "convergent sum_integral_diff_series"
```
```    89   using sum_integral_diff_series_Bseq sum_integral_diff_series_monoseq
```
```    90   by (blast intro!: Bseq_monoseq_convergent)
```
```    91
```
```    92 theorem integral_test:
```
```    93   "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. integral {0..of_nat n} f)"
```
```    94 proof -
```
```    95   have "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))"
```
```    96     by (simp add: summable_iff_convergent')
```
```    97   also have "... \<longleftrightarrow> convergent (\<lambda>n. integral {0..of_nat n} f)"
```
```    98   proof
```
```    99     assume "convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))"
```
```   100     from convergent_diff[OF this sum_integral_diff_series_convergent]
```
```   101       show "convergent (\<lambda>n. integral {0..of_nat n} f)"
```
```   102         unfolding sum_integral_diff_series_def by simp
```
```   103   next
```
```   104     assume "convergent (\<lambda>n. integral {0..of_nat n} f)"
```
```   105     from convergent_add[OF this sum_integral_diff_series_convergent]
```
```   106       show "convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))" unfolding sum_integral_diff_series_def by simp
```
```   107   qed
```
```   108   finally show ?thesis by simp
```
```   109 qed
```
```   110
```
```   111 end
```
```   112
```
```   113 end
```