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))"