Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: testtracker.vdmsl Sprache: Isabelle

Original von: Isabelle^©

(*  Title:    HOL/Analysis/Integral_Test.thy
    Author:   Manuel Eberl, TU München
*)

section \<open>Integral Test for Summability\<close>

theory Integral_Test
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
  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)
\<close>

(* TODO: continuous_in \<rightarrow> integrable_on *)
locale\<^marker>\<open>tag important\<close> antimono_fun_sum_integral_diff =
  fixes f :: "real \ real"
  assumes dec: "\x y. x \ 0 \ x \ y \ f x \ f y"
  assumes nonneg: "\x. x \ 0 \ f x \ 0"
  assumes cont: "continuous_on {0..} f"
begin

definition "sum_integral_diff_series n = (\k\n. f (of_nat k)) - (integral {0..of_nat n} f)"

lemma sum_integral_diff_series_nonneg:
  "sum_integral_diff_series n \ 0"
proof -
  note int = integrable_continuous_real[OF continuous_on_subset[OF cont]]
  let ?int = "\a b. integral {of_nat a..of_nat b} f"
  have "-sum_integral_diff_series n = ?int 0 n - (\k\n. f (of_nat k))"
    by (simp add: sum_integral_diff_series_def)
  also have "?int 0 n = (\k
  proof (induction n)
    case (Suc n)
    have "?int 0 (Suc n) = ?int 0 n + ?int n (Suc n)"
      by (intro integral_combine[symmetric] int) simp_all
    with Suc show ?case by simp
  qed simp_all
  also have "... \ (\k_::real. f (of_nat k)))"
    by (intro sum_mono integral_le int) (auto intro: dec)
  also have "... = (\k
  also have "\ - (\k\n. f (of_nat k)) = -(\k\{..n} - {..
    by (subst sum_diff) auto
  also have "\ \ 0" by (auto intro!: sum_nonneg nonneg)
  finally show "sum_integral_diff_series n \ 0" by simp
qed

lemma sum_integral_diff_series_antimono:
  assumes "m \ n"
  shows   "sum_integral_diff_series m \ sum_integral_diff_series n"
proof -
  let ?int = "\a b. integral {of_nat a..of_nat b} f"
  note int = integrable_continuous_real[OF continuous_on_subset[OF cont]]
  have d_mono: "sum_integral_diff_series (Suc n) \ sum_integral_diff_series n" for n
  proof -
    fix n :: nat
    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)"
      by (subst integral_combine [symmetric, of "of_nat 0" "of_nat n" "of_nat (Suc n)"])
         (auto intro!: int simp: algebra_simps)
    also have "?int n (Suc n) \ integral {of_nat n..of_nat (Suc n)} (\_::real. f (of_nat (Suc n)))"
      by (intro integral_le int) (auto intro: dec)
    hence "f (of_nat (Suc n)) + -?int n (Suc n) \ 0" by (simp add: algebra_simps)
    finally show "sum_integral_diff_series (Suc n) \ sum_integral_diff_series n" by simp
  qed
  with assms show ?thesis
    by (induction rule: inc_induct) (auto intro: order.trans[OF _ d_mono])
qed

lemma sum_integral_diff_series_Bseq: "Bseq sum_integral_diff_series"
proof -
  from sum_integral_diff_series_nonneg and sum_integral_diff_series_antimono
    have "norm (sum_integral_diff_series n) \ sum_integral_diff_series 0" for n by simp
  thus "Bseq sum_integral_diff_series" by (rule BseqI')
qed

lemma sum_integral_diff_series_monoseq: "monoseq sum_integral_diff_series"
  using sum_integral_diff_series_antimono unfolding monoseq_def by blast

lemma sum_integral_diff_series_convergent: "convergent sum_integral_diff_series"
  using sum_integral_diff_series_Bseq sum_integral_diff_series_monoseq
  by (blast intro!: Bseq_monoseq_convergent)

theorem integral_test:
  "summable (\n. f (of_nat n)) \ convergent (\n. integral {0..of_nat n} f)"
proof -
  have "summable (\n. f (of_nat n)) \ convergent (\n. \k\n. f (of_nat k))"
    by (simp add: summable_iff_convergent')
  also have "... \ convergent (\n. integral {0..of_nat n} f)"
  proof
    assume "convergent (\n. \k\n. f (of_nat k))"
    from convergent_diff[OF this sum_integral_diff_series_convergent]
      show "convergent (\n. integral {0..of_nat n} f)"
        unfolding sum_integral_diff_series_def by simp
  next
    assume "convergent (\n. integral {0..of_nat n} f)"
    from convergent_add[OF this sum_integral_diff_series_convergent]
      show "convergent (\n. \k\n. f (of_nat k))" unfolding sum_integral_diff_series_def by simp
  qed
  finally show ?thesis by simp
qed

end

end

¤ Dauer der Verarbeitung: 0.38 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.