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