author Manuel Eberl Mon Oct 22 19:03:47 2018 +0200 (7 months ago) changeset 69180 922833cc6839 parent 69179 dff89effe26b child 69181 effe7f8b2b1b
Tagged some theories in HOL-Analysis
     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.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"

     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Oct 22 12:22:18 2018 +0200
2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Oct 22 19:03:47 2018 +0200
2.3 @@ -9,10 +9,12 @@
2.4     "HOL-Library.Periodic_Fun"
2.5  begin
2.6
2.7 +subsection\<open>Möbius transformations\<close>
2.8 +
2.9  (* TODO: Figure out what to do with Möbius transformations *)
2.10 -definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
2.11 -
2.12 -lemma moebius_inverse:
2.13 +definition%important "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
2.14 +
2.15 +theorem moebius_inverse:
2.16    assumes "a * d \<noteq> b * c" "c * z + d \<noteq> 0"
2.17    shows   "moebius d (-b) (-c) a (moebius a b c d z) = z"
2.18  proof -
2.19 @@ -62,7 +64,7 @@
2.20      by (simp add: norm_power Im_power2)
2.21  qed
2.22
2.23 -subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
2.24 +subsection%unimportant\<open>The Exponential Function\<close>
2.25
2.26  lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
2.27    by simp
2.28 @@ -114,7 +116,7 @@
2.29      using sums_unique2 by blast
2.30  qed
2.31
2.32 -corollary exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
2.33 +corollary%unimportant exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
2.34    using exp_Euler [of "-z"]
2.35    by simp
2.36
2.37 @@ -127,7 +129,32 @@
2.38  lemma cos_exp_eq:  "cos z = (exp(\<i> * z) + exp(-(\<i> * z))) / 2"
2.39    by (simp add: exp_Euler exp_minus_Euler)
2.40
2.41 -subsection\<open>Relationships between real and complex trigonometric and hyperbolic functions\<close>
2.42 +theorem Euler: "exp(z) = of_real(exp(Re z)) *
2.43 +              (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
2.44 +by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)
2.45 +
2.46 +lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
2.47 +  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
2.48 +
2.49 +lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
2.50 +  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
2.51 +
2.52 +lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
2.53 +  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
2.54 +
2.55 +lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
2.56 +  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
2.57 +
2.58 +lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
2.59 +  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
2.60 +
2.61 +lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
2.62 +  by (simp add: Re_sin Im_sin algebra_simps)
2.63 +
2.64 +lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
2.65 +  by (simp add: Re_sin Im_sin algebra_simps)
2.66 +
2.67 +subsection%unimportant\<open>Relationships between real and complex trigonometric and hyperbolic functions\<close>
2.68
2.69  lemma real_sin_eq [simp]: "Re(sin(of_real x)) = sin x"
2.71 @@ -186,34 +213,7 @@
2.72    shows   "(\<lambda>x. cos (f x)) holomorphic_on A"
2.73    using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)
2.74
2.75 -subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
2.76 -
2.77 -lemma Euler: "exp(z) = of_real(exp(Re z)) *
2.78 -              (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
2.79 -by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)
2.80 -
2.81 -lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
2.82 -  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
2.83 -
2.84 -lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
2.85 -  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
2.86 -
2.87 -lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
2.88 -  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
2.89 -
2.90 -lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
2.91 -  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
2.92 -
2.93 -lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
2.94 -  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
2.95 -
2.96 -lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
2.97 -  by (simp add: Re_sin Im_sin algebra_simps)
2.98 -
2.99 -lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
2.100 -  by (simp add: Re_sin Im_sin algebra_simps)
2.101 -
2.102 -subsection\<open>More on the Polar Representation of Complex Numbers\<close>
2.103 +subsection%unimportant\<open>More on the Polar Representation of Complex Numbers\<close>
2.104
2.105  lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
2.107 @@ -693,7 +693,7 @@
2.108  qed
2.109
2.110
2.111 -subsection\<open>Taylor series for complex exponential, sine and cosine\<close>
2.112 +subsection%unimportant\<open>Taylor series for complex exponential, sine and cosine\<close>
2.113
2.114  declare power_Suc [simp del]
2.115
2.116 @@ -859,10 +859,10 @@
2.117
2.118  subsection\<open>The argument of a complex number (HOL Light version)\<close>
2.119
2.120 -definition is_Arg :: "[complex,real] \<Rightarrow> bool"
2.121 +definition%important is_Arg :: "[complex,real] \<Rightarrow> bool"
2.122    where "is_Arg z r \<equiv> z = of_real(norm z) * exp(\<i> * of_real r)"
2.123
2.124 -definition Arg2pi :: "complex \<Rightarrow> real"
2.125 +definition%important Arg2pi :: "complex \<Rightarrow> real"
2.126    where "Arg2pi z \<equiv> if z = 0 then 0 else THE t. 0 \<le> t \<and> t < 2*pi \<and> is_Arg z t"
2.127
2.128  lemma is_Arg_2pi_iff: "is_Arg z (r + of_int k * (2 * pi)) \<longleftrightarrow> is_Arg z r"
2.129 @@ -940,7 +940,7 @@
2.130      done
2.131  qed
2.132
2.133 -corollary
2.134 +corollary%unimportant
2.135    shows Arg2pi_ge_0: "0 \<le> Arg2pi z"
2.136      and Arg2pi_lt_2pi: "Arg2pi z < 2*pi"
2.137      and Arg2pi_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
2.138 @@ -1023,7 +1023,7 @@
2.139      by blast
2.140  qed auto
2.141
2.142 -corollary Arg2pi_gt_0:
2.143 +corollary%unimportant Arg2pi_gt_0:
2.144    assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
2.145      shows "Arg2pi z > 0"
2.146    using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order
2.147 @@ -1128,7 +1128,7 @@
2.148      by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
2.149  qed
2.150
2.151 -subsection\<open>Analytic properties of tangent function\<close>
2.152 +subsection%unimportant\<open>Analytic properties of tangent function\<close>
2.153
2.154  lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
2.155    by (simp add: cnj_cos cnj_sin tan_def)
2.156 @@ -1151,12 +1151,12 @@
2.157    by (simp add: field_differentiable_within_tan holomorphic_on_def)
2.158
2.159
2.160 -subsection\<open>Complex logarithms (the conventional principal value)\<close>
2.161 +subsection\<open>The principal branch of the Complex logarithm\<close>
2.162
2.163  instantiation complex :: ln
2.164  begin
2.165
2.166 -definition ln_complex :: "complex \<Rightarrow> complex"
2.167 +definition%important ln_complex :: "complex \<Rightarrow> complex"
2.168    where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
2.169
2.170  text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close>
2.171 @@ -1189,7 +1189,7 @@
2.172    apply auto
2.173    done
2.174
2.175 -subsection\<open>Relation to Real Logarithm\<close>
2.176 +subsection%unimportant\<open>Relation to Real Logarithm\<close>
2.177
2.178  lemma Ln_of_real:
2.179    assumes "0 < z"
2.180 @@ -1203,10 +1203,10 @@
2.181      using assms by simp
2.182  qed
2.183
2.184 -corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
2.185 +corollary%unimportant Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
2.186    by (auto simp: Ln_of_real elim: Reals_cases)
2.187
2.188 -corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
2.189 +corollary%unimportant Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
2.191
2.192  lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
2.193 @@ -1244,13 +1244,13 @@
2.194  lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
2.195    by (metis exp_Ln ln_exp norm_exp_eq_Re)
2.196
2.197 -corollary ln_cmod_le:
2.198 +corollary%unimportant ln_cmod_le:
2.199    assumes z: "z \<noteq> 0"
2.200      shows "ln (cmod z) \<le> cmod (Ln z)"
2.201    using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
2.202    by (metis Re_Ln complex_Re_le_cmod z)
2.203
2.204 -proposition exists_complex_root:
2.205 +proposition%unimportant exists_complex_root:
2.206    fixes z :: complex
2.207    assumes "n \<noteq> 0"  obtains w where "z = w ^ n"
2.208  proof (cases "z=0")
2.209 @@ -1259,13 +1259,13 @@
2.210      by (rule_tac w = "exp(Ln z / n)" in that) (simp add: assms exp_of_nat_mult [symmetric])
2.211  qed (use assms in auto)
2.212
2.213 -corollary exists_complex_root_nonzero:
2.214 +corollary%unimportant exists_complex_root_nonzero:
2.215    fixes z::complex
2.216    assumes "z \<noteq> 0" "n \<noteq> 0"
2.217    obtains w where "w \<noteq> 0" "z = w ^ n"
2.218    by (metis exists_complex_root [of n z] assms power_0_left)
2.219
2.220 -subsection\<open>Derivative of Ln away from the branch cut\<close>
2.221 +subsection%unimportant\<open>Derivative of Ln away from the branch cut\<close>
2.222
2.223  lemma
2.224    assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
2.225 @@ -1357,8 +1357,106 @@
2.226    qed
2.227  qed
2.228
2.229 -
2.231 +theorem Ln_series:
2.232 +  fixes z :: complex
2.233 +  assumes "norm z < 1"
2.234 +  shows   "(\<lambda>n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\<lambda>n. ?f n * z^n) sums _")
2.235 +proof -
2.236 +  let ?F = "\<lambda>z. \<Sum>n. ?f n * z^n" and ?F' = "\<lambda>z. \<Sum>n. diffs ?f n * z^n"
2.237 +  have r: "conv_radius ?f = 1"
2.238 +    by (intro conv_radius_ratio_limit_nonzero[of _ 1])
2.239 +       (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)
2.240 +
2.241 +  have "\<exists>c. \<forall>z\<in>ball 0 1. ln (1 + z) - ?F z = c"
2.242 +  proof (rule has_field_derivative_zero_constant)
2.243 +    fix z :: complex assume z': "z \<in> ball 0 1"
2.244 +    hence z: "norm z < 1" by simp
2.245 +    define t :: complex where "t = of_real (1 + norm z) / 2"
2.246 +    from z have t: "norm z < norm t" "norm t < 1" unfolding t_def
2.248 +
2.249 +    have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
2.250 +    also from z have "... < 1" by simp
2.251 +    finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
2.252 +      by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
2.253 +    moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
2.254 +      by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
2.255 +    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
2.256 +                       (at z within ball 0 1)"
2.257 +      by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
2.258 +    also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
2.259 +      by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all
2.260 +    from sums_split_initial_segment[OF this, of 1]
2.261 +      have "(\<lambda>i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)
2.262 +    hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)
2.263 +    also have "inverse (1 + z) - inverse (1 + z) = 0" by simp
2.264 +    finally show "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .
2.265 +  qed simp_all
2.266 +  then obtain c where c: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> ln (1 + z) - ?F z = c" by blast
2.267 +  from c[of 0] have "c = 0" by (simp only: powser_zero) simp
2.268 +  with c[of z] assms have "ln (1 + z) = ?F z" by simp
2.269 +  moreover have "summable (\<lambda>n. ?f n * z^n)" using assms r
2.270 +    by (intro summable_in_conv_radius) simp_all
2.271 +  ultimately show ?thesis by (simp add: sums_iff)
2.272 +qed
2.273 +
2.274 +lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
2.275 +  by (drule Ln_series) (simp add: power_minus')
2.276 +
2.277 +lemma ln_series':
2.278 +  assumes "abs (x::real) < 1"
2.279 +  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
2.280 +proof -
2.281 +  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
2.282 +    by (intro Ln_series') simp_all
2.283 +  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
2.284 +    by (rule ext) simp
2.285 +  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
2.286 +    by (subst Ln_of_real [symmetric]) simp_all
2.287 +  finally show ?thesis by (subst (asm) sums_of_real_iff)
2.288 +qed
2.289 +
2.290 +lemma Ln_approx_linear:
2.291 +  fixes z :: complex
2.292 +  assumes "norm z < 1"
2.293 +  shows   "norm (ln (1 + z) - z) \<le> norm z^2 / (1 - norm z)"
2.294 +proof -
2.295 +  let ?f = "\<lambda>n. (-1)^Suc n / of_nat n"
2.296 +  from assms have "(\<lambda>n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp
2.297 +  moreover have "(\<lambda>n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp
2.298 +  ultimately have "(\<lambda>n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"
2.299 +    by (subst left_diff_distrib, intro sums_diff) simp_all
2.300 +  from sums_split_initial_segment[OF this, of "Suc 1"]
2.301 +    have "(\<lambda>i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"
2.302 +    by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)
2.303 +  hence "(Ln (1 + z) - z) = (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"
2.304 +    by (simp add: sums_iff)
2.305 +  also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
2.306 +    by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
2.307 +       (auto simp: assms field_simps intro!: always_eventually)
2.308 +  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
2.309 +             (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
2.310 +    by (intro summable_norm)
2.311 +       (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
2.312 +  also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
2.313 +    by (intro mult_left_mono) (simp_all add: divide_simps)
2.314 +  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))
2.315 +         \<le> (\<Sum>i. norm (-(z^2) * (-z)^i))"
2.316 +    using A assms
2.317 +    apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
2.318 +    apply (intro suminf_le summable_mult summable_geometric)
2.319 +    apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
2.320 +    done
2.321 +  also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms
2.322 +    by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
2.323 +  also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms
2.324 +    by (subst suminf_geometric) (simp_all add: divide_inverse)
2.325 +  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
2.326 +  finally show ?thesis .
2.327 +qed
2.328 +
2.329 +
2.331
2.332  lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
2.333    using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
2.334 @@ -1455,7 +1553,7 @@
2.335      mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
2.336
2.337
2.338 -subsection\<open>More Properties of Ln\<close>
2.339 +subsection%unimportant\<open>More Properties of Ln\<close>
2.340
2.341  lemma cnj_Ln: assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" shows "cnj(Ln z) = Ln(cnj z)"
2.342  proof (cases "z=0")
2.343 @@ -1533,27 +1631,27 @@
2.344    using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
2.345    by (auto simp: exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
2.346
2.347 -corollary Ln_times_simple:
2.348 +corollary%unimportant Ln_times_simple:
2.349      "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
2.350           \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
2.352
2.353 -corollary Ln_times_of_real:
2.354 +corollary%unimportant Ln_times_of_real:
2.355      "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_real r * z) = ln r + Ln(z)"
2.356    using mpi_less_Im_Ln Im_Ln_le_pi
2.357    by (force simp: Ln_times)
2.358
2.359 -corollary Ln_times_Reals:
2.360 +corollary%unimportant Ln_times_Reals:
2.361      "\<lbrakk>r \<in> Reals; Re r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(r * z) = ln (Re r) + Ln(z)"
2.362    using Ln_Reals_eq Ln_times_of_real by fastforce
2.363
2.364 -corollary Ln_divide_of_real:
2.365 +corollary%unimportant Ln_divide_of_real:
2.366      "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
2.367  using Ln_times_of_real [of "inverse r" z]
2.368  by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric]
2.369           del: of_real_inverse)
2.370
2.371 -corollary Ln_prod:
2.372 +corollary%unimportant Ln_prod:
2.373    fixes f :: "'a \<Rightarrow> complex"
2.374    assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
2.375    shows "\<exists>n. Ln (prod f A) = (\<Sum>x \<in> A. Ln (f x) + (of_int (n x) * (2 * pi)) * \<i>)"
2.376 @@ -1655,7 +1753,7 @@
2.377
2.378  text\<open>Finally: it's is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
2.379
2.380 -definition Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
2.381 +definition%important Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
2.382
2.383  lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
2.384    by (simp add: Im_Ln_eq_pi Arg_def)
2.385 @@ -1793,7 +1891,7 @@
2.386    using complex_is_Real_iff
2.387    by (simp add: Arg_def Im_Ln_eq_0) (metis less_eq_real_def of_real_Re of_real_def scale_zero_left)
2.388
2.389 -corollary Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
2.390 +corollary%unimportant Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
2.391    using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
2.392
2.393  lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
2.394 @@ -1869,7 +1967,7 @@
2.395    using continuous_at_Arg continuous_at_imp_continuous_within by blast
2.396
2.397
2.398 -subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
2.399 +subsection\<open>The Unwinding Number and the Ln product Formula\<close>
2.400
2.401  text\<open>Note that in this special case the unwinding number is -1, 0 or 1. But it's always an integer.\<close>
2.402
2.403 @@ -1895,7 +1993,7 @@
2.404    using Arg_exp_diff_2pi [of z]
2.405    by (force simp: Ints_def image_def field_simps Arg_def intro!: complex_eqI)
2.406
2.407 -definition unwinding :: "complex \<Rightarrow> int" where
2.408 +definition%important unwinding :: "complex \<Rightarrow> int" where
2.409     "unwinding z \<equiv> THE k. of_int k = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
2.410
2.411  lemma unwinding: "of_int (unwinding z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
2.412 @@ -1910,7 +2008,7 @@
2.414
2.415
2.416 -subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
2.417 +subsection%unimportant\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
2.418
2.419  lemma Arg2pi_Ln:
2.420    assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi"
2.421 @@ -1960,104 +2058,6 @@
2.422    qed (use assms in auto)
2.423  qed
2.424
2.425 -lemma Ln_series:
2.426 -  fixes z :: complex
2.427 -  assumes "norm z < 1"
2.428 -  shows   "(\<lambda>n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\<lambda>n. ?f n * z^n) sums _")
2.429 -proof -
2.430 -  let ?F = "\<lambda>z. \<Sum>n. ?f n * z^n" and ?F' = "\<lambda>z. \<Sum>n. diffs ?f n * z^n"
2.431 -  have r: "conv_radius ?f = 1"
2.432 -    by (intro conv_radius_ratio_limit_nonzero[of _ 1])
2.433 -       (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)
2.434 -
2.435 -  have "\<exists>c. \<forall>z\<in>ball 0 1. ln (1 + z) - ?F z = c"
2.436 -  proof (rule has_field_derivative_zero_constant)
2.437 -    fix z :: complex assume z': "z \<in> ball 0 1"
2.438 -    hence z: "norm z < 1" by simp
2.439 -    define t :: complex where "t = of_real (1 + norm z) / 2"
2.440 -    from z have t: "norm z < norm t" "norm t < 1" unfolding t_def
2.442 -
2.443 -    have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
2.444 -    also from z have "... < 1" by simp
2.445 -    finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
2.446 -      by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
2.447 -    moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
2.448 -      by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
2.449 -    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
2.450 -                       (at z within ball 0 1)"
2.451 -      by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
2.452 -    also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
2.453 -      by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all
2.454 -    from sums_split_initial_segment[OF this, of 1]
2.455 -      have "(\<lambda>i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)
2.456 -    hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)
2.457 -    also have "inverse (1 + z) - inverse (1 + z) = 0" by simp
2.458 -    finally show "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .
2.459 -  qed simp_all
2.460 -  then obtain c where c: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> ln (1 + z) - ?F z = c" by blast
2.461 -  from c[of 0] have "c = 0" by (simp only: powser_zero) simp
2.462 -  with c[of z] assms have "ln (1 + z) = ?F z" by simp
2.463 -  moreover have "summable (\<lambda>n. ?f n * z^n)" using assms r
2.464 -    by (intro summable_in_conv_radius) simp_all
2.465 -  ultimately show ?thesis by (simp add: sums_iff)
2.466 -qed
2.467 -
2.468 -lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
2.469 -  by (drule Ln_series) (simp add: power_minus')
2.470 -
2.471 -lemma ln_series':
2.472 -  assumes "abs (x::real) < 1"
2.473 -  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
2.474 -proof -
2.475 -  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
2.476 -    by (intro Ln_series') simp_all
2.477 -  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
2.478 -    by (rule ext) simp
2.479 -  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
2.480 -    by (subst Ln_of_real [symmetric]) simp_all
2.481 -  finally show ?thesis by (subst (asm) sums_of_real_iff)
2.482 -qed
2.483 -
2.484 -lemma Ln_approx_linear:
2.485 -  fixes z :: complex
2.486 -  assumes "norm z < 1"
2.487 -  shows   "norm (ln (1 + z) - z) \<le> norm z^2 / (1 - norm z)"
2.488 -proof -
2.489 -  let ?f = "\<lambda>n. (-1)^Suc n / of_nat n"
2.490 -  from assms have "(\<lambda>n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp
2.491 -  moreover have "(\<lambda>n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp
2.492 -  ultimately have "(\<lambda>n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"
2.493 -    by (subst left_diff_distrib, intro sums_diff) simp_all
2.494 -  from sums_split_initial_segment[OF this, of "Suc 1"]
2.495 -    have "(\<lambda>i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"
2.496 -    by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)
2.497 -  hence "(Ln (1 + z) - z) = (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"
2.498 -    by (simp add: sums_iff)
2.499 -  also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
2.500 -    by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
2.501 -       (auto simp: assms field_simps intro!: always_eventually)
2.502 -  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
2.503 -             (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
2.504 -    by (intro summable_norm)
2.505 -       (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
2.506 -  also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
2.507 -    by (intro mult_left_mono) (simp_all add: divide_simps)
2.508 -  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))
2.509 -         \<le> (\<Sum>i. norm (-(z^2) * (-z)^i))"
2.510 -    using A assms
2.511 -    apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
2.512 -    apply (intro suminf_le summable_mult summable_geometric)
2.513 -    apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
2.514 -    done
2.515 -  also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms
2.516 -    by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
2.517 -  also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms
2.518 -    by (subst suminf_geometric) (simp_all add: divide_inverse)
2.519 -  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
2.520 -  finally show ?thesis .
2.521 -qed
2.522 -
2.523
2.524  text\<open>Relation between Arg2pi and arctangent in upper halfplane\<close>
2.525  lemma Arg2pi_arctan_upperhalf:
2.526 @@ -2166,7 +2166,7 @@
2.527    using open_Arg2pi2pi_gt [of t]
2.528    by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
2.529
2.530 -subsection\<open>Complex Powers\<close>
2.531 +subsection%unimportant\<open>Complex Powers\<close>
2.532
2.533  lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
2.535 @@ -2535,7 +2535,7 @@
2.536  qed
2.537
2.538
2.539 -subsection\<open>Some Limits involving Logarithms\<close>
2.540 +subsection%unimportant\<open>Some Limits involving Logarithms\<close>
2.541
2.542  lemma lim_Ln_over_power:
2.543    fixes s::complex
2.544 @@ -2686,7 +2686,7 @@
2.545  qed
2.546
2.547
2.548 -subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
2.549 +subsection%unimportant\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
2.550
2.551  lemma csqrt_exp_Ln:
2.552    assumes "z \<noteq> 0"
2.553 @@ -2759,7 +2759,7 @@
2.554      "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) csqrt"
2.555    by (simp add: field_differentiable_within_csqrt field_differentiable_imp_continuous_at)
2.556
2.557 -corollary isCont_csqrt' [simp]:
2.558 +corollary%unimportant isCont_csqrt' [simp]:
2.559     "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
2.560    by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
2.561
2.562 @@ -2802,7 +2802,7 @@
2.563
2.564  text\<open>The branch cut gives standard bounds in the real case.\<close>
2.565
2.566 -definition Arctan :: "complex \<Rightarrow> complex" where
2.567 +definition%important Arctan :: "complex \<Rightarrow> complex" where
2.568      "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
2.569
2.570  lemma Arctan_def_moebius: "Arctan z = \<i>/2 * Ln (moebius (-\<i>) 1 \<i> 1 z)"
2.571 @@ -2948,7 +2948,7 @@
2.572      "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
2.573    by (simp add: field_differentiable_within_Arctan holomorphic_on_def)
2.574
2.575 -lemma Arctan_series:
2.576 +theorem Arctan_series:
2.577    assumes z: "norm (z :: complex) < 1"
2.578    defines "g \<equiv> \<lambda>n. if odd n then -\<i>*\<i>^n / n else 0"
2.579    defines "h \<equiv> \<lambda>z n. (-1)^n / of_nat (2*n+1) * (z::complex)^(2*n+1)"
2.580 @@ -3022,7 +3022,7 @@
2.581  qed
2.582
2.583  text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>
2.586    assumes x: "x > (0::real)"
2.587    shows "(\<lambda>n. (2*((x - 1) / (x + 1)) ^ (2*n+1) / of_nat (2*n+1))) sums ln x"
2.588  proof -
2.589 @@ -3051,7 +3051,7 @@
2.590    finally show ?thesis by (subst (asm) sums_of_real_iff)
2.591  qed
2.592
2.593 -subsection \<open>Real arctangent\<close>
2.594 +subsection%unimportant \<open>Real arctangent\<close>
2.595
2.596  lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
2.597  proof -
2.598 @@ -3212,7 +3212,7 @@
2.599      by (auto simp: arctan_series)
2.600  qed
2.601
2.602 -subsection \<open>Bounds on pi using real arctangent\<close>
2.603 +subsection%unimportant \<open>Bounds on pi using real arctangent\<close>
2.604
2.605  lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
2.606    using machin by simp
2.607 @@ -3223,13 +3223,13 @@
2.608          arctan_bounds[of "1/239" 4]
2.610
2.611 -corollary pi_gt3: "pi > 3"
2.612 +lemma pi_gt3: "pi > 3"
2.613    using pi_approx by simp
2.614
2.615
2.616  subsection\<open>Inverse Sine\<close>
2.617
2.618 -definition Arcsin :: "complex \<Rightarrow> complex" where
2.619 +definition%important Arcsin :: "complex \<Rightarrow> complex" where
2.620     "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
2.621
2.622  lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 0"
2.623 @@ -3396,7 +3396,7 @@
2.624
2.625  subsection\<open>Inverse Cosine\<close>
2.626
2.627 -definition Arccos :: "complex \<Rightarrow> complex" where
2.628 +definition%important Arccos :: "complex \<Rightarrow> complex" where
2.629     "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
2.630
2.631  lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
2.632 @@ -3555,7 +3555,7 @@
2.633    by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
2.634
2.635
2.636 -subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
2.637 +subsection%unimportant\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
2.638
2.639  lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> \<bar>Re(Arcsin z)\<bar> < pi/2"
2.640    unfolding Re_Arcsin
2.641 @@ -3608,7 +3608,7 @@
2.642  qed
2.643
2.644
2.645 -subsection\<open>Interrelations between Arcsin and Arccos\<close>
2.646 +subsection%unimportant\<open>Interrelations between Arcsin and Arccos\<close>
2.647
2.648  lemma cos_Arcsin_nonzero:
2.649    assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
2.650 @@ -3710,7 +3710,7 @@
2.652
2.653
2.654 -subsection\<open>Relationship with Arcsin on the Real Numbers\<close>
2.655 +subsection%unimportant\<open>Relationship with Arcsin on the Real Numbers\<close>
2.656
2.657  lemma Im_Arcsin_of_real:
2.658    assumes "\<bar>x\<bar> \<le> 1"
2.659 @@ -3727,7 +3727,7 @@
2.660      by (simp add: Im_Arcsin exp_minus)
2.661  qed
2.662
2.663 -corollary Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
2.664 +corollary%unimportant Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
2.665    by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
2.666
2.667  lemma arcsin_eq_Re_Arcsin:
2.668 @@ -3760,7 +3760,7 @@
2.669    by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
2.670
2.671
2.672 -subsection\<open>Relationship with Arccos on the Real Numbers\<close>
2.673 +subsection%unimportant\<open>Relationship with Arccos on the Real Numbers\<close>
2.674
2.675  lemma Im_Arccos_of_real:
2.676    assumes "\<bar>x\<bar> \<le> 1"
2.677 @@ -3777,7 +3777,7 @@
2.678      by (simp add: Im_Arccos exp_minus)
2.679  qed
2.680
2.681 -corollary Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
2.682 +corollary%unimportant Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
2.683    by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
2.684
2.685  lemma arccos_eq_Re_Arccos:
2.686 @@ -3809,7 +3809,7 @@
2.687  lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
2.688    by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
2.689
2.690 -subsection\<open>Some interrelationships among the real inverse trig functions\<close>
2.691 +subsection%unimportant\<open>Some interrelationships among the real inverse trig functions\<close>
2.692
2.693  lemma arccos_arctan:
2.694    assumes "-1 < x" "x < 1"
2.695 @@ -3879,7 +3879,7 @@
2.696    using arccos_arcsin_sqrt_pos [of "-x"]
2.698
2.699 -subsection\<open>Continuity results for arcsin and arccos\<close>
2.700 +subsection%unimportant\<open>Continuity results for arcsin and arccos\<close>
2.701
2.702  lemma continuous_on_Arcsin_real [continuous_intros]:
2.703      "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
2.704 @@ -3945,7 +3945,7 @@
2.705
2.706  subsection\<open>Roots of unity\<close>
2.707
2.708 -lemma complex_root_unity:
2.709 +theorem complex_root_unity:
2.710    fixes j::nat
2.711    assumes "n \<noteq> 0"
2.712      shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
2.713 @@ -4033,7 +4033,7 @@
2.714    apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
2.715    done
2.716
2.717 -subsection\<open> Formulation of loop homotopy in terms of maps out of type complex\<close>
2.718 +subsection\<open>Formulation of loop homotopy in terms of maps out of type complex\<close>
2.719
2.720  lemma homotopic_circlemaps_imp_homotopic_loops:
2.721    assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"

     3.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Mon Oct 22 12:22:18 2018 +0200
3.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Mon Oct 22 19:03:47 2018 +0200
3.3 @@ -6,13 +6,23 @@
3.4      measure on the left part of the sum type 'a + 'b)
3.5  *)
3.6
3.7 -section \<open>Embed Measure Spaces with a Function\<close>
3.8 +section \<open>Embedding Measure Spaces with a Function\<close>
3.9
3.10  theory Embed_Measure
3.11  imports Binary_Product_Measure
3.12  begin
3.13
3.14 -definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
3.15 +text \<open>
3.16 +  Given a measure space on some carrier set \<open>\<Omega>\<close> and a function \<open>f\<close>, we can define a push-forward
3.17 +  measure on the carrier set $f(\Omega)$ whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
3.18 +  the original sigma algebra.
3.19 +
3.20 +  This is useful e.\,g.\ when \<open>f\<close> is injective, i.\,e.\ it is some kind of tagging'' function.
3.21 +  For instance, suppose we have some algebraaic datatype of values with various constructors,
3.22 +  including a constructor \<open>RealVal\<close> for real numbers. Then \<open>embed_measure\<close> allows us to lift a
3.23 +  measure on real numbers to the appropriate subset of that algebraic datatype.
3.24 +\<close>
3.25 +definition%important embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
3.26    "embed_measure M f = measure_of (f  space M) {f  A |A. A \<in> sets M}
3.27                             (\<lambda>A. emeasure M (f - A \<inter> space M))"
3.28

     4.1 --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Mon Oct 22 12:22:18 2018 +0200
4.2 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Mon Oct 22 19:03:47 2018 +0200
4.3 @@ -6,7 +6,7 @@
4.4      This could probably be weakened somehow.
4.5  *)
4.6
4.7 -section \<open>Integration by Substition\<close>
4.8 +section \<open>Integration by Substition for the Lebesgue integral\<close>
4.9
4.10  theory Lebesgue_Integral_Substitution
4.11  imports Interval_Integral
4.12 @@ -278,7 +278,7 @@
4.13    qed
4.14  qed
4.15
4.16 -lemma nn_integral_substitution:
4.17 +theorem nn_integral_substitution:
4.18    fixes f :: "real \<Rightarrow> real"
4.19    assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
4.20    assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
4.21 @@ -317,7 +317,7 @@
4.22    finally show ?thesis .
4.23  qed auto
4.24
4.25 -lemma integral_substitution:
4.26 +theorem integral_substitution:
4.27    assumes integrable: "set_integrable lborel {g a..g b} f"
4.28    assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
4.29    assumes contg': "continuous_on {a..b} g'"
4.30 @@ -384,7 +384,7 @@
4.31                       (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
4.32  qed
4.33
4.34 -lemma interval_integral_substitution:
4.35 +theorem interval_integral_substitution:
4.36    assumes integrable: "set_integrable lborel {g a..g b} f"
4.37    assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
4.38    assumes contg': "continuous_on {a..b} g'"
`