src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 69180 922833cc6839
parent 69064 5840724b1d71
child 69286 e4d5a07fecb6
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Oct 22 12:22:18 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Oct 22 19:03:47 2018 +0200
     1.3 @@ -8,8 +8,9 @@
     1.4  imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Nonpos_Ints"
     1.5  begin
     1.6  
     1.7 +(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
     1.8  
     1.9 -subsection\<open>General lemmas\<close>
    1.10 +subsection%unimportant\<open>General lemmas\<close>
    1.11  
    1.12  lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
    1.13    by (simp add: complex_nonneg_Reals_iff cmod_eq_Re)
    1.14 @@ -82,8 +83,20 @@
    1.15  lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
    1.16    by (intro continuous_on_id continuous_on_norm)
    1.17  
    1.18 -subsection\<open>DERIV stuff\<close>
    1.19 +(*MOVE? But not to Finite_Cartesian_Product*)
    1.20 +lemma sums_vec_nth :
    1.21 +  assumes "f sums a"
    1.22 +  shows "(\<lambda>x. f x $ i) sums a $ i"
    1.23 +using assms unfolding sums_def
    1.24 +by (auto dest: tendsto_vec_nth [where i=i])
    1.25  
    1.26 +lemma summable_vec_nth :
    1.27 +  assumes "summable f"
    1.28 +  shows "summable (\<lambda>x. f x $ i)"
    1.29 +using assms unfolding summable_def
    1.30 +by (blast intro: sums_vec_nth)
    1.31 +
    1.32 +(* TODO: Move? *)
    1.33  lemma DERIV_zero_connected_constant:
    1.34    fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
    1.35    assumes "connected S"
    1.36 @@ -144,23 +157,6 @@
    1.37    "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
    1.38    by (metis DERIV_zero_unique UNIV_I convex_UNIV)
    1.39  
    1.40 -subsection \<open>Some limit theorems about real part of real series etc\<close>
    1.41 -
    1.42 -(*MOVE? But not to Finite_Cartesian_Product*)
    1.43 -lemma sums_vec_nth :
    1.44 -  assumes "f sums a"
    1.45 -  shows "(\<lambda>x. f x $ i) sums a $ i"
    1.46 -using assms unfolding sums_def
    1.47 -by (auto dest: tendsto_vec_nth [where i=i])
    1.48 -
    1.49 -lemma summable_vec_nth :
    1.50 -  assumes "summable f"
    1.51 -  shows "summable (\<lambda>x. f x $ i)"
    1.52 -using assms unfolding summable_def
    1.53 -by (blast intro: sums_vec_nth)
    1.54 -
    1.55 -subsection \<open>Complex number lemmas\<close>
    1.56 -
    1.57  lemma
    1.58    shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
    1.59      and open_halfspace_Re_gt: "open {z. Re(z) > b}"
    1.60 @@ -186,7 +182,7 @@
    1.61  lemma closed_Real_halfspace_Re_le: "closed (\<real> \<inter> {w. Re w \<le> x})"
    1.62    by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le)
    1.63  
    1.64 -corollary closed_nonpos_Reals_complex [simp]: "closed (\<real>\<^sub>\<le>\<^sub>0 :: complex set)"
    1.65 +lemma closed_nonpos_Reals_complex [simp]: "closed (\<real>\<^sub>\<le>\<^sub>0 :: complex set)"
    1.66  proof -
    1.67    have "\<real>\<^sub>\<le>\<^sub>0 = \<real> \<inter> {z. Re(z) \<le> 0}"
    1.68      using complex_nonpos_Reals_iff complex_is_Real_iff by auto
    1.69 @@ -198,7 +194,7 @@
    1.70    using closed_halfspace_Re_ge
    1.71    by (simp add: closed_Int closed_complex_Reals)
    1.72  
    1.73 -corollary closed_nonneg_Reals_complex [simp]: "closed (\<real>\<^sub>\<ge>\<^sub>0 :: complex set)"
    1.74 +lemma closed_nonneg_Reals_complex [simp]: "closed (\<real>\<^sub>\<ge>\<^sub>0 :: complex set)"
    1.75  proof -
    1.76    have "\<real>\<^sub>\<ge>\<^sub>0 = \<real> \<inter> {z. Re(z) \<ge> 0}"
    1.77      using complex_nonneg_Reals_iff complex_is_Real_iff by auto
    1.78 @@ -240,11 +236,11 @@
    1.79  
    1.80  subsection\<open>Holomorphic functions\<close>
    1.81  
    1.82 -definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
    1.83 +definition%important holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
    1.84             (infixl "(holomorphic'_on)" 50)
    1.85    where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f field_differentiable (at x within s)"
    1.86  
    1.87 -named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
    1.88 +named_theorems%important holomorphic_intros "structural introduction rules for holomorphic_on"
    1.89  
    1.90  lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f field_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
    1.91    by (simp add: holomorphic_on_def)
    1.92 @@ -502,7 +498,7 @@
    1.93    by (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
    1.94      (use assms in \<open>auto simp: holomorphic_derivI\<close>)
    1.95  
    1.96 -subsection\<open>Caratheodory characterization\<close>
    1.97 +subsection%unimportant\<open>Caratheodory characterization\<close>
    1.98  
    1.99  lemma field_differentiable_caratheodory_at:
   1.100    "f field_differentiable (at z) \<longleftrightarrow>
   1.101 @@ -518,10 +514,10 @@
   1.102  
   1.103  subsection\<open>Analyticity on a set\<close>
   1.104  
   1.105 -definition analytic_on (infixl "(analytic'_on)" 50)
   1.106 +definition%important analytic_on (infixl "(analytic'_on)" 50)
   1.107    where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
   1.108  
   1.109 -named_theorems analytic_intros "introduction rules for proving analyticity"
   1.110 +named_theorems%important analytic_intros "introduction rules for proving analyticity"
   1.111  
   1.112  lemma analytic_imp_holomorphic: "f analytic_on S \<Longrightarrow> f holomorphic_on S"
   1.113    by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
   1.114 @@ -738,7 +734,7 @@
   1.115    finally show ?thesis .
   1.116  qed
   1.117  
   1.118 -subsection\<open>analyticity at a point\<close>
   1.119 +subsection%unimportant\<open>Analyticity at a point\<close>
   1.120  
   1.121  lemma analytic_at_ball:
   1.122    "f analytic_on {z} \<longleftrightarrow> (\<exists>e. 0<e \<and> f holomorphic_on ball z e)"
   1.123 @@ -773,7 +769,7 @@
   1.124      by (force simp add: analytic_at)
   1.125  qed
   1.126  
   1.127 -subsection\<open>Combining theorems for derivative with ``analytic at'' hypotheses\<close>
   1.128 +subsection%unimportant\<open>Combining theorems for derivative with ``analytic at'' hypotheses\<close>
   1.129  
   1.130  lemma
   1.131    assumes "f analytic_on {z}" "g analytic_on {z}"
   1.132 @@ -809,7 +805,7 @@
   1.133    "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
   1.134  by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
   1.135  
   1.136 -subsection\<open>Complex differentiation of sequences and series\<close>
   1.137 +subsection%unimportant\<open>Complex differentiation of sequences and series\<close>
   1.138  
   1.139  (* TODO: Could probably be simplified using Uniform_Limit *)
   1.140  lemma has_complex_derivative_sequence:
   1.141 @@ -914,7 +910,7 @@
   1.142      by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
   1.143  qed
   1.144  
   1.145 -subsection\<open>Bound theorem\<close>
   1.146 +subsection%unimportant\<open>Bound theorem\<close>
   1.147  
   1.148  lemma field_differentiable_bound:
   1.149    fixes S :: "'a::real_normed_field set"
   1.150 @@ -928,7 +924,7 @@
   1.151    apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
   1.152    done
   1.153  
   1.154 -subsection\<open>Inverse function theorem for complex derivatives\<close>
   1.155 +subsection%unimportant\<open>Inverse function theorem for complex derivatives\<close>
   1.156  
   1.157  lemma has_field_derivative_inverse_basic:
   1.158    shows "DERIV f (g y) :> f' \<Longrightarrow>
   1.159 @@ -969,7 +965,7 @@
   1.160    apply (rule has_derivative_inverse_strong_x [of S g y f])
   1.161    by auto
   1.162  
   1.163 -subsection \<open>Taylor on Complex Numbers\<close>
   1.164 +subsection%unimportant \<open>Taylor on Complex Numbers\<close>
   1.165  
   1.166  lemma sum_Suc_reindex:
   1.167    fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
   1.168 @@ -1155,7 +1151,7 @@
   1.169  qed
   1.170  
   1.171  
   1.172 -subsection \<open>Polynomal function extremal theorem, from HOL Light\<close>
   1.173 +subsection%unimportant \<open>Polynomal function extremal theorem, from HOL Light\<close>
   1.174  
   1.175  lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
   1.176      fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"