src/HOL/Analysis/Summation_Tests.thy
 changeset 68643 3db6c9338ec1 parent 68532 f8b98d31ad45 child 69597 ff784d5a5bfb
```     1.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Mon Jul 16 15:24:06 2018 +0200
1.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Mon Jul 16 17:50:07 2018 +0200
1.3 @@ -50,7 +50,7 @@
1.4    shows   "limsup (\<lambda>n. ereal (root n (norm (f n)))) = ereal l"
1.5    by (intro limsup_root_limit tendsto_ereal assms)
1.6
1.7 -lemma root_test_convergence':
1.8 +theorem root_test_convergence':
1.9    fixes f :: "nat \<Rightarrow> 'a :: banach"
1.10    defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
1.11    assumes l: "l < 1"
1.12 @@ -82,7 +82,7 @@
1.13      by (rule summable_comparison_test_ev[OF _ summable_geometric]) (simp add: c)
1.14  qed
1.15
1.16 -lemma root_test_divergence:
1.17 +theorem root_test_divergence:
1.18    fixes f :: "nat \<Rightarrow> 'a :: banach"
1.19    defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
1.20    assumes l: "l > 1"
1.21 @@ -167,7 +167,7 @@
1.22    finally show ?case by simp
1.23  qed simp
1.24
1.25 -lemma condensation_test:
1.26 +theorem condensation_test:
1.27    assumes mono: "\<And>m. 0 < m \<Longrightarrow> f (Suc m) \<le> f m"
1.28    assumes nonneg: "\<And>n. f n \<ge> 0"
1.29    shows "summable f \<longleftrightarrow> summable (\<lambda>n. 2^n * f (2^n))"
1.30 @@ -273,7 +273,7 @@
1.31    finally show ?thesis .
1.32  qed
1.33
1.34 -lemma summable_complex_powr_iff:
1.35 +theorem summable_complex_powr_iff:
1.36    assumes "Re s < -1"
1.37    shows   "summable (\<lambda>n. exp (of_real (ln (of_nat n)) * s))"
1.38    by (rule summable_norm_cancel, subst abs_summable_complex_powr_iff) fact
1.39 @@ -312,7 +312,7 @@
1.40
1.41  subsubsection \<open>Kummer's test\<close>
1.42
1.43 -lemma kummers_test_convergence:
1.44 +theorem kummers_test_convergence:
1.45    fixes f p :: "nat \<Rightarrow> real"
1.46    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
1.47    assumes nonneg_p: "eventually (\<lambda>n. p n \<ge> 0) sequentially"
1.48 @@ -372,7 +372,7 @@
1.49  qed
1.50
1.51
1.52 -lemma kummers_test_divergence:
1.53 +theorem kummers_test_divergence:
1.54    fixes f p :: "nat \<Rightarrow> real"
1.55    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
1.56    assumes pos_p: "eventually (\<lambda>n. p n > 0) sequentially"
1.57 @@ -403,7 +403,7 @@
1.58
1.59  subsubsection \<open>Ratio test\<close>
1.60
1.61 -lemma ratio_test_convergence:
1.62 +theorem ratio_test_convergence:
1.63    fixes f :: "nat \<Rightarrow> real"
1.64    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
1.65    defines "l \<equiv> liminf (\<lambda>n. ereal (f n / f (Suc n)))"
1.66 @@ -417,7 +417,7 @@
1.67      by (cases "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
1.68  qed simp
1.69
1.70 -lemma ratio_test_divergence:
1.71 +theorem ratio_test_divergence:
1.72    fixes f :: "nat \<Rightarrow> real"
1.73    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
1.74    defines "l \<equiv> limsup (\<lambda>n. ereal (f n / f (Suc n)))"
1.75 @@ -434,7 +434,7 @@
1.76
1.77  subsubsection \<open>Raabe's test\<close>
1.78
1.79 -lemma raabes_test_convergence:
1.80 +theorem raabes_test_convergence:
1.81  fixes f :: "nat \<Rightarrow> real"
1.82    assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
1.83    defines "l \<equiv> liminf (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
1.84 @@ -449,7 +449,7 @@
1.85    finally show "?l' > 0" by (cases ?l') (simp_all add: algebra_simps)
1.87
1.88 -lemma raabes_test_divergence:
1.89 +theorem raabes_test_divergence:
1.90  fixes f :: "nat \<Rightarrow> real"
1.91    assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
1.92    defines "l \<equiv> limsup (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
1.93 @@ -473,7 +473,7 @@
1.94    all inputs with a norm that is smaller than that radius and to diverge for all inputs with a
1.95    norm that is greater.
1.96  \<close>
1.97 -definition conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
1.98 +definition%important conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
1.99    "conv_radius f = inverse (limsup (\<lambda>n. ereal (root n (norm (f n)))))"
1.100
1.102 @@ -505,7 +505,7 @@
1.104    unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
1.105