# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1531756207 -7200
# Node ID 3db6c9338ec107d51767b391abcb1691561f23d7
# Parent  d812b6ee711bd14b0d3aa64c6676603345cdb670
Tagged some more files in HOL-Analysis

diff -r d812b6ee711b -r 3db6c9338ec1 src/HOL/Analysis/FPS_Convergence.thy
--- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Jul 16 15:24:06 2018 +0200
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Mon Jul 16 17:50:07 2018 +0200
@@ -13,7 +13,7 @@
   "HOL-Computational_Algebra.Formal_Power_Series"
 begin
 
-subsection \<open>Balls with extended real radius\<close>
+subsection%unimportant \<open>Balls with extended real radius\<close>
 
 text \<open>
   The following is a variant of @{const ball} that also allows an infinite radius.
@@ -54,13 +54,13 @@
 
 subsection \<open>Basic properties of convergent power series\<close>
 
-definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
+definition%important fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
   "fps_conv_radius f = conv_radius (fps_nth f)"
 
-definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
+definition%important eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
   "eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)"
 
-definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
+definition%important fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
   "fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
 
 lemma norm_summable_fps:
@@ -73,7 +73,7 @@
   shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)"
   by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
 
-lemma sums_eval_fps:
+theorem sums_eval_fps:
   fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
   assumes "norm z < fps_conv_radius f"
   shows   "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z"
@@ -194,7 +194,7 @@
 qed
 
 
-subsection \<open>Lower bounds on radius of convergence\<close>
+subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
 
 lemma fps_conv_radius_deriv:
   fixes f :: "'a :: {banach, real_normed_field} fps"
@@ -447,12 +447,12 @@
 
 subsection \<open>Evaluating power series\<close>
 
-lemma eval_fps_deriv:
+theorem eval_fps_deriv:
   assumes "norm z < fps_conv_radius f"
   shows   "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
   by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)
 
-lemma fps_nth_conv_deriv:
+theorem fps_nth_conv_deriv:
   fixes f :: "complex fps"
   assumes "fps_conv_radius f > 0"
   shows   "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
@@ -478,7 +478,7 @@
   finally show ?case by (simp add: divide_simps)
 qed
 
-lemma eval_fps_eqD:
+theorem eval_fps_eqD:
   fixes f g :: "complex fps"
   assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0"
   assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)"
@@ -792,7 +792,8 @@
   the coefficients of the series with the singularities of the function, this predicate
   is enough.
 \<close>
-definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
+definition%important
+  has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
   (infixl "has'_fps'_expansion" 60) 
   where "(f has_fps_expansion F) \<longleftrightarrow> 
             fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
@@ -1261,7 +1262,7 @@
     by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
 qed
 
-lemma residue_fps_expansion_over_power_at_0:
+theorem residue_fps_expansion_over_power_at_0:
   assumes "f has_fps_expansion F"
   shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
 proof -
diff -r d812b6ee711b -r 3db6c9338ec1 src/HOL/Analysis/Generalised_Binomial_Theorem.thy
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 15:24:06 2018 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 17:50:07 2018 +0200
@@ -70,7 +70,7 @@
   with a show ?thesis by simp
 qed
 
-lemma gen_binomial_complex:
+theorem gen_binomial_complex:
   fixes z :: complex
   assumes "norm z < 1"
   shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"
diff -r d812b6ee711b -r 3db6c9338ec1 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Jul 16 15:24:06 2018 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Jul 16 17:50:07 2018 +0200
@@ -19,7 +19,7 @@
 
 subsection \<open>The Harmonic numbers\<close>
 
-definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
+definition%important harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
   "harm n = (\<Sum>k=1..n. inverse (of_nat k))"
 
 lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))"
@@ -54,7 +54,7 @@
   finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" .
 qed (simp_all add: harm_def)
 
-lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
+theorem not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
 proof -
   have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow>
             convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm)
@@ -156,7 +156,7 @@
   thus ?thesis by (subst (asm) convergent_Suc_iff)
 qed
 
-lemma euler_mascheroni_LIMSEQ:
+lemma%important euler_mascheroni_LIMSEQ:
   "(\<lambda>n. harm n - ln (of_nat n) :: real) \<longlonglongrightarrow> euler_mascheroni"
   unfolding euler_mascheroni_def
   by (simp add: convergent_LIMSEQ_iff [symmetric] euler_mascheroni_convergent)
@@ -187,7 +187,7 @@
   thus ?thesis by simp
 qed
 
-lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
+theorem alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
 proof -
   let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
   let ?g = "\<lambda>n. if even n then 0 else (2::real)"
@@ -250,7 +250,7 @@
 qed
 
 
-subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
+subsection%unimportant \<open>Bounds on the Euler-Mascheroni constant\<close>
 
 (* TODO: Move? *)
 lemma ln_inverse_approx_le:
@@ -340,9 +340,9 @@
 
 
 lemma euler_mascheroni_lower:
-        "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
-  and euler_mascheroni_upper:
-        "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
+          "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
+    and euler_mascheroni_upper:
+          "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
 proof -
   define D :: "_ \<Rightarrow> real"
     where "D n = inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))" for n
diff -r d812b6ee711b -r 3db6c9338ec1 src/HOL/Analysis/Integral_Test.thy
--- a/src/HOL/Analysis/Integral_Test.thy	Mon Jul 16 15:24:06 2018 +0200
+++ b/src/HOL/Analysis/Integral_Test.thy	Mon Jul 16 17:50:07 2018 +0200
@@ -19,7 +19,7 @@
 \<close>
 
 (* TODO: continuous_in \<rightarrow> integrable_on *)
-locale antimono_fun_sum_integral_diff =
+locale%important antimono_fun_sum_integral_diff =
   fixes f :: "real \<Rightarrow> real"
   assumes dec: "\<And>x y. x \<ge> 0 \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
   assumes nonneg: "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
@@ -89,7 +89,7 @@
   using sum_integral_diff_series_Bseq sum_integral_diff_series_monoseq
   by (blast intro!: Bseq_monoseq_convergent)
 
-lemma integral_test:
+theorem integral_test:
   "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. integral {0..of_nat n} f)"
 proof -
   have "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))"
diff -r d812b6ee711b -r 3db6c9338ec1 src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Mon Jul 16 15:24:06 2018 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy	Mon Jul 16 17:50:07 2018 +0200
@@ -50,7 +50,7 @@
   shows   "limsup (\<lambda>n. ereal (root n (norm (f n)))) = ereal l"
   by (intro limsup_root_limit tendsto_ereal assms)
 
-lemma root_test_convergence':
+theorem root_test_convergence':
   fixes f :: "nat \<Rightarrow> 'a :: banach"
   defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
   assumes l: "l < 1"
@@ -82,7 +82,7 @@
     by (rule summable_comparison_test_ev[OF _ summable_geometric]) (simp add: c)
 qed
 
-lemma root_test_divergence:
+theorem root_test_divergence:
   fixes f :: "nat \<Rightarrow> 'a :: banach"
   defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
   assumes l: "l > 1"
@@ -167,7 +167,7 @@
   finally show ?case by simp
 qed simp
 
-lemma condensation_test:
+theorem condensation_test:
   assumes mono: "\<And>m. 0 < m \<Longrightarrow> f (Suc m) \<le> f m"
   assumes nonneg: "\<And>n. f n \<ge> 0"
   shows "summable f \<longleftrightarrow> summable (\<lambda>n. 2^n * f (2^n))"
@@ -273,7 +273,7 @@
   finally show ?thesis .
 qed
 
-lemma summable_complex_powr_iff:
+theorem summable_complex_powr_iff:
   assumes "Re s < -1"
   shows   "summable (\<lambda>n. exp (of_real (ln (of_nat n)) * s))"
   by (rule summable_norm_cancel, subst abs_summable_complex_powr_iff) fact
@@ -312,7 +312,7 @@
 
 subsubsection \<open>Kummer's test\<close>
 
-lemma kummers_test_convergence:
+theorem kummers_test_convergence:
   fixes f p :: "nat \<Rightarrow> real"
   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   assumes nonneg_p: "eventually (\<lambda>n. p n \<ge> 0) sequentially"
@@ -372,7 +372,7 @@
 qed
 
 
-lemma kummers_test_divergence:
+theorem kummers_test_divergence:
   fixes f p :: "nat \<Rightarrow> real"
   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   assumes pos_p: "eventually (\<lambda>n. p n > 0) sequentially"
@@ -403,7 +403,7 @@
 
 subsubsection \<open>Ratio test\<close>
 
-lemma ratio_test_convergence:
+theorem ratio_test_convergence:
   fixes f :: "nat \<Rightarrow> real"
   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   defines "l \<equiv> liminf (\<lambda>n. ereal (f n / f (Suc n)))"
@@ -417,7 +417,7 @@
     by (cases "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
 qed simp
 
-lemma ratio_test_divergence:
+theorem ratio_test_divergence:
   fixes f :: "nat \<Rightarrow> real"
   assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
   defines "l \<equiv> limsup (\<lambda>n. ereal (f n / f (Suc n)))"
@@ -434,7 +434,7 @@
 
 subsubsection \<open>Raabe's test\<close>
 
-lemma raabes_test_convergence:
+theorem raabes_test_convergence:
 fixes f :: "nat \<Rightarrow> real"
   assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
   defines "l \<equiv> liminf (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
@@ -449,7 +449,7 @@
   finally show "?l' > 0" by (cases ?l') (simp_all add: algebra_simps)
 qed (simp_all add: pos)
 
-lemma raabes_test_divergence:
+theorem raabes_test_divergence:
 fixes f :: "nat \<Rightarrow> real"
   assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
   defines "l \<equiv> limsup (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
@@ -473,7 +473,7 @@
   all inputs with a norm that is smaller than that radius and to diverge for all inputs with a
   norm that is greater.
 \<close>
-definition conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
+definition%important conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
   "conv_radius f = inverse (limsup (\<lambda>n. ereal (root n (norm (f n)))))"
 
 lemma conv_radius_cong_weak [cong]: "(\<And>n. f n = g n) \<Longrightarrow> conv_radius f = conv_radius g"
@@ -505,7 +505,7 @@
   shows   "conv_radius f = conv_radius g"
   unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
 
-lemma abs_summable_in_conv_radius:
+theorem abs_summable_in_conv_radius:
   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   assumes "ereal (norm z) < conv_radius f"
   shows   "summable (\<lambda>n. norm (f n * z ^ n))"
@@ -543,7 +543,7 @@
   shows   "summable (\<lambda>n. f n * z ^ n)"
   by (rule summable_norm_cancel, rule abs_summable_in_conv_radius) fact+
 
-lemma not_summable_outside_conv_radius:
+theorem not_summable_outside_conv_radius:
   fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   assumes "ereal (norm z) > conv_radius f"
   shows   "\<not>summable (\<lambda>n. f n * z ^ n)"