src/HOL/Analysis/Integral_Test.thy
 changeset 68643 3db6c9338ec1 parent 64267 b9a1486e79be child 70136 f03a01a18c6e
```     1.1 --- a/src/HOL/Analysis/Integral_Test.thy	Mon Jul 16 15:24:06 2018 +0200
1.2 +++ b/src/HOL/Analysis/Integral_Test.thy	Mon Jul 16 17:50:07 2018 +0200
1.3 @@ -19,7 +19,7 @@
1.4  \<close>
1.5
1.6  (* TODO: continuous_in \<rightarrow> integrable_on *)
1.7 -locale antimono_fun_sum_integral_diff =
1.8 +locale%important antimono_fun_sum_integral_diff =
1.9    fixes f :: "real \<Rightarrow> real"
1.10    assumes dec: "\<And>x y. x \<ge> 0 \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
1.11    assumes nonneg: "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
1.12 @@ -89,7 +89,7 @@
1.13    using sum_integral_diff_series_Bseq sum_integral_diff_series_monoseq
1.14    by (blast intro!: Bseq_monoseq_convergent)
1.15
1.16 -lemma integral_test:
1.17 +theorem integral_test:
1.18    "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. integral {0..of_nat n} f)"
1.19  proof -
1.20    have "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))"
```