# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1503248103 -7200
# Node ID aec5d9c88d69231a325312299e5acf477bc161bc
# Parent  621897f47fab3f10b08ea95266eebd0cd50959f8
More lemmas for HOL-Analysis

diff -r 621897f47fab -r aec5d9c88d69 src/HOL/Analysis/Complex_Transcendental.thy
--- 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)
diff -r 621897f47fab -r aec5d9c88d69 src/HOL/Analysis/Generalised_Binomial_Theorem.thy
--- 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]]
diff -r 621897f47fab -r aec5d9c88d69 src/HOL/Analysis/Summation_Tests.thy
--- 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"
diff -r 621897f47fab -r aec5d9c88d69 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- 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 =
diff -r 621897f47fab -r aec5d9c88d69 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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)