--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Aug 20 03:35:20 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sun Aug 20 18:55:03 2017 +0200
@@ -247,6 +247,19 @@
lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
by (simp add: exp_eq)
+lemma exp_integer_2pi_plus1:
+ assumes "n \<in> \<int>"
+ shows "exp(((2 * n + 1) * pi) * \<i>) = - 1"
+proof -
+ from assms obtain n' where [simp]: "n = of_int n'"
+ by (auto simp: Ints_def)
+ have "exp(((2 * n + 1) * pi) * \<i>) = exp (pi * \<i>)"
+ using assms by (subst exp_eq) (auto intro!: exI[of _ n'] simp: algebra_simps)
+ also have "... = - 1"
+ by simp
+ finally show ?thesis .
+qed
+
lemma inj_on_exp_pi:
fixes z::complex shows "inj_on exp (ball z pi)"
proof (clarsimp simp: inj_on_def exp_eq)
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Sun Aug 20 03:35:20 2017 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Sun Aug 20 18:55:03 2017 +0200
@@ -61,7 +61,7 @@
have "eventually (\<lambda>n. (a gchoose n) = 0) sequentially"
using eventually_gt_at_top[of "nat \<lfloor>norm a\<rfloor>"]
by eventually_elim (insert a, auto elim!: Nats_cases simp: binomial_gbinomial[symmetric])
- from conv_radius_cong[OF this] a show ?thesis by simp
+ from conv_radius_cong'[OF this] a show ?thesis by simp
next
assume a: "a \<notin> \<nat>"
from tendsto_norm[OF gbinomial_ratio_limit[OF this]]
--- a/src/HOL/Analysis/Summation_Tests.thy Sun Aug 20 03:35:20 2017 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy Sun Aug 20 18:55:03 2017 +0200
@@ -465,7 +465,6 @@
qed (insert pos eventually_gt_at_top[of "0::nat"] not_summable_harmonic, simp_all)
-
subsection \<open>Radius of convergence\<close>
text \<open>
@@ -477,6 +476,9 @@
definition 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"
+ by (drule ext) simp_all
+
lemma conv_radius_nonneg: "conv_radius f \<ge> 0"
proof -
have "0 = limsup (\<lambda>n. 0)" by (subst Limsup_const) simp_all
@@ -489,19 +491,20 @@
lemma conv_radius_zero [simp]: "conv_radius (\<lambda>_. 0) = \<infinity>"
by (auto simp: conv_radius_def zero_ereal_def [symmetric] Limsup_const)
-lemma conv_radius_cong:
- assumes "eventually (\<lambda>x. f x = g x) sequentially"
- shows "conv_radius f = conv_radius g"
-proof -
- have "eventually (\<lambda>n. ereal (root n (norm (f n))) = ereal (root n (norm (g n)))) sequentially"
- using assms by eventually_elim simp
- from Limsup_eq[OF this] show ?thesis unfolding conv_radius_def by simp
-qed
-
lemma conv_radius_altdef:
"conv_radius f = liminf (\<lambda>n. inverse (ereal (root n (norm (f n)))))"
by (subst Liminf_inverse_ereal) (simp_all add: real_root_ge_zero conv_radius_def)
+lemma conv_radius_cong':
+ assumes "eventually (\<lambda>x. f x = g x) sequentially"
+ shows "conv_radius f = conv_radius g"
+ unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
+
+lemma conv_radius_cong:
+ assumes "eventually (\<lambda>x. norm (f x) = norm (g x)) sequentially"
+ 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:
fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
assumes "ereal (norm z) < conv_radius f"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Aug 20 03:35:20 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Aug 20 18:55:03 2017 +0200
@@ -1736,6 +1736,17 @@
by force
qed
+lemma subset_box_complex:
+ "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
+ (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
+ "cbox a b \<subseteq> box c d \<longleftrightarrow>
+ (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a > Re c \<and> Im a > Im c \<and> Re b < Re d \<and> Im b < Im d"
+ "box a b \<subseteq> cbox c d \<longleftrightarrow>
+ (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
+ "box a b \<subseteq> box c d \<longleftrightarrow>
+ (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
+ by (subst subset_box; force simp: Basis_complex_def)+
+
lemma Int_interval:
fixes a :: "'a::euclidean_space"
shows "cbox a b \<inter> cbox c d =
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Aug 20 03:35:20 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Aug 20 18:55:03 2017 +0200
@@ -439,22 +439,8 @@
lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X"
by (simp add: fps_eq_iff)
-lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then 1::'a::comm_ring_1 else 0)"
-proof (induct k)
- case 0
- then show ?case by (simp add: X_def fps_eq_iff)
-next
- case (Suc k)
- have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)" for m
- proof -
- have "(X^Suc k) $ m = (if m = 0 then 0 else (X^k) $ (m - 1))"
- by (simp del: One_nat_def)
- then show ?thesis
- using Suc.hyps by (auto cong del: if_weak_cong)
- qed
- then show ?case
- by (simp add: fps_eq_iff)
-qed
+lemma X_power_iff: "X ^ n = Abs_fps (\<lambda>m. if m = n then 1 else 0)"
+ by (induction n) (auto simp: fps_eq_iff)
lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)"
by (simp add: X_def)
@@ -4325,6 +4311,12 @@
definition "fps_cos (c::'a::field_char_0) =
Abs_fps (\<lambda>n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)"
+lemma fps_sin_0 [simp]: "fps_sin 0 = 0"
+ by (intro fps_ext) (auto simp: fps_sin_def elim!: oddE)
+
+lemma fps_cos_0 [simp]: "fps_cos 0 = 1"
+ by (intro fps_ext) (auto simp: fps_cos_def)
+
lemma fps_sin_deriv:
"fps_deriv (fps_sin c) = fps_const c * fps_cos c"
(is "?lhs = ?rhs")
@@ -4502,6 +4494,9 @@
definition "fps_tan c = fps_sin c / fps_cos c"
+lemma fps_tan_0 [simp]: "fps_tan 0 = 0"
+ by (simp add: fps_tan_def)
+
lemma fps_tan_deriv: "fps_deriv (fps_tan c) = fps_const c / (fps_cos c)\<^sup>2"
proof -
have th0: "fps_cos c $ 0 \<noteq> 0" by (simp add: fps_cos_def)