# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1540227827 -7200
# Node ID 922833cc6839e4f37251805ddb57c121ddde0347
# Parent  dff89effe26b516b149b7926fa6719b2e2aaaf9e
Tagged some theories in HOL-Analysis

diff -r dff89effe26b -r 922833cc6839 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Oct 22 12:22:18 2018 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Oct 22 19:03:47 2018 +0200
@@ -8,8 +8,9 @@
 imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Nonpos_Ints"
 begin
 
+(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
 
-subsection\<open>General lemmas\<close>
+subsection%unimportant\<open>General lemmas\<close>
 
 lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
   by (simp add: complex_nonneg_Reals_iff cmod_eq_Re)
@@ -82,8 +83,20 @@
 lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
   by (intro continuous_on_id continuous_on_norm)
 
-subsection\<open>DERIV stuff\<close>
+(*MOVE? But not to Finite_Cartesian_Product*)
+lemma sums_vec_nth :
+  assumes "f sums a"
+  shows "(\<lambda>x. f x $ i) sums a $ i"
+using assms unfolding sums_def
+by (auto dest: tendsto_vec_nth [where i=i])
 
+lemma summable_vec_nth :
+  assumes "summable f"
+  shows "summable (\<lambda>x. f x $ i)"
+using assms unfolding summable_def
+by (blast intro: sums_vec_nth)
+
+(* TODO: Move? *)
 lemma DERIV_zero_connected_constant:
   fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
   assumes "connected S"
@@ -144,23 +157,6 @@
   "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
   by (metis DERIV_zero_unique UNIV_I convex_UNIV)
 
-subsection \<open>Some limit theorems about real part of real series etc\<close>
-
-(*MOVE? But not to Finite_Cartesian_Product*)
-lemma sums_vec_nth :
-  assumes "f sums a"
-  shows "(\<lambda>x. f x $ i) sums a $ i"
-using assms unfolding sums_def
-by (auto dest: tendsto_vec_nth [where i=i])
-
-lemma summable_vec_nth :
-  assumes "summable f"
-  shows "summable (\<lambda>x. f x $ i)"
-using assms unfolding summable_def
-by (blast intro: sums_vec_nth)
-
-subsection \<open>Complex number lemmas\<close>
-
 lemma
   shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
     and open_halfspace_Re_gt: "open {z. Re(z) > b}"
@@ -186,7 +182,7 @@
 lemma closed_Real_halfspace_Re_le: "closed (\<real> \<inter> {w. Re w \<le> x})"
   by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le)
 
-corollary closed_nonpos_Reals_complex [simp]: "closed (\<real>\<^sub>\<le>\<^sub>0 :: complex set)"
+lemma closed_nonpos_Reals_complex [simp]: "closed (\<real>\<^sub>\<le>\<^sub>0 :: complex set)"
 proof -
   have "\<real>\<^sub>\<le>\<^sub>0 = \<real> \<inter> {z. Re(z) \<le> 0}"
     using complex_nonpos_Reals_iff complex_is_Real_iff by auto
@@ -198,7 +194,7 @@
   using closed_halfspace_Re_ge
   by (simp add: closed_Int closed_complex_Reals)
 
-corollary closed_nonneg_Reals_complex [simp]: "closed (\<real>\<^sub>\<ge>\<^sub>0 :: complex set)"
+lemma closed_nonneg_Reals_complex [simp]: "closed (\<real>\<^sub>\<ge>\<^sub>0 :: complex set)"
 proof -
   have "\<real>\<^sub>\<ge>\<^sub>0 = \<real> \<inter> {z. Re(z) \<ge> 0}"
     using complex_nonneg_Reals_iff complex_is_Real_iff by auto
@@ -240,11 +236,11 @@
 
 subsection\<open>Holomorphic functions\<close>
 
-definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
+definition%important holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
            (infixl "(holomorphic'_on)" 50)
   where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f field_differentiable (at x within s)"
 
-named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
+named_theorems%important holomorphic_intros "structural introduction rules for holomorphic_on"
 
 lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f field_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
   by (simp add: holomorphic_on_def)
@@ -502,7 +498,7 @@
   by (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
     (use assms in \<open>auto simp: holomorphic_derivI\<close>)
 
-subsection\<open>Caratheodory characterization\<close>
+subsection%unimportant\<open>Caratheodory characterization\<close>
 
 lemma field_differentiable_caratheodory_at:
   "f field_differentiable (at z) \<longleftrightarrow>
@@ -518,10 +514,10 @@
 
 subsection\<open>Analyticity on a set\<close>
 
-definition analytic_on (infixl "(analytic'_on)" 50)
+definition%important analytic_on (infixl "(analytic'_on)" 50)
   where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
 
-named_theorems analytic_intros "introduction rules for proving analyticity"
+named_theorems%important analytic_intros "introduction rules for proving analyticity"
 
 lemma analytic_imp_holomorphic: "f analytic_on S \<Longrightarrow> f holomorphic_on S"
   by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
@@ -738,7 +734,7 @@
   finally show ?thesis .
 qed
 
-subsection\<open>analyticity at a point\<close>
+subsection%unimportant\<open>Analyticity at a point\<close>
 
 lemma analytic_at_ball:
   "f analytic_on {z} \<longleftrightarrow> (\<exists>e. 0<e \<and> f holomorphic_on ball z e)"
@@ -773,7 +769,7 @@
     by (force simp add: analytic_at)
 qed
 
-subsection\<open>Combining theorems for derivative with ``analytic at'' hypotheses\<close>
+subsection%unimportant\<open>Combining theorems for derivative with ``analytic at'' hypotheses\<close>
 
 lemma
   assumes "f analytic_on {z}" "g analytic_on {z}"
@@ -809,7 +805,7 @@
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
 by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
 
-subsection\<open>Complex differentiation of sequences and series\<close>
+subsection%unimportant\<open>Complex differentiation of sequences and series\<close>
 
 (* TODO: Could probably be simplified using Uniform_Limit *)
 lemma has_complex_derivative_sequence:
@@ -914,7 +910,7 @@
     by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
 qed
 
-subsection\<open>Bound theorem\<close>
+subsection%unimportant\<open>Bound theorem\<close>
 
 lemma field_differentiable_bound:
   fixes S :: "'a::real_normed_field set"
@@ -928,7 +924,7 @@
   apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
   done
 
-subsection\<open>Inverse function theorem for complex derivatives\<close>
+subsection%unimportant\<open>Inverse function theorem for complex derivatives\<close>
 
 lemma has_field_derivative_inverse_basic:
   shows "DERIV f (g y) :> f' \<Longrightarrow>
@@ -969,7 +965,7 @@
   apply (rule has_derivative_inverse_strong_x [of S g y f])
   by auto
 
-subsection \<open>Taylor on Complex Numbers\<close>
+subsection%unimportant \<open>Taylor on Complex Numbers\<close>
 
 lemma sum_Suc_reindex:
   fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
@@ -1155,7 +1151,7 @@
 qed
 
 
-subsection \<open>Polynomal function extremal theorem, from HOL Light\<close>
+subsection%unimportant \<open>Polynomal function extremal theorem, from HOL Light\<close>
 
 lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
     fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
diff -r dff89effe26b -r 922833cc6839 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Oct 22 12:22:18 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Oct 22 19:03:47 2018 +0200
@@ -9,10 +9,12 @@
    "HOL-Library.Periodic_Fun"
 begin
 
+subsection\<open>Möbius transformations\<close>
+
 (* TODO: Figure out what to do with Möbius transformations *)
-definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
-
-lemma moebius_inverse:
+definition%important "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
+
+theorem moebius_inverse:
   assumes "a * d \<noteq> b * c" "c * z + d \<noteq> 0"
   shows   "moebius d (-b) (-c) a (moebius a b c d z) = z"
 proof -
@@ -62,7 +64,7 @@
     by (simp add: norm_power Im_power2)
 qed
 
-subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
+subsection%unimportant\<open>The Exponential Function\<close>
 
 lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   by simp
@@ -114,7 +116,7 @@
     using sums_unique2 by blast
 qed
 
-corollary exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
+corollary%unimportant exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
   using exp_Euler [of "-z"]
   by simp
 
@@ -127,7 +129,32 @@
 lemma cos_exp_eq:  "cos z = (exp(\<i> * z) + exp(-(\<i> * z))) / 2"
   by (simp add: exp_Euler exp_minus_Euler)
 
-subsection\<open>Relationships between real and complex trigonometric and hyperbolic functions\<close>
+theorem Euler: "exp(z) = of_real(exp(Re z)) *
+              (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
+by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)
+
+lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
+  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
+
+lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
+  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
+
+lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
+  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
+
+lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
+  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
+
+lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
+  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
+
+lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
+  by (simp add: Re_sin Im_sin algebra_simps)
+
+lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
+  by (simp add: Re_sin Im_sin algebra_simps)
+
+subsection%unimportant\<open>Relationships between real and complex trigonometric and hyperbolic functions\<close>
 
 lemma real_sin_eq [simp]: "Re(sin(of_real x)) = sin x"
   by (simp add: sin_of_real)
@@ -186,34 +213,7 @@
   shows   "(\<lambda>x. cos (f x)) holomorphic_on A"
   using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)
 
-subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
-
-lemma Euler: "exp(z) = of_real(exp(Re z)) *
-              (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
-by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)
-
-lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
-  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
-
-lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
-  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
-
-lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
-  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
-
-lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
-  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
-
-lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
-  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
-
-lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
-  by (simp add: Re_sin Im_sin algebra_simps)
-
-lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
-  by (simp add: Re_sin Im_sin algebra_simps)
-
-subsection\<open>More on the Polar Representation of Complex Numbers\<close>
+subsection%unimportant\<open>More on the Polar Representation of Complex Numbers\<close>
 
 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
   by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
@@ -693,7 +693,7 @@
 qed
 
 
-subsection\<open>Taylor series for complex exponential, sine and cosine\<close>
+subsection%unimportant\<open>Taylor series for complex exponential, sine and cosine\<close>
 
 declare power_Suc [simp del]
 
@@ -859,10 +859,10 @@
 
 subsection\<open>The argument of a complex number (HOL Light version)\<close>
 
-definition is_Arg :: "[complex,real] \<Rightarrow> bool"
+definition%important is_Arg :: "[complex,real] \<Rightarrow> bool"
   where "is_Arg z r \<equiv> z = of_real(norm z) * exp(\<i> * of_real r)"
 
-definition Arg2pi :: "complex \<Rightarrow> real"
+definition%important Arg2pi :: "complex \<Rightarrow> real"
   where "Arg2pi z \<equiv> if z = 0 then 0 else THE t. 0 \<le> t \<and> t < 2*pi \<and> is_Arg z t"
 
 lemma is_Arg_2pi_iff: "is_Arg z (r + of_int k * (2 * pi)) \<longleftrightarrow> is_Arg z r"
@@ -940,7 +940,7 @@
     done
 qed
 
-corollary
+corollary%unimportant
   shows Arg2pi_ge_0: "0 \<le> Arg2pi z"
     and Arg2pi_lt_2pi: "Arg2pi z < 2*pi"
     and Arg2pi_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
@@ -1023,7 +1023,7 @@
     by blast
 qed auto
 
-corollary Arg2pi_gt_0:
+corollary%unimportant Arg2pi_gt_0:
   assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
     shows "Arg2pi z > 0"
   using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order
@@ -1128,7 +1128,7 @@
     by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
 qed
 
-subsection\<open>Analytic properties of tangent function\<close>
+subsection%unimportant\<open>Analytic properties of tangent function\<close>
 
 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
   by (simp add: cnj_cos cnj_sin tan_def)
@@ -1151,12 +1151,12 @@
   by (simp add: field_differentiable_within_tan holomorphic_on_def)
 
 
-subsection\<open>Complex logarithms (the conventional principal value)\<close>
+subsection\<open>The principal branch of the Complex logarithm\<close>
 
 instantiation complex :: ln
 begin
 
-definition ln_complex :: "complex \<Rightarrow> complex"
+definition%important ln_complex :: "complex \<Rightarrow> complex"
   where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
 
 text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close>
@@ -1189,7 +1189,7 @@
   apply auto
   done
 
-subsection\<open>Relation to Real Logarithm\<close>
+subsection%unimportant\<open>Relation to Real Logarithm\<close>
 
 lemma Ln_of_real:
   assumes "0 < z"
@@ -1203,10 +1203,10 @@
     using assms by simp
 qed
 
-corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
+corollary%unimportant Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
   by (auto simp: Ln_of_real elim: Reals_cases)
 
-corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
+corollary%unimportant Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
   by (simp add: Ln_of_real)
 
 lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
@@ -1244,13 +1244,13 @@
 lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
   by (metis exp_Ln ln_exp norm_exp_eq_Re)
 
-corollary ln_cmod_le:
+corollary%unimportant ln_cmod_le:
   assumes z: "z \<noteq> 0"
     shows "ln (cmod z) \<le> cmod (Ln z)"
   using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
   by (metis Re_Ln complex_Re_le_cmod z)
 
-proposition exists_complex_root:
+proposition%unimportant exists_complex_root:
   fixes z :: complex
   assumes "n \<noteq> 0"  obtains w where "z = w ^ n"
 proof (cases "z=0")
@@ -1259,13 +1259,13 @@
     by (rule_tac w = "exp(Ln z / n)" in that) (simp add: assms exp_of_nat_mult [symmetric])
 qed (use assms in auto)
 
-corollary exists_complex_root_nonzero:
+corollary%unimportant exists_complex_root_nonzero:
   fixes z::complex
   assumes "z \<noteq> 0" "n \<noteq> 0"
   obtains w where "w \<noteq> 0" "z = w ^ n"
   by (metis exists_complex_root [of n z] assms power_0_left)
 
-subsection\<open>Derivative of Ln away from the branch cut\<close>
+subsection%unimportant\<open>Derivative of Ln away from the branch cut\<close>
 
 lemma
   assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
@@ -1357,8 +1357,106 @@
   qed
 qed
 
-
-subsection\<open>Quadrant-type results for Ln\<close>
+theorem Ln_series:
+  fixes z :: complex
+  assumes "norm z < 1"
+  shows   "(\<lambda>n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\<lambda>n. ?f n * z^n) sums _")
+proof -
+  let ?F = "\<lambda>z. \<Sum>n. ?f n * z^n" and ?F' = "\<lambda>z. \<Sum>n. diffs ?f n * z^n"
+  have r: "conv_radius ?f = 1"
+    by (intro conv_radius_ratio_limit_nonzero[of _ 1])
+       (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)
+
+  have "\<exists>c. \<forall>z\<in>ball 0 1. ln (1 + z) - ?F z = c"
+  proof (rule has_field_derivative_zero_constant)
+    fix z :: complex assume z': "z \<in> ball 0 1"
+    hence z: "norm z < 1" by simp
+    define t :: complex where "t = of_real (1 + norm z) / 2"
+    from z have t: "norm z < norm t" "norm t < 1" unfolding t_def
+      by (simp_all add: field_simps norm_divide del: of_real_add)
+
+    have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
+    also from z have "... < 1" by simp
+    finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
+      by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
+    moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
+      by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
+    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
+                       (at z within ball 0 1)"
+      by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
+    also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
+      by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all
+    from sums_split_initial_segment[OF this, of 1]
+      have "(\<lambda>i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)
+    hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)
+    also have "inverse (1 + z) - inverse (1 + z) = 0" by simp
+    finally show "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .
+  qed simp_all
+  then obtain c where c: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> ln (1 + z) - ?F z = c" by blast
+  from c[of 0] have "c = 0" by (simp only: powser_zero) simp
+  with c[of z] assms have "ln (1 + z) = ?F z" by simp
+  moreover have "summable (\<lambda>n. ?f n * z^n)" using assms r
+    by (intro summable_in_conv_radius) simp_all
+  ultimately show ?thesis by (simp add: sums_iff)
+qed
+
+lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
+  by (drule Ln_series) (simp add: power_minus')
+
+lemma ln_series':
+  assumes "abs (x::real) < 1"
+  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
+proof -
+  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
+    by (intro Ln_series') simp_all
+  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
+    by (rule ext) simp
+  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
+    by (subst Ln_of_real [symmetric]) simp_all
+  finally show ?thesis by (subst (asm) sums_of_real_iff)
+qed
+
+lemma Ln_approx_linear:
+  fixes z :: complex
+  assumes "norm z < 1"
+  shows   "norm (ln (1 + z) - z) \<le> norm z^2 / (1 - norm z)"
+proof -
+  let ?f = "\<lambda>n. (-1)^Suc n / of_nat n"
+  from assms have "(\<lambda>n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp
+  moreover have "(\<lambda>n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp
+  ultimately have "(\<lambda>n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"
+    by (subst left_diff_distrib, intro sums_diff) simp_all
+  from sums_split_initial_segment[OF this, of "Suc 1"]
+    have "(\<lambda>i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"
+    by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)
+  hence "(Ln (1 + z) - z) = (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"
+    by (simp add: sums_iff)
+  also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
+    by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
+       (auto simp: assms field_simps intro!: always_eventually)
+  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
+             (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
+    by (intro summable_norm)
+       (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
+  also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
+    by (intro mult_left_mono) (simp_all add: divide_simps)
+  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))
+         \<le> (\<Sum>i. norm (-(z^2) * (-z)^i))"
+    using A assms
+    apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
+    apply (intro suminf_le summable_mult summable_geometric)
+    apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
+    done
+  also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms
+    by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
+  also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms
+    by (subst suminf_geometric) (simp_all add: divide_inverse)
+  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
+  finally show ?thesis .
+qed
+
+
+subsection%unimportant\<open>Quadrant-type results for Ln\<close>
 
 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
   using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
@@ -1455,7 +1553,7 @@
     mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
 
 
-subsection\<open>More Properties of Ln\<close>
+subsection%unimportant\<open>More Properties of Ln\<close>
 
 lemma cnj_Ln: assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" shows "cnj(Ln z) = Ln(cnj z)"
 proof (cases "z=0")
@@ -1533,27 +1631,27 @@
   using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
   by (auto simp: exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
 
-corollary Ln_times_simple:
+corollary%unimportant Ln_times_simple:
     "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
          \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
   by (simp add: Ln_times)
 
-corollary Ln_times_of_real:
+corollary%unimportant Ln_times_of_real:
     "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_real r * z) = ln r + Ln(z)"
   using mpi_less_Im_Ln Im_Ln_le_pi
   by (force simp: Ln_times)
 
-corollary Ln_times_Reals:
+corollary%unimportant Ln_times_Reals:
     "\<lbrakk>r \<in> Reals; Re r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(r * z) = ln (Re r) + Ln(z)"
   using Ln_Reals_eq Ln_times_of_real by fastforce
 
-corollary Ln_divide_of_real:
+corollary%unimportant Ln_divide_of_real:
     "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
 using Ln_times_of_real [of "inverse r" z]
 by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric]
          del: of_real_inverse)
 
-corollary Ln_prod:
+corollary%unimportant Ln_prod:
   fixes f :: "'a \<Rightarrow> complex"
   assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
   shows "\<exists>n. Ln (prod f A) = (\<Sum>x \<in> A. Ln (f x) + (of_int (n x) * (2 * pi)) * \<i>)"
@@ -1655,7 +1753,7 @@
 
 text\<open>Finally: it's is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
 
-definition Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
+definition%important Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
 
 lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
   by (simp add: Im_Ln_eq_pi Arg_def)
@@ -1793,7 +1891,7 @@
   using complex_is_Real_iff
   by (simp add: Arg_def Im_Ln_eq_0) (metis less_eq_real_def of_real_Re of_real_def scale_zero_left)
 
-corollary Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
+corollary%unimportant Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
   using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
 
 lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
@@ -1869,7 +1967,7 @@
   using continuous_at_Arg continuous_at_imp_continuous_within by blast
 
 
-subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
+subsection\<open>The Unwinding Number and the Ln product Formula\<close>
 
 text\<open>Note that in this special case the unwinding number is -1, 0 or 1. But it's always an integer.\<close>
 
@@ -1895,7 +1993,7 @@
   using Arg_exp_diff_2pi [of z]
   by (force simp: Ints_def image_def field_simps Arg_def intro!: complex_eqI)
 
-definition unwinding :: "complex \<Rightarrow> int" where
+definition%important unwinding :: "complex \<Rightarrow> int" where
    "unwinding z \<equiv> THE k. of_int k = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
 
 lemma unwinding: "of_int (unwinding z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
@@ -1910,7 +2008,7 @@
   using unwinding_2pi by (simp add: exp_add)
 
 
-subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
+subsection%unimportant\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
 
 lemma Arg2pi_Ln:
   assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi"
@@ -1960,104 +2058,6 @@
   qed (use assms in auto)
 qed
 
-lemma Ln_series:
-  fixes z :: complex
-  assumes "norm z < 1"
-  shows   "(\<lambda>n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\<lambda>n. ?f n * z^n) sums _")
-proof -
-  let ?F = "\<lambda>z. \<Sum>n. ?f n * z^n" and ?F' = "\<lambda>z. \<Sum>n. diffs ?f n * z^n"
-  have r: "conv_radius ?f = 1"
-    by (intro conv_radius_ratio_limit_nonzero[of _ 1])
-       (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)
-
-  have "\<exists>c. \<forall>z\<in>ball 0 1. ln (1 + z) - ?F z = c"
-  proof (rule has_field_derivative_zero_constant)
-    fix z :: complex assume z': "z \<in> ball 0 1"
-    hence z: "norm z < 1" by simp
-    define t :: complex where "t = of_real (1 + norm z) / 2"
-    from z have t: "norm z < norm t" "norm t < 1" unfolding t_def
-      by (simp_all add: field_simps norm_divide del: of_real_add)
-
-    have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
-    also from z have "... < 1" by simp
-    finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
-      by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
-    moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
-      by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
-    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
-                       (at z within ball 0 1)"
-      by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
-    also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
-      by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all
-    from sums_split_initial_segment[OF this, of 1]
-      have "(\<lambda>i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)
-    hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)
-    also have "inverse (1 + z) - inverse (1 + z) = 0" by simp
-    finally show "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .
-  qed simp_all
-  then obtain c where c: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> ln (1 + z) - ?F z = c" by blast
-  from c[of 0] have "c = 0" by (simp only: powser_zero) simp
-  with c[of z] assms have "ln (1 + z) = ?F z" by simp
-  moreover have "summable (\<lambda>n. ?f n * z^n)" using assms r
-    by (intro summable_in_conv_radius) simp_all
-  ultimately show ?thesis by (simp add: sums_iff)
-qed
-
-lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
-  by (drule Ln_series) (simp add: power_minus')
-
-lemma ln_series':
-  assumes "abs (x::real) < 1"
-  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
-proof -
-  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
-    by (intro Ln_series') simp_all
-  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
-    by (rule ext) simp
-  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
-    by (subst Ln_of_real [symmetric]) simp_all
-  finally show ?thesis by (subst (asm) sums_of_real_iff)
-qed
-
-lemma Ln_approx_linear:
-  fixes z :: complex
-  assumes "norm z < 1"
-  shows   "norm (ln (1 + z) - z) \<le> norm z^2 / (1 - norm z)"
-proof -
-  let ?f = "\<lambda>n. (-1)^Suc n / of_nat n"
-  from assms have "(\<lambda>n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp
-  moreover have "(\<lambda>n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp
-  ultimately have "(\<lambda>n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"
-    by (subst left_diff_distrib, intro sums_diff) simp_all
-  from sums_split_initial_segment[OF this, of "Suc 1"]
-    have "(\<lambda>i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"
-    by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)
-  hence "(Ln (1 + z) - z) = (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"
-    by (simp add: sums_iff)
-  also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
-    by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
-       (auto simp: assms field_simps intro!: always_eventually)
-  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
-             (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
-    by (intro summable_norm)
-       (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
-  also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
-    by (intro mult_left_mono) (simp_all add: divide_simps)
-  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))
-         \<le> (\<Sum>i. norm (-(z^2) * (-z)^i))"
-    using A assms
-    apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
-    apply (intro suminf_le summable_mult summable_geometric)
-    apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
-    done
-  also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms
-    by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
-  also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms
-    by (subst suminf_geometric) (simp_all add: divide_inverse)
-  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
-  finally show ?thesis .
-qed
-
 
 text\<open>Relation between Arg2pi and arctangent in upper halfplane\<close>
 lemma Arg2pi_arctan_upperhalf:
@@ -2166,7 +2166,7 @@
   using open_Arg2pi2pi_gt [of t]
   by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
 
-subsection\<open>Complex Powers\<close>
+subsection%unimportant\<open>Complex Powers\<close>
 
 lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
   by (simp add: powr_def)
@@ -2535,7 +2535,7 @@
 qed
 
 
-subsection\<open>Some Limits involving Logarithms\<close>
+subsection%unimportant\<open>Some Limits involving Logarithms\<close>
 
 lemma lim_Ln_over_power:
   fixes s::complex
@@ -2686,7 +2686,7 @@
 qed
 
 
-subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
+subsection%unimportant\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
 
 lemma csqrt_exp_Ln:
   assumes "z \<noteq> 0"
@@ -2759,7 +2759,7 @@
     "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) csqrt"
   by (simp add: field_differentiable_within_csqrt field_differentiable_imp_continuous_at)
 
-corollary isCont_csqrt' [simp]:
+corollary%unimportant isCont_csqrt' [simp]:
    "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
   by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
 
@@ -2802,7 +2802,7 @@
 
 text\<open>The branch cut gives standard bounds in the real case.\<close>
 
-definition Arctan :: "complex \<Rightarrow> complex" where
+definition%important Arctan :: "complex \<Rightarrow> complex" where
     "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
 
 lemma Arctan_def_moebius: "Arctan z = \<i>/2 * Ln (moebius (-\<i>) 1 \<i> 1 z)"
@@ -2948,7 +2948,7 @@
     "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
   by (simp add: field_differentiable_within_Arctan holomorphic_on_def)
 
-lemma Arctan_series:
+theorem Arctan_series:
   assumes z: "norm (z :: complex) < 1"
   defines "g \<equiv> \<lambda>n. if odd n then -\<i>*\<i>^n / n else 0"
   defines "h \<equiv> \<lambda>z n. (-1)^n / of_nat (2*n+1) * (z::complex)^(2*n+1)"
@@ -3022,7 +3022,7 @@
 qed
 
 text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>
-lemma ln_series_quadratic:
+theorem ln_series_quadratic:
   assumes x: "x > (0::real)"
   shows "(\<lambda>n. (2*((x - 1) / (x + 1)) ^ (2*n+1) / of_nat (2*n+1))) sums ln x"
 proof -
@@ -3051,7 +3051,7 @@
   finally show ?thesis by (subst (asm) sums_of_real_iff)
 qed
 
-subsection \<open>Real arctangent\<close>
+subsection%unimportant \<open>Real arctangent\<close>
 
 lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
 proof -
@@ -3212,7 +3212,7 @@
     by (auto simp: arctan_series)
 qed
 
-subsection \<open>Bounds on pi using real arctangent\<close>
+subsection%unimportant \<open>Bounds on pi using real arctangent\<close>
 
 lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
   using machin by simp
@@ -3223,13 +3223,13 @@
         arctan_bounds[of "1/239" 4]
   by (simp_all add: eval_nat_numeral)
 
-corollary pi_gt3: "pi > 3"
+lemma pi_gt3: "pi > 3"
   using pi_approx by simp
 
 
 subsection\<open>Inverse Sine\<close>
 
-definition Arcsin :: "complex \<Rightarrow> complex" where
+definition%important Arcsin :: "complex \<Rightarrow> complex" where
    "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
 
 lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 0"
@@ -3396,7 +3396,7 @@
 
 subsection\<open>Inverse Cosine\<close>
 
-definition Arccos :: "complex \<Rightarrow> complex" where
+definition%important Arccos :: "complex \<Rightarrow> complex" where
    "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
 
 lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
@@ -3555,7 +3555,7 @@
   by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
 
 
-subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
+subsection%unimportant\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
 
 lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> \<bar>Re(Arcsin z)\<bar> < pi/2"
   unfolding Re_Arcsin
@@ -3608,7 +3608,7 @@
 qed
 
 
-subsection\<open>Interrelations between Arcsin and Arccos\<close>
+subsection%unimportant\<open>Interrelations between Arcsin and Arccos\<close>
 
 lemma cos_Arcsin_nonzero:
   assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
@@ -3710,7 +3710,7 @@
   by (simp add: Arcsin_Arccos_csqrt_pos)
 
 
-subsection\<open>Relationship with Arcsin on the Real Numbers\<close>
+subsection%unimportant\<open>Relationship with Arcsin on the Real Numbers\<close>
 
 lemma Im_Arcsin_of_real:
   assumes "\<bar>x\<bar> \<le> 1"
@@ -3727,7 +3727,7 @@
     by (simp add: Im_Arcsin exp_minus)
 qed
 
-corollary Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
+corollary%unimportant Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
   by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
 
 lemma arcsin_eq_Re_Arcsin:
@@ -3760,7 +3760,7 @@
   by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
 
 
-subsection\<open>Relationship with Arccos on the Real Numbers\<close>
+subsection%unimportant\<open>Relationship with Arccos on the Real Numbers\<close>
 
 lemma Im_Arccos_of_real:
   assumes "\<bar>x\<bar> \<le> 1"
@@ -3777,7 +3777,7 @@
     by (simp add: Im_Arccos exp_minus)
 qed
 
-corollary Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
+corollary%unimportant Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
   by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
 
 lemma arccos_eq_Re_Arccos:
@@ -3809,7 +3809,7 @@
 lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
   by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
 
-subsection\<open>Some interrelationships among the real inverse trig functions\<close>
+subsection%unimportant\<open>Some interrelationships among the real inverse trig functions\<close>
 
 lemma arccos_arctan:
   assumes "-1 < x" "x < 1"
@@ -3879,7 +3879,7 @@
   using arccos_arcsin_sqrt_pos [of "-x"]
   by (simp add: arccos_minus)
 
-subsection\<open>Continuity results for arcsin and arccos\<close>
+subsection%unimportant\<open>Continuity results for arcsin and arccos\<close>
 
 lemma continuous_on_Arcsin_real [continuous_intros]:
     "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
@@ -3945,7 +3945,7 @@
 
 subsection\<open>Roots of unity\<close>
 
-lemma complex_root_unity:
+theorem complex_root_unity:
   fixes j::nat
   assumes "n \<noteq> 0"
     shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
@@ -4033,7 +4033,7 @@
   apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
   done
 
-subsection\<open> Formulation of loop homotopy in terms of maps out of type complex\<close>
+subsection\<open>Formulation of loop homotopy in terms of maps out of type complex\<close>
 
 lemma homotopic_circlemaps_imp_homotopic_loops:
   assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
diff -r dff89effe26b -r 922833cc6839 src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Mon Oct 22 12:22:18 2018 +0200
+++ b/src/HOL/Analysis/Embed_Measure.thy	Mon Oct 22 19:03:47 2018 +0200
@@ -6,13 +6,23 @@
     measure on the left part of the sum type 'a + 'b)
 *)
 
-section \<open>Embed Measure Spaces with a Function\<close>
+section \<open>Embedding Measure Spaces with a Function\<close>
 
 theory Embed_Measure
 imports Binary_Product_Measure
 begin
 
-definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
+text \<open>
+  Given a measure space on some carrier set \<open>\<Omega>\<close> and a function \<open>f\<close>, we can define a push-forward
+  measure on the carrier set $f(\Omega)$ whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
+  the original sigma algebra.
+
+  This is useful e.\,g.\ when \<open>f\<close> is injective, i.\,e.\ it is some kind of ``tagging'' function.
+  For instance, suppose we have some algebraaic datatype of values with various constructors,
+  including a constructor \<open>RealVal\<close> for real numbers. Then \<open>embed_measure\<close> allows us to lift a 
+  measure on real numbers to the appropriate subset of that algebraic datatype.
+\<close>
+definition%important embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
   "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M}
                            (\<lambda>A. emeasure M (f -` A \<inter> space M))"
 
diff -r dff89effe26b -r 922833cc6839 src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Mon Oct 22 12:22:18 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Mon Oct 22 19:03:47 2018 +0200
@@ -6,7 +6,7 @@
     This could probably be weakened somehow.
 *)
 
-section \<open>Integration by Substition\<close>
+section \<open>Integration by Substition for the Lebesgue integral\<close>
 
 theory Lebesgue_Integral_Substitution
 imports Interval_Integral
@@ -278,7 +278,7 @@
   qed
 qed
 
-lemma nn_integral_substitution:
+theorem nn_integral_substitution:
   fixes f :: "real \<Rightarrow> real"
   assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
@@ -317,7 +317,7 @@
   finally show ?thesis .
 qed auto
 
-lemma integral_substitution:
+theorem integral_substitution:
   assumes integrable: "set_integrable lborel {g a..g b} f"
   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes contg': "continuous_on {a..b} g'"
@@ -384,7 +384,7 @@
                      (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
 qed
 
-lemma interval_integral_substitution:
+theorem interval_integral_substitution:
   assumes integrable: "set_integrable lborel {g a..g b} f"
   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes contg': "continuous_on {a..b} g'"