Tagged some theories in HOL-Analysis
authorManuel Eberl <eberlm@in.tum.de>
Mon Oct 22 19:03:47 2018 +0200 (7 months ago)
changeset 69180922833cc6839
parent 69179 dff89effe26b
child 69181 effe7f8b2b1b
Tagged some theories in HOL-Analysis
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Embed_Measure.thy
src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
     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"
     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.70    by (simp add: sin_of_real)
    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.106    by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
   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.190    by (simp add: Ln_of_real)
   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.230 -subsection\<open>Quadrant-type results for Ln\<close>
   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.247 +      by (simp_all add: field_simps norm_divide del: of_real_add)
   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.330 +subsection%unimportant\<open>Quadrant-type results for Ln\<close>
   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.351    by (simp add: Ln_times)
   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.413    using unwinding_2pi by (simp add: exp_add)
   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.441 -      by (simp_all add: field_simps norm_divide del: of_real_add)
   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.534    by (simp add: powr_def)
   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.584 -lemma ln_series_quadratic:
   2.585 +theorem ln_series_quadratic:
   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.609    by (simp_all add: eval_nat_numeral)
   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.651    by (simp add: Arcsin_Arccos_csqrt_pos)
   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.697    by (simp add: arccos_minus)
   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'"