(* 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) alsohave"?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 ?caseby simp qed simp_all alsohave"... \ (\k_::real. f (of_nat k)))" by (intro sum_mono integral_le int) (auto intro: dec) alsohave"... = (\k alsohave"\ - (\k\n. f (of_nat k)) = -(\k\{..n} - {.. by (subst sum_diff) auto alsohave"\ \ 0" by (auto intro!: sum_nonneg nonneg) finallyshow"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) alsohave"?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) alsohave"?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) finallyshow"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') alsohave"... \ 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 finallyshow ?thesis by simp qed
end
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
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.
