Tagged some more files in HOL-Analysis
authorManuel Eberl <eberlm@in.tum.de>
Mon Jul 16 17:50:07 2018 +0200 (9 months ago)
changeset 686433db6c9338ec1
parent 68642 d812b6ee711b
child 68645 5e15795788d3
Tagged some more files in HOL-Analysis
src/HOL/Analysis/FPS_Convergence.thy
src/HOL/Analysis/Generalised_Binomial_Theorem.thy
src/HOL/Analysis/Harmonic_Numbers.thy
src/HOL/Analysis/Integral_Test.thy
src/HOL/Analysis/Summation_Tests.thy
     1.1 --- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Jul 16 15:24:06 2018 +0200
     1.2 +++ b/src/HOL/Analysis/FPS_Convergence.thy	Mon Jul 16 17:50:07 2018 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    "HOL-Computational_Algebra.Formal_Power_Series"
     1.5  begin
     1.6  
     1.7 -subsection \<open>Balls with extended real radius\<close>
     1.8 +subsection%unimportant \<open>Balls with extended real radius\<close>
     1.9  
    1.10  text \<open>
    1.11    The following is a variant of @{const ball} that also allows an infinite radius.
    1.12 @@ -54,13 +54,13 @@
    1.13  
    1.14  subsection \<open>Basic properties of convergent power series\<close>
    1.15  
    1.16 -definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
    1.17 +definition%important fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
    1.18    "fps_conv_radius f = conv_radius (fps_nth f)"
    1.19  
    1.20 -definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.21 +definition%important eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.22    "eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)"
    1.23  
    1.24 -definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
    1.25 +definition%important fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
    1.26    "fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
    1.27  
    1.28  lemma norm_summable_fps:
    1.29 @@ -73,7 +73,7 @@
    1.30    shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)"
    1.31    by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
    1.32  
    1.33 -lemma sums_eval_fps:
    1.34 +theorem sums_eval_fps:
    1.35    fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
    1.36    assumes "norm z < fps_conv_radius f"
    1.37    shows   "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z"
    1.38 @@ -194,7 +194,7 @@
    1.39  qed
    1.40  
    1.41  
    1.42 -subsection \<open>Lower bounds on radius of convergence\<close>
    1.43 +subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
    1.44  
    1.45  lemma fps_conv_radius_deriv:
    1.46    fixes f :: "'a :: {banach, real_normed_field} fps"
    1.47 @@ -447,12 +447,12 @@
    1.48  
    1.49  subsection \<open>Evaluating power series\<close>
    1.50  
    1.51 -lemma eval_fps_deriv:
    1.52 +theorem eval_fps_deriv:
    1.53    assumes "norm z < fps_conv_radius f"
    1.54    shows   "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
    1.55    by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)
    1.56  
    1.57 -lemma fps_nth_conv_deriv:
    1.58 +theorem fps_nth_conv_deriv:
    1.59    fixes f :: "complex fps"
    1.60    assumes "fps_conv_radius f > 0"
    1.61    shows   "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
    1.62 @@ -478,7 +478,7 @@
    1.63    finally show ?case by (simp add: divide_simps)
    1.64  qed
    1.65  
    1.66 -lemma eval_fps_eqD:
    1.67 +theorem eval_fps_eqD:
    1.68    fixes f g :: "complex fps"
    1.69    assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0"
    1.70    assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)"
    1.71 @@ -792,7 +792,8 @@
    1.72    the coefficients of the series with the singularities of the function, this predicate
    1.73    is enough.
    1.74  \<close>
    1.75 -definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
    1.76 +definition%important
    1.77 +  has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
    1.78    (infixl "has'_fps'_expansion" 60) 
    1.79    where "(f has_fps_expansion F) \<longleftrightarrow> 
    1.80              fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
    1.81 @@ -1261,7 +1262,7 @@
    1.82      by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
    1.83  qed
    1.84  
    1.85 -lemma residue_fps_expansion_over_power_at_0:
    1.86 +theorem residue_fps_expansion_over_power_at_0:
    1.87    assumes "f has_fps_expansion F"
    1.88    shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
    1.89  proof -
     2.1 --- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 15:24:06 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 17:50:07 2018 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4    with a show ?thesis by simp
     2.5  qed
     2.6  
     2.7 -lemma gen_binomial_complex:
     2.8 +theorem gen_binomial_complex:
     2.9    fixes z :: complex
    2.10    assumes "norm z < 1"
    2.11    shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"
     3.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Jul 16 15:24:06 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Jul 16 17:50:07 2018 +0200
     3.3 @@ -19,7 +19,7 @@
     3.4  
     3.5  subsection \<open>The Harmonic numbers\<close>
     3.6  
     3.7 -definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
     3.8 +definition%important harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
     3.9    "harm n = (\<Sum>k=1..n. inverse (of_nat k))"
    3.10  
    3.11  lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))"
    3.12 @@ -54,7 +54,7 @@
    3.13    finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" .
    3.14  qed (simp_all add: harm_def)
    3.15  
    3.16 -lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
    3.17 +theorem not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
    3.18  proof -
    3.19    have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow>
    3.20              convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm)
    3.21 @@ -156,7 +156,7 @@
    3.22    thus ?thesis by (subst (asm) convergent_Suc_iff)
    3.23  qed
    3.24  
    3.25 -lemma euler_mascheroni_LIMSEQ:
    3.26 +lemma%important euler_mascheroni_LIMSEQ:
    3.27    "(\<lambda>n. harm n - ln (of_nat n) :: real) \<longlonglongrightarrow> euler_mascheroni"
    3.28    unfolding euler_mascheroni_def
    3.29    by (simp add: convergent_LIMSEQ_iff [symmetric] euler_mascheroni_convergent)
    3.30 @@ -187,7 +187,7 @@
    3.31    thus ?thesis by simp
    3.32  qed
    3.33  
    3.34 -lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
    3.35 +theorem alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
    3.36  proof -
    3.37    let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
    3.38    let ?g = "\<lambda>n. if even n then 0 else (2::real)"
    3.39 @@ -250,7 +250,7 @@
    3.40  qed
    3.41  
    3.42  
    3.43 -subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
    3.44 +subsection%unimportant \<open>Bounds on the Euler-Mascheroni constant\<close>
    3.45  
    3.46  (* TODO: Move? *)
    3.47  lemma ln_inverse_approx_le:
    3.48 @@ -340,9 +340,9 @@
    3.49  
    3.50  
    3.51  lemma euler_mascheroni_lower:
    3.52 -        "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
    3.53 -  and euler_mascheroni_upper:
    3.54 -        "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
    3.55 +          "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
    3.56 +    and euler_mascheroni_upper:
    3.57 +          "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
    3.58  proof -
    3.59    define D :: "_ \<Rightarrow> real"
    3.60      where "D n = inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))" for n
     4.1 --- a/src/HOL/Analysis/Integral_Test.thy	Mon Jul 16 15:24:06 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Integral_Test.thy	Mon Jul 16 17:50:07 2018 +0200
     4.3 @@ -19,7 +19,7 @@
     4.4  \<close>
     4.5  
     4.6  (* TODO: continuous_in \<rightarrow> integrable_on *)
     4.7 -locale antimono_fun_sum_integral_diff =
     4.8 +locale%important antimono_fun_sum_integral_diff =
     4.9    fixes f :: "real \<Rightarrow> real"
    4.10    assumes dec: "\<And>x y. x \<ge> 0 \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
    4.11    assumes nonneg: "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
    4.12 @@ -89,7 +89,7 @@
    4.13    using sum_integral_diff_series_Bseq sum_integral_diff_series_monoseq
    4.14    by (blast intro!: Bseq_monoseq_convergent)
    4.15  
    4.16 -lemma integral_test:
    4.17 +theorem integral_test:
    4.18    "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. integral {0..of_nat n} f)"
    4.19  proof -
    4.20    have "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))"
     5.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Mon Jul 16 15:24:06 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Mon Jul 16 17:50:07 2018 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4    shows   "limsup (\<lambda>n. ereal (root n (norm (f n)))) = ereal l"
     5.5    by (intro limsup_root_limit tendsto_ereal assms)
     5.6  
     5.7 -lemma root_test_convergence':
     5.8 +theorem root_test_convergence':
     5.9    fixes f :: "nat \<Rightarrow> 'a :: banach"
    5.10    defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
    5.11    assumes l: "l < 1"
    5.12 @@ -82,7 +82,7 @@
    5.13      by (rule summable_comparison_test_ev[OF _ summable_geometric]) (simp add: c)
    5.14  qed
    5.15  
    5.16 -lemma root_test_divergence:
    5.17 +theorem root_test_divergence:
    5.18    fixes f :: "nat \<Rightarrow> 'a :: banach"
    5.19    defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
    5.20    assumes l: "l > 1"
    5.21 @@ -167,7 +167,7 @@
    5.22    finally show ?case by simp
    5.23  qed simp
    5.24  
    5.25 -lemma condensation_test:
    5.26 +theorem condensation_test:
    5.27    assumes mono: "\<And>m. 0 < m \<Longrightarrow> f (Suc m) \<le> f m"
    5.28    assumes nonneg: "\<And>n. f n \<ge> 0"
    5.29    shows "summable f \<longleftrightarrow> summable (\<lambda>n. 2^n * f (2^n))"
    5.30 @@ -273,7 +273,7 @@
    5.31    finally show ?thesis .
    5.32  qed
    5.33  
    5.34 -lemma summable_complex_powr_iff:
    5.35 +theorem summable_complex_powr_iff:
    5.36    assumes "Re s < -1"
    5.37    shows   "summable (\<lambda>n. exp (of_real (ln (of_nat n)) * s))"
    5.38    by (rule summable_norm_cancel, subst abs_summable_complex_powr_iff) fact
    5.39 @@ -312,7 +312,7 @@
    5.40  
    5.41  subsubsection \<open>Kummer's test\<close>
    5.42  
    5.43 -lemma kummers_test_convergence:
    5.44 +theorem kummers_test_convergence:
    5.45    fixes f p :: "nat \<Rightarrow> real"
    5.46    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
    5.47    assumes nonneg_p: "eventually (\<lambda>n. p n \<ge> 0) sequentially"
    5.48 @@ -372,7 +372,7 @@
    5.49  qed
    5.50  
    5.51  
    5.52 -lemma kummers_test_divergence:
    5.53 +theorem kummers_test_divergence:
    5.54    fixes f p :: "nat \<Rightarrow> real"
    5.55    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
    5.56    assumes pos_p: "eventually (\<lambda>n. p n > 0) sequentially"
    5.57 @@ -403,7 +403,7 @@
    5.58  
    5.59  subsubsection \<open>Ratio test\<close>
    5.60  
    5.61 -lemma ratio_test_convergence:
    5.62 +theorem ratio_test_convergence:
    5.63    fixes f :: "nat \<Rightarrow> real"
    5.64    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
    5.65    defines "l \<equiv> liminf (\<lambda>n. ereal (f n / f (Suc n)))"
    5.66 @@ -417,7 +417,7 @@
    5.67      by (cases "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
    5.68  qed simp
    5.69  
    5.70 -lemma ratio_test_divergence:
    5.71 +theorem ratio_test_divergence:
    5.72    fixes f :: "nat \<Rightarrow> real"
    5.73    assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
    5.74    defines "l \<equiv> limsup (\<lambda>n. ereal (f n / f (Suc n)))"
    5.75 @@ -434,7 +434,7 @@
    5.76  
    5.77  subsubsection \<open>Raabe's test\<close>
    5.78  
    5.79 -lemma raabes_test_convergence:
    5.80 +theorem raabes_test_convergence:
    5.81  fixes f :: "nat \<Rightarrow> real"
    5.82    assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
    5.83    defines "l \<equiv> liminf (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
    5.84 @@ -449,7 +449,7 @@
    5.85    finally show "?l' > 0" by (cases ?l') (simp_all add: algebra_simps)
    5.86  qed (simp_all add: pos)
    5.87  
    5.88 -lemma raabes_test_divergence:
    5.89 +theorem raabes_test_divergence:
    5.90  fixes f :: "nat \<Rightarrow> real"
    5.91    assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
    5.92    defines "l \<equiv> limsup (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
    5.93 @@ -473,7 +473,7 @@
    5.94    all inputs with a norm that is smaller than that radius and to diverge for all inputs with a
    5.95    norm that is greater.
    5.96  \<close>
    5.97 -definition conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
    5.98 +definition%important conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
    5.99    "conv_radius f = inverse (limsup (\<lambda>n. ereal (root n (norm (f n)))))"
   5.100  
   5.101  lemma conv_radius_cong_weak [cong]: "(\<And>n. f n = g n) \<Longrightarrow> conv_radius f = conv_radius g"
   5.102 @@ -505,7 +505,7 @@
   5.103    shows   "conv_radius f = conv_radius g"
   5.104    unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
   5.105  
   5.106 -lemma abs_summable_in_conv_radius:
   5.107 +theorem abs_summable_in_conv_radius:
   5.108    fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   5.109    assumes "ereal (norm z) < conv_radius f"
   5.110    shows   "summable (\<lambda>n. norm (f n * z ^ n))"
   5.111 @@ -543,7 +543,7 @@
   5.112    shows   "summable (\<lambda>n. f n * z ^ n)"
   5.113    by (rule summable_norm_cancel, rule abs_summable_in_conv_radius) fact+
   5.114  
   5.115 -lemma not_summable_outside_conv_radius:
   5.116 +theorem not_summable_outside_conv_radius:
   5.117    fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
   5.118    assumes "ereal (norm z) > conv_radius f"
   5.119    shows   "\<not>summable (\<lambda>n. f n * z ^ n)"