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