--- 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"
--- 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"
--- 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))"
--- 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'"