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.86  qed (simp_all add: pos)
    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.101  lemma conv_radius_cong_weak [cong]: "(\<And>n. f n = g n) \<Longrightarrow> conv_radius f = conv_radius g"
   1.102 @@ -505,7 +505,7 @@
   1.103    shows   "conv_radius f = conv_radius g"
   1.104    unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
   1.105  
   1.106 -lemma abs_summable_in_conv_radius:
   1.107 +theorem abs_summable_in_conv_radius:
   1.108    fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.109    assumes "ereal (norm z) < conv_radius f"
   1.110    shows   "summable (\<lambda>n. norm (f n * z ^ n))"
   1.111 @@ -543,7 +543,7 @@
   1.112    shows   "summable (\<lambda>n. f n * z ^ n)"
   1.113    by (rule summable_norm_cancel, rule abs_summable_in_conv_radius) fact+
   1.114  
   1.115 -lemma not_summable_outside_conv_radius:
   1.116 +theorem not_summable_outside_conv_radius:
   1.117    fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   1.118    assumes "ereal (norm z) > conv_radius f"
   1.119    shows   "\<not>summable (\<lambda>n. f n * z ^ n)"