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