--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Jun 25 14:45:05 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Jun 25 14:06:50 2018 +0100
@@ -84,7 +84,7 @@
shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
using arc_simple_path inside_arc_empty by blast
-
+
subsection \<open>Piecewise differentiable functions\<close>
definition piecewise_differentiable_on
@@ -466,7 +466,7 @@
next
case False
have *: "\<And>x. finite (S \<inter> {y. m * y + c = x})"
- using False not_finite_existsD by fastforce
+ using False not_finite_existsD by fastforce
show ?thesis
apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise])
apply (rule * assms derivative_intros | simp add: False vimage_def)+
@@ -601,7 +601,7 @@
have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
proof (rule differentiable_transform_within)
show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x"
- using that g12D
+ using that g12D
apply (simp only: joinpaths_def)
by (rule differentiable_chain_at derivative_intros | force)+
show "\<And>x'. \<lbrakk>dist x' x < dist (x/2) (1/2)\<rbrakk>
@@ -740,7 +740,7 @@
by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - S\<close> that)
next
have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
- then show "f differentiable at (g t)"
+ then show "f differentiable at (g t)"
using der[THEN field_differentiable_imp_differentiable] by auto
qed
moreover have "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
@@ -767,7 +767,7 @@
qed
ultimately have "f \<circ> g C1_differentiable_on {0..1} - S"
using C1_differentiable_on_eq by blast
- moreover have "path (f \<circ> g)"
+ moreover have "path (f \<circ> g)"
apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
using der
by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
@@ -898,7 +898,7 @@
{0..1}"
using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]]
by (simp add: has_integral_neg)
- then show ?thesis
+ then show ?thesis
using S
apply (clarsimp simp: reversepath_def has_contour_integral_def)
apply (rule_tac S = "(\<lambda>x. 1 - x) ` S" in has_integral_spike_finite)
@@ -2155,7 +2155,7 @@
done
} note * = this
show ?thesis
- using cd e
+ using cd e
apply (simp add: field_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def)
apply (clarify dest!: spec mp)
using * unfolding dist_norm
@@ -2508,7 +2508,7 @@
by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull])
have **: "\<And>f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)"
by (simp add: algebra_simps)
- have "norm (?pathint (shrink u) (shrink v) - ?pathint u v)
+ have "norm (?pathint (shrink u) (shrink v) - ?pathint u v)
\<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))"
apply (rule has_integral_bound
[of _ "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
@@ -2835,7 +2835,7 @@
qed
lemma contour_integral_convex_primitive:
- assumes "convex S" "continuous_on S f"
+ assumes "convex S" "continuous_on S f"
"\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
obtains g where "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative f x) (at x within S)"
proof (cases "S={}")
@@ -2846,7 +2846,7 @@
lemma holomorphic_convex_primitive:
fixes f :: "complex \<Rightarrow> complex"
- assumes "convex S" "finite K" and contf: "continuous_on S f"
+ assumes "convex S" "finite K" and contf: "continuous_on S f"
and fd: "\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x"
obtains g where "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative f x) (at x within S)"
proof (rule contour_integral_convex_primitive [OF \<open>convex S\<close> contf Cauchy_theorem_triangle_cofinite])
@@ -2871,7 +2871,7 @@
corollary Cauchy_theorem_convex:
"\<lbrakk>continuous_on S f; convex S; finite K;
\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x;
- valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk>
+ valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk>
\<Longrightarrow> (f has_contour_integral 0) g"
by (metis holomorphic_convex_primitive Cauchy_theorem_primitive)
@@ -3561,14 +3561,14 @@
assume "0 < e" and g: "winding_number_prop p z e g n"
then show "\<exists>r. winding_number_prop (\<lambda>w. p w - z) 0 e r n"
by (rule_tac x="\<lambda>t. g t - z" in exI)
- (force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs
+ (force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs
vector_derivative_def has_vector_derivative_diff_const piecewise_C1_differentiable_diff C1_differentiable_imp_piecewise)
next
fix n e g
assume "0 < e" and g: "winding_number_prop (\<lambda>w. p w - z) 0 e g n"
then show "\<exists>r. winding_number_prop p z e r n"
apply (rule_tac x="\<lambda>t. g t + z" in exI)
- apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs
+ apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs
piecewise_C1_differentiable_add vector_derivative_def has_vector_derivative_add_const C1_differentiable_imp_piecewise)
apply (force simp: algebra_simps)
done
@@ -3665,7 +3665,7 @@
by (force simp: ge0)
show "((\<lambda>x. if 0 < x \<and> x < 1 then ?vd x else 0) has_integral ?int z) (cbox 0 1)"
by (rule has_integral_spike_interior [OF hi]) simp
- qed
+ qed
then show ?thesis
by (simp add: Re_winding_number [OF \<gamma>] field_simps)
qed
@@ -3679,7 +3679,7 @@
let ?vd = "\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)"
let ?int = "\<lambda>z. contour_integral \<gamma> (\<lambda>w. 1 / (w - z))"
have hi: "(?vd has_integral ?int z) (cbox 0 1)"
- unfolding box_real
+ unfolding box_real
apply (subst has_contour_integral [symmetric])
using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
@@ -3782,7 +3782,7 @@
unfolding integrable_on_def [symmetric]
proof (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>]])
show "\<exists>d h. 0 < d \<and>
- (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))"
+ (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))"
if "w \<in> - {z}" for w
apply (rule_tac x="norm(w - z)" in exI)
using that inverse_eq_divide has_field_derivative_at_within h
@@ -3899,21 +3899,21 @@
have cont: "continuous_on {0..1}
(\<lambda>x. Im (integral {0..x} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))))"
by (intro continuous_intros indefinite_integral_continuous_1 winding_number_exp_integral [OF gpd]; simp)
- have "Arg r \<le> 2*pi"
- by (simp add: Arg less_eq_real_def)
+ have "Arg2pi r \<le> 2*pi"
+ by (simp add: Arg2pi less_eq_real_def)
also have "\<dots> \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))"
using 1
apply (simp add: winding_number_valid_path [OF \<gamma> z] contour_integral_integral)
apply (simp add: Complex.Re_divide field_simps power2_eq_square)
done
- finally have "Arg r \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))" .
- then have "\<exists>t. t \<in> {0..1} \<and> Im(integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg r"
- by (simp add: Arg_ge_0 cont IVT')
+ finally have "Arg2pi r \<le> Im (integral {0..1} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z)))" .
+ then have "\<exists>t. t \<in> {0..1} \<and> Im(integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg2pi r"
+ by (simp add: Arg2pi_ge_0 cont IVT')
then obtain t where t: "t \<in> {0..1}"
- and eqArg: "Im (integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg r"
+ and eqArg: "Im (integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg2pi r"
by blast
define i where "i = integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
- have iArg: "Arg r = Im i"
+ have iArg: "Arg2pi r = Im i"
using eqArg by (simp add: i_def)
have gpdt: "\<gamma> piecewise_C1_differentiable_on {0..t}"
by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t)
@@ -3927,7 +3927,7 @@
by (simp add: r_def)
then have "z + complex_of_real (exp (Re i)) * (w - z) / complex_of_real (cmod r) = \<gamma> t"
apply simp
- apply (subst Complex_Transcendental.Arg_eq [of r])
+ apply (subst Complex_Transcendental.Arg2pi_eq [of r])
apply (simp add: iArg)
using * apply (simp add: exp_eq_polar field_simps)
done
@@ -4158,7 +4158,7 @@
lemma winding_number_eq:
"\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> S; z \<in> S; connected S; S \<inter> path_image \<gamma> = {}\<rbrakk>
\<Longrightarrow> winding_number \<gamma> w = winding_number \<gamma> z"
- using winding_number_constant by (metis constant_on_def)
+ using winding_number_constant by (metis constant_on_def)
lemma open_winding_number_levelsets:
assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
@@ -5329,7 +5329,7 @@
using \<open>0 \<le> B\<close> \<open>0 < e\<close> by (simp add: divide_simps)
have "\<exists>h. (\<forall>x\<in>{0..1}. cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - h x) \<le> e) \<and> h integrable_on {0..1}"
proof (intro exI conjI ballI)
- show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e"
+ show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e"
if "x \<in> {0..1}" for x
apply (rule order_trans [OF _ Ble])
using noleB [OF that] fga [OF that] \<open>0 \<le> B\<close> \<open>0 < e\<close>
@@ -5339,13 +5339,13 @@
qed (rule inta)
}
then show lintg: "l contour_integrable_on \<gamma>"
- unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
+ unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
{ fix e::real
define B' where "B' = B + 1"
have B': "B' > 0" "B' > B" using \<open>0 \<le> B\<close> by (auto simp: B'_def)
assume "0 < e"
then have ev_no': "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. 2 * cmod (f n x - l x) < e / B'"
- using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B' / 2"] B'
+ using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B' / 2"] B'
by (simp add: field_simps)
have ie: "integral {0..1::real} (\<lambda>x. e / 2) < e" using \<open>0 < e\<close> by simp
have *: "cmod (f x (\<gamma> t) * vector_derivative \<gamma> (at t) - l (\<gamma> t) * vector_derivative \<gamma> (at t)) \<le> e / 2"
@@ -6024,7 +6024,7 @@
\<Longrightarrow> f field_differentiable at x" for a b c x
by (metis cdf Diff_iff Int_iff ball_min_Int subsetD convex_ball e interior_mono interior_subset subset_hull)
obtain g where "\<And>w. w \<in> ball z (min d e) \<Longrightarrow> (g has_field_derivative f w) (at w within ball z (min d e))"
- apply (rule contour_integral_convex_primitive
+ apply (rule contour_integral_convex_primitive
[OF convex_ball fde Cauchy_theorem_triangle_cofinite [OF _ K]])
using cont fd by auto
then have "f holomorphic_on ball z (min d e)"
@@ -6040,7 +6040,7 @@
lemma no_isolated_singularity':
fixes z::complex
- assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)"
+ assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)"
and holf: "f holomorphic_on (S - K)" and S: "open S" and K: "finite K"
shows "f holomorphic_on S"
proof (rule no_isolated_singularity[OF _ assms(2-)])
@@ -6050,9 +6050,9 @@
show "(f \<longlongrightarrow> f z) (at z within S)"
proof (cases "z \<in> K")
case False
- from holf have "continuous_on (S - K) f"
+ from holf have "continuous_on (S - K) f"
by (rule holomorphic_on_imp_continuous_on)
- with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))"
+ with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))"
by (simp add: continuous_on_def)
also from z K S False have "at z within (S - K) = at z within S"
by (subst (1 2) at_within_open) (auto intro: finite_imp_closed)
@@ -6071,7 +6071,7 @@
have *: "\<And>x. x \<in> interior S \<Longrightarrow> f field_differentiable at x"
unfolding holomorphic_on_open [symmetric] field_differentiable_def
using no_isolated_singularity [where S = "interior S"]
- by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd
+ by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd
field_differentiable_at_within field_differentiable_def holomorphic_onI
holomorphic_on_imp_differentiable_at open_interior)
show ?thesis
@@ -6159,7 +6159,7 @@
proof -
\<comment> \<open>Replacing @{term r} and the original (weak) premises with stronger ones\<close>
obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
- proof
+ proof
have "cball z ((r + dist w z) / 2) \<subseteq> ball z r"
using w by (simp add: dist_commute real_sum_of_halves subset_eq)
then show "f holomorphic_on cball z ((r + dist w z) / 2)"
@@ -6169,7 +6169,7 @@
then show "0 < (r + dist w z) / 2"
by simp (use zero_le_dist [of w z] in linarith)
qed (use w in \<open>auto simp: dist_commute\<close>)
- then have holf: "f holomorphic_on ball z r"
+ then have holf: "f holomorphic_on ball z r"
using ball_subset_cball holomorphic_on_subset by blast
have contf: "continuous_on (cball z r) f"
by (simp add: holfc holomorphic_on_imp_continuous_on)
@@ -6179,12 +6179,12 @@
by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
- proof
+ proof
show "\<And>u. cmod (u - z) = r \<Longrightarrow> r - dist z w \<le> cmod (u - w)"
by (metis add_diff_eq diff_add_cancel dist_norm norm_diff_ineq)
qed (use w in \<open>auto simp: dist_norm norm_minus_commute\<close>)
have ul: "uniform_limit (sphere z r) (\<lambda>n x. (\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k))) (\<lambda>x. f x / (x - w)) sequentially"
- unfolding uniform_limit_iff dist_norm
+ unfolding uniform_limit_iff dist_norm
proof clarify
fix e::real
assume "0 < e"
@@ -6378,7 +6378,7 @@
apply (auto intro: Cauchy_higher_derivative_integral_circlepath [where k=0, simplified])
done
have ul_less: "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - w)) (\<lambda>x. g x / (x - w)) F"
- using greater \<open>0 < d\<close>
+ using greater \<open>0 < d\<close>
apply (clarsimp simp add: uniform_limit_iff dist_norm norm_divide diff_divide_distrib [symmetric] divide_simps)
apply (rule_tac e1="e * d" in eventually_mono [OF uniform_limitD [OF ulim]])
apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
@@ -6389,7 +6389,7 @@
by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
have f_tends_cig: "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
proof (rule Lim_transform_eventually)
- show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w))
+ show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w))
= 2 * of_real pi * \<i> * f x w"
apply (rule eventually_mono [OF cont contour_integral_unique [OF Cauchy_integral_circlepath]])
using w\<open>0 < d\<close> d_def by auto
@@ -6507,7 +6507,7 @@
proof -
obtain r where "0 < r" and r: "cball z r \<subseteq> S"
and ul: "uniform_limit (cball z r) f g sequentially"
- using ulim_g [OF \<open>z \<in> S\<close>] by blast
+ using ulim_g [OF \<open>z \<in> S\<close>] by blast
have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r"
proof (intro eventuallyI conjI)
show "continuous_on (cball z r) (f x)" for x
@@ -6537,7 +6537,7 @@
proof -
obtain r where "0 < r" and r: "cball z r \<subseteq> S"
and ul: "uniform_limit (cball z r) f g sequentially"
- using ulim_g [OF \<open>z \<in> S\<close>] by blast
+ using ulim_g [OF \<open>z \<in> S\<close>] by blast
have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and>
(\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))"
proof (intro eventuallyI conjI ballI)
@@ -6555,7 +6555,7 @@
subsection\<open>On analytic functions defined by a series\<close>
-
+
lemma series_and_derivative_comparison:
fixes S :: "complex set"
assumes S: "open S"
@@ -6878,7 +6878,7 @@
have "isCont (\<lambda>z. if z = a then deriv f a else (f z - f a) / (z - a)) x"
if "dist a x < e" for x
proof (cases "x=a")
- case True
+ case True
then have "f field_differentiable at a"
using holfb \<open>0 < e\<close> holomorphic_on_imp_differentiable_at by auto
with True show ?thesis
@@ -6961,10 +6961,10 @@
\<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
shows "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on S" (is "?F analytic_on S")
unfolding analytic_on_def
-proof
+proof
fix x
assume "x \<in> S"
- with g obtain e where "0 < e" and e: "g holomorphic_on ball x e"
+ with g obtain e where "0 < e" and e: "g holomorphic_on ball x e"
by (auto simp add: analytic_on_def)
obtain d where "0 < d" and d: "\<And>w. w \<in> ball x d - {a} \<Longrightarrow> g w = (w - a) * f w"
using \<open>x \<in> S\<close> eq by blast
@@ -7279,7 +7279,7 @@
obtain k1 where "k1>0" and k1: "\<And>x'. norm (x' - x) \<le> k1 \<Longrightarrow> norm (deriv f x' - deriv f x) < e"
using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> U\<close>]]
by (metis UNIV_I dist_norm)
- obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U"
+ obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U"
by (blast intro: openE [OF \<open>open U\<close>] \<open>x \<in> U\<close>)
have neq: "norm ((f z' - f x') / (z' - x') - deriv f x) \<le> e"
if "z' \<noteq> x'" and less_k1: "norm (x'-x, z'-x) < k1" and less_k2: "norm (x'-x, z'-x) < k2"
@@ -7518,7 +7518,7 @@
then have wn0: "\<And>w. w \<notin> S \<Longrightarrow> winding_number p w = 0"
by (simp add: zero)
show ?thesis
- using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols
+ using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols
by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq)
qed
@@ -7579,7 +7579,7 @@
using valid_path_imp_path by blast
proposition holomorphic_logarithm_exists:
- assumes A: "convex A" "open A"
+ assumes A: "convex A" "open A"
and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
and z0: "z0 \<in> A"
obtains g where "g holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> exp (g x) = f x"
--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Jun 25 14:45:05 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Jun 25 14:06:50 2018 +0100
@@ -60,7 +60,7 @@
shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
proof (cases "Im z = 0 \<or> Re z = 0")
case True
- with assms abs_square_less_1 show ?thesis
+ with assms abs_square_less_1 show ?thesis
by (force simp add: Re_power2 Im_power2 cmod_def)
next
case False
@@ -210,7 +210,7 @@
lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
(is "?lhs = ?rhs")
-proof
+proof
assume "exp z = 1"
then have "Re z = 0"
by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
@@ -770,15 +770,15 @@
subsection\<open>The argument of a complex number\<close>
-definition Arg :: "complex \<Rightarrow> real" where
- "Arg z \<equiv> if z = 0 then 0
+definition Arg2pi :: "complex \<Rightarrow> real" where
+ "Arg2pi z \<equiv> if z = 0 then 0
else THE t. 0 \<le> t \<and> t < 2*pi \<and>
z = of_real(norm z) * exp(\<i> * of_real t)"
-lemma Arg_0 [simp]: "Arg(0) = 0"
- by (simp add: Arg_def)
-
-lemma Arg_unique_lemma:
+lemma Arg2pi_0 [simp]: "Arg2pi(0) = 0"
+ by (simp add: Arg2pi_def)
+
+lemma Arg2pi_unique_lemma:
assumes z: "z = of_real(norm z) * exp(\<i> * of_real t)"
and z': "z = of_real(norm z) * exp(\<i> * of_real t')"
and t: "0 \<le> t" "t < 2*pi"
@@ -803,10 +803,10 @@
by (simp add: n)
qed
-lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
+lemma Arg2pi: "0 \<le> Arg2pi z & Arg2pi z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
proof (cases "z=0")
case True then show ?thesis
- by (simp add: Arg_def)
+ by (simp add: Arg2pi_def)
next
case False
obtain t where t: "0 \<le> t" "t < 2*pi"
@@ -819,70 +819,70 @@
apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
done
show ?thesis
- apply (simp add: Arg_def False)
+ apply (simp add: Arg2pi_def False)
apply (rule theI [where a=t])
using t z False
- apply (auto intro: Arg_unique_lemma)
+ apply (auto intro: Arg2pi_unique_lemma)
done
qed
corollary
- shows Arg_ge_0: "0 \<le> Arg z"
- and Arg_lt_2pi: "Arg z < 2*pi"
- and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
- using Arg by auto
-
-lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
- by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
-
-lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
- by (rule Arg_unique_lemma [OF _ Arg_eq])
- (use Arg [of z] in \<open>auto simp: norm_mult\<close>)
-
-lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
- apply (rule Arg_unique [of "norm z"])
+ 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))"
+ using Arg2pi by auto
+
+lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg2pi z)) = z"
+ by (metis Arg2pi_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
+
+lemma Arg2pi_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg2pi z = a"
+ by (rule Arg2pi_unique_lemma [OF _ Arg2pi_eq])
+ (use Arg2pi [of z] in \<open>auto simp: norm_mult\<close>)
+
+lemma Arg2pi_minus: "z \<noteq> 0 \<Longrightarrow> Arg2pi (-z) = (if Arg2pi z < pi then Arg2pi z + pi else Arg2pi z - pi)"
+ apply (rule Arg2pi_unique [of "norm z"])
apply (rule complex_eqI)
- using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z]
+ using Arg2pi_ge_0 [of z] Arg2pi_eq [of z] Arg2pi_lt_2pi [of z]
apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
apply (metis Re_rcis Im_rcis rcis_def)+
done
-lemma Arg_times_of_real [simp]:
- assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
+lemma Arg2pi_times_of_real [simp]:
+ assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z"
proof (cases "z=0")
case False
show ?thesis
- by (rule Arg_unique [of "r * norm z"]) (use Arg False assms in auto)
+ by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms in auto)
qed auto
-lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
- by (metis Arg_times_of_real mult.commute)
-
-lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
- by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
-
-lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
+lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z"
+ by (metis Arg2pi_times_of_real mult.commute)
+
+lemma Arg2pi_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg2pi (z / of_real r) = Arg2pi z"
+ by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+
+lemma Arg2pi_le_pi: "Arg2pi z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
proof (cases "z=0")
case False
- have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
- by (metis Arg_eq)
- also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
+ have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+ by (metis Arg2pi_eq)
+ also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg2pi z))))"
using False by (simp add: zero_le_mult_iff)
- also have "... \<longleftrightarrow> Arg z \<le> pi"
- by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
+ also have "... \<longleftrightarrow> Arg2pi z \<le> pi"
+ by (simp add: Im_exp) (metis Arg2pi_ge_0 Arg2pi_lt_2pi sin_lt_zero sin_ge_zero not_le)
finally show ?thesis
by blast
qed auto
-lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
+lemma Arg2pi_lt_pi: "0 < Arg2pi z \<and> Arg2pi z < pi \<longleftrightarrow> 0 < Im z"
proof (cases "z=0")
case False
- have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
- by (metis Arg_eq)
- also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
+ have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+ by (metis Arg2pi_eq)
+ also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg2pi z))))"
using False by (simp add: zero_less_mult_iff)
- also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
- using Arg_ge_0 Arg_lt_2pi sin_le_zero sin_gt_zero
+ also have "... \<longleftrightarrow> 0 < Arg2pi z \<and> Arg2pi z < pi"
+ using Arg2pi_ge_0 Arg2pi_lt_2pi sin_le_zero sin_gt_zero
apply (auto simp: Im_exp)
using le_less apply fastforce
using not_le by blast
@@ -890,19 +890,19 @@
by blast
qed auto
-lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
+lemma Arg2pi_eq_0: "Arg2pi z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
proof (cases "z=0")
case False
- have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
- by (metis Arg_eq)
- also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
+ have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
+ by (metis Arg2pi_eq)
+ also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg2pi z)))"
using False by (simp add: zero_le_mult_iff)
- also have "... \<longleftrightarrow> Arg z = 0"
+ also have "... \<longleftrightarrow> Arg2pi z = 0"
proof -
- have [simp]: "Arg z = 0 \<Longrightarrow> z \<in> \<real>"
- using Arg_eq [of z] by (auto simp: Reals_def)
- moreover have "\<lbrakk>z \<in> \<real>; 0 \<le> cos (Arg z)\<rbrakk> \<Longrightarrow> Arg z = 0"
- by (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
+ have [simp]: "Arg2pi z = 0 \<Longrightarrow> z \<in> \<real>"
+ using Arg2pi_eq [of z] by (auto simp: Reals_def)
+ moreover have "\<lbrakk>z \<in> \<real>; 0 \<le> cos (Arg2pi z)\<rbrakk> \<Longrightarrow> Arg2pi z = 0"
+ by (metis Arg2pi_lt_pi Arg2pi_ge_0 Arg2pi_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
ultimately show ?thesis
by (auto simp: Re_exp)
qed
@@ -910,104 +910,104 @@
by blast
qed auto
-corollary Arg_gt_0:
+corollary Arg2pi_gt_0:
assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
- shows "Arg z > 0"
- using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
-
-lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
- by (simp add: Arg_eq_0)
-
-lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
- using Arg_eq_0 [of "-z"]
- by (metis Arg_eq_0 Arg_gt_0 Arg_le_pi Arg_lt_pi complex_is_Real_iff dual_order.order_iff_strict not_less pi_neq_zero)
-
-lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
- using Arg_eq_0 Arg_eq_pi not_le by auto
-
-lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+ shows "Arg2pi z > 0"
+ using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order by fastforce
+
+lemma Arg2pi_of_real: "Arg2pi(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
+ by (simp add: Arg2pi_eq_0)
+
+lemma Arg2pi_eq_pi: "Arg2pi z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
+ using Arg2pi_eq_0 [of "-z"]
+ by (metis Arg2pi_eq_0 Arg2pi_gt_0 Arg2pi_le_pi Arg2pi_lt_pi complex_is_Real_iff dual_order.order_iff_strict not_less pi_neq_zero)
+
+lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \<or> Arg2pi z = pi \<longleftrightarrow> z \<in> \<real>"
+ using Arg2pi_eq_0 Arg2pi_eq_pi not_le by auto
+
+lemma Arg2pi_inverse: "Arg2pi(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
proof (cases "z=0")
case False
show ?thesis
- apply (rule Arg_unique [of "inverse (norm z)"])
- using False Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z]
+ apply (rule Arg2pi_unique [of "inverse (norm z)"])
+ using False Arg2pi_ge_0 [of z] Arg2pi_lt_2pi [of z] Arg2pi_eq [of z] Arg2pi_eq_0 [of z]
apply (auto simp: exp_diff field_simps)
done
qed auto
-lemma Arg_eq_iff:
+lemma Arg2pi_eq_iff:
assumes "w \<noteq> 0" "z \<noteq> 0"
- shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
- using assms Arg_eq [of z] Arg_eq [of w]
+ shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
+ using assms Arg2pi_eq [of z] Arg2pi_eq [of w]
apply auto
apply (rule_tac x="norm w / norm z" in exI)
apply (simp add: divide_simps)
by (metis mult.commute mult.left_commute)
-lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
- by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq)
-
-lemma Arg_divide:
- assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
- shows "Arg(z / w) = Arg z - Arg w"
- apply (rule Arg_unique [of "norm(z / w)"])
- using assms Arg_eq Arg_ge_0 [of w] Arg_lt_2pi [of z]
+lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \<longleftrightarrow> Arg2pi z = 0"
+ by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq)
+
+lemma Arg2pi_divide:
+ assumes "w \<noteq> 0" "z \<noteq> 0" "Arg2pi w \<le> Arg2pi z"
+ shows "Arg2pi(z / w) = Arg2pi z - Arg2pi w"
+ apply (rule Arg2pi_unique [of "norm(z / w)"])
+ using assms Arg2pi_eq Arg2pi_ge_0 [of w] Arg2pi_lt_2pi [of z]
apply (auto simp: exp_diff norm_divide field_simps)
done
-lemma Arg_le_div_sum:
- assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
- shows "Arg z = Arg w + Arg(z / w)"
- by (simp add: Arg_divide assms)
-
-lemma Arg_le_div_sum_eq:
+lemma Arg2pi_le_div_sum:
+ assumes "w \<noteq> 0" "z \<noteq> 0" "Arg2pi w \<le> Arg2pi z"
+ shows "Arg2pi z = Arg2pi w + Arg2pi(z / w)"
+ by (simp add: Arg2pi_divide assms)
+
+lemma Arg2pi_le_div_sum_eq:
assumes "w \<noteq> 0" "z \<noteq> 0"
- shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
- using assms by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
-
-lemma Arg_diff:
+ shows "Arg2pi w \<le> Arg2pi z \<longleftrightarrow> Arg2pi z = Arg2pi w + Arg2pi(z / w)"
+ using assms by (auto simp: Arg2pi_ge_0 intro: Arg2pi_le_div_sum)
+
+lemma Arg2pi_diff:
assumes "w \<noteq> 0" "z \<noteq> 0"
- shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
- using assms Arg_divide Arg_inverse [of "w/z"]
- apply (clarsimp simp add: Arg_ge_0 Arg_divide not_le)
- by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
-
-lemma Arg_add:
+ shows "Arg2pi w - Arg2pi z = (if Arg2pi z \<le> Arg2pi w then Arg2pi(w / z) else Arg2pi(w/z) - 2*pi)"
+ using assms Arg2pi_divide Arg2pi_inverse [of "w/z"]
+ apply (clarsimp simp add: Arg2pi_ge_0 Arg2pi_divide not_le)
+ by (metis Arg2pi_eq_0 less_irrefl minus_diff_eq right_minus_eq)
+
+lemma Arg2pi_add:
assumes "w \<noteq> 0" "z \<noteq> 0"
- shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
- using assms Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
- apply (auto simp: Arg_ge_0 Arg_divide not_le)
- apply (metis Arg_lt_2pi add.commute)
- apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
+ shows "Arg2pi w + Arg2pi z = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi(w * z) else Arg2pi(w * z) + 2*pi)"
+ using assms Arg2pi_diff [of "w*z" z] Arg2pi_le_div_sum_eq [of z "w*z"]
+ apply (auto simp: Arg2pi_ge_0 Arg2pi_divide not_le)
+ apply (metis Arg2pi_lt_2pi add.commute)
+ apply (metis (no_types) Arg2pi add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
done
-lemma Arg_times:
+lemma Arg2pi_times:
assumes "w \<noteq> 0" "z \<noteq> 0"
- shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
- else (Arg w + Arg z) - 2*pi)"
- using Arg_add [OF assms]
+ shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z
+ else (Arg2pi w + Arg2pi z) - 2*pi)"
+ using Arg2pi_add [OF assms]
by auto
-lemma Arg_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg (cnj z) = Arg (inverse z)"
- apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
+lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)"
+ apply (simp add: Arg2pi_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
by (metis of_real_power zero_less_norm_iff zero_less_power)
-lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
proof (cases "z=0")
case False
then show ?thesis
- by (simp add: Arg_cnj_eq_inverse Arg_inverse)
+ by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)
qed auto
-lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
- using Arg_eq_0 Arg_eq_0_pi by auto
-
-lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
- by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
+lemma Arg2pi_real: "z \<in> \<real> \<Longrightarrow> Arg2pi z = (if 0 \<le> Re z then 0 else pi)"
+ using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto
+
+lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z"
+ by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
lemma complex_split_polar:
obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
- using Arg cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
+ using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
proof (cases w rule: complex_split_polar)
@@ -1108,10 +1108,10 @@
have "ln (exp 0) = (0::complex)"
by (simp add: del: exp_zero)
then show ?thesis
- by simp
+ by simp
qed
-
+
lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
@@ -1214,7 +1214,7 @@
lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S Ln"
by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
-lemma continuous_on_Ln' [continuous_intros]:
+lemma continuous_on_Ln' [continuous_intros]:
"continuous_on S f \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S (\<lambda>x. Ln (f x))"
by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto
@@ -1254,7 +1254,7 @@
using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
qed
qed
-
+
subsection\<open>Quadrant-type results for Ln\<close>
@@ -1367,7 +1367,7 @@
have "\<bar>Im (cnj (Ln z))\<bar> < pi"
by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
moreover have "\<bar>Im (Ln (cnj z))\<bar> \<le> pi"
- by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff False Im_Ln_le_pi mpi_less_Im_Ln)
+ by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff False Im_Ln_le_pi mpi_less_Im_Ln)
ultimately show ?thesis
by simp
qed
@@ -1375,7 +1375,7 @@
by simp
show "exp (cnj (Ln z)) = exp (Ln (cnj z))"
by (metis False complex_cnj_zero_iff exp_Ln exp_cnj)
- qed
+ qed
qed (use assms in auto)
@@ -1395,11 +1395,11 @@
ultimately show ?thesis
by simp
qed
- finally show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
+ finally show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
by simp
show "exp (Ln (inverse z)) = exp (- Ln z)"
by (simp add: False exp_minus)
- qed
+ qed
qed (use assms in auto)
lemma Ln_minus1 [simp]: "Ln(-1) = \<i> * pi"
@@ -1529,28 +1529,28 @@
using assms by (simp add: powr_def)
-subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
-
-lemma Arg_Ln:
- assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
+subsection\<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"
proof (cases "z = 0")
case True
with assms show ?thesis
by simp
next
case False
- then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
- using Arg [of z]
+ then have "z / of_real(norm z) = exp(\<i> * of_real(Arg2pi z))"
+ using Arg2pi [of z]
by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
- then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
+ then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg2pi z) - pi))"
using cis_conv_exp cis_pi
by (auto simp: exp_diff algebra_simps)
- then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
+ then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg2pi z) - pi)))"
by simp
- also have "... = \<i> * (of_real(Arg z) - pi)"
- using Arg [of z] assms pi_not_less_zero
+ also have "... = \<i> * (of_real(Arg2pi z) - pi)"
+ using Arg2pi [of z] assms pi_not_less_zero
by auto
- finally have "Arg z = Im (Ln (- z / of_real (cmod z))) + pi"
+ finally have "Arg2pi z = Im (Ln (- z / of_real (cmod z))) + pi"
by simp
also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
@@ -1559,23 +1559,23 @@
finally show ?thesis .
qed
-lemma continuous_at_Arg:
+lemma continuous_at_Arg2pi:
assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
- shows "continuous (at z) Arg"
+ shows "continuous (at z) Arg2pi"
proof -
have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
- have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
- using Arg_Ln Arg_gt_0 complex_is_Real_iff by auto
+ have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
+ using Arg2pi_Ln Arg2pi_gt_0 complex_is_Real_iff by auto
consider "Re z < 0" | "Im z \<noteq> 0" using assms
using complex_nonneg_Reals_iff not_le by blast
- then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg z"
- using "*" by (simp add: isCont_def) (metis Arg_Ln Arg_gt_0 complex_is_Real_iff)
+ then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
+ using "*" by (simp add: isCont_def) (metis Arg2pi_Ln Arg2pi_gt_0 complex_is_Real_iff)
show ?thesis
unfolding continuous_at
proof (rule Lim_transform_within_open)
- show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
- by (auto simp add: Arg_Ln [OF Arg_gt_0] complex_nonneg_Reals_iff)
+ show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
+ by (auto simp add: Arg2pi_Ln [OF Arg2pi_gt_0] complex_nonneg_Reals_iff)
qed (use assms in auto)
qed
@@ -1662,8 +1662,8 @@
(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))"
+ 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)
@@ -1678,14 +1678,14 @@
qed
-text\<open>Relation between Arg and arctangent in upper halfplane\<close>
-lemma Arg_arctan_upperhalf:
+text\<open>Relation between Arg2pi and arctangent in upper halfplane\<close>
+lemma Arg2pi_arctan_upperhalf:
assumes "0 < Im z"
- shows "Arg z = pi/2 - arctan(Re z / Im z)"
+ shows "Arg2pi z = pi/2 - arctan(Re z / Im z)"
proof (cases "z = 0")
case False
show ?thesis
- proof (rule Arg_unique [of "norm z"])
+ proof (rule Arg2pi_unique [of "norm z"])
show "(cmod z) * exp (\<i> * (pi / 2 - arctan (Re z / Im z))) = z"
apply (auto simp: exp_Euler cos_diff sin_diff)
using assms norm_complex_def [of z, symmetric]
@@ -1695,34 +1695,34 @@
qed (use False arctan [of "Re z / Im z"] in auto)
qed (use assms in auto)
-lemma Arg_eq_Im_Ln:
+lemma Arg2pi_eq_Im_Ln:
assumes "0 \<le> Im z" "0 < Re z"
- shows "Arg z = Im (Ln z)"
+ shows "Arg2pi z = Im (Ln z)"
proof (cases "Im z = 0")
case True then show ?thesis
- using Arg_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
+ using Arg2pi_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
next
case False
- then have *: "Arg z > 0"
- using Arg_gt_0 complex_is_Real_iff by blast
+ then have *: "Arg2pi z > 0"
+ using Arg2pi_gt_0 complex_is_Real_iff by blast
then have "z \<noteq> 0"
by auto
with * assms False show ?thesis
- by (subst Arg_Ln) (auto simp: Ln_minus)
+ by (subst Arg2pi_Ln) (auto simp: Ln_minus)
qed
-lemma continuous_within_upperhalf_Arg:
+lemma continuous_within_upperhalf_Arg2pi:
assumes "z \<noteq> 0"
- shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
+ shows "continuous (at z within {z. 0 \<le> Im z}) Arg2pi"
proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0")
case False then show ?thesis
- using continuous_at_Arg continuous_at_imp_continuous_within by auto
+ using continuous_at_Arg2pi continuous_at_imp_continuous_within by auto
next
case True
then have z: "z \<in> \<real>" "0 < Re z"
using assms by (auto simp: complex_nonneg_Reals_iff complex_is_Real_iff complex_neq_0)
- then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
- by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
+ then have [simp]: "Arg2pi z = 0" "Im (Ln z) = 0"
+ by (auto simp: Arg2pi_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
show ?thesis
proof (clarsimp simp add: continuous_within Lim_within dist_norm)
fix e::real
@@ -1739,50 +1739,50 @@
then have "0 < Re x"
using z by linarith
}
- then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg x\<bar> < e"
+ then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg2pi x\<bar> < e"
apply (rule_tac x="min d (Re z / 2)" in exI)
using z d
- apply (auto simp: Arg_eq_Im_Ln)
+ apply (auto simp: Arg2pi_eq_Im_Ln)
done
qed
qed
-lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
+lemma continuous_on_upperhalf_Arg2pi: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg2pi"
unfolding continuous_on_eq_continuous_within
- by (metis DiffE Diff_subset continuous_within_subset continuous_within_upperhalf_Arg insertCI)
-
-lemma open_Arg_less_Int:
+ by (metis DiffE Diff_subset continuous_within_subset continuous_within_upperhalf_Arg2pi insertCI)
+
+lemma open_Arg2pi2pi_less_Int:
assumes "0 \<le> s" "t \<le> 2*pi"
- shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
+ shows "open ({y. s < Arg2pi y} \<inter> {y. Arg2pi y < t})"
proof -
- have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg"
- using continuous_at_Arg continuous_at_imp_continuous_within
+ have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg2pi"
+ using continuous_at_Arg2pi continuous_at_imp_continuous_within
by (auto simp: continuous_on_eq_continuous_within)
have 2: "open (UNIV - \<real>\<^sub>\<ge>\<^sub>0 :: complex set)" by (simp add: open_Diff)
have "open ({z. s < z} \<inter> {z. z < t})"
using open_lessThan [of t] open_greaterThan [of s]
by (metis greaterThan_def lessThan_def open_Int)
- moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
- using assms by (auto simp: Arg_real complex_nonneg_Reals_iff complex_is_Real_iff)
+ moreover have "{y. s < Arg2pi y} \<inter> {y. Arg2pi y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
+ using assms by (auto simp: Arg2pi_real complex_nonneg_Reals_iff complex_is_Real_iff)
ultimately show ?thesis
using continuous_imp_open_vimage [OF 1 2, of "{z. Re z > s} \<inter> {z. Re z < t}"]
by auto
qed
-lemma open_Arg_gt: "open {z. t < Arg z}"
+lemma open_Arg2pi2pi_gt: "open {z. t < Arg2pi z}"
proof (cases "t < 0")
- case True then have "{z. t < Arg z} = UNIV"
- using Arg_ge_0 less_le_trans by auto
+ case True then have "{z. t < Arg2pi z} = UNIV"
+ using Arg2pi_ge_0 less_le_trans by auto
then show ?thesis
by simp
next
case False then show ?thesis
- using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
+ using open_Arg2pi2pi_less_Int [of t "2*pi"] Arg2pi_lt_2pi
by auto
qed
-lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
- using open_Arg_gt [of t]
+lemma closed_Arg2pi2pi_le: "closed {z. Arg2pi z \<le> t}"
+ using open_Arg2pi2pi_gt [of t]
by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
subsection\<open>Complex Powers\<close>
@@ -1890,7 +1890,7 @@
declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
lemma has_field_derivative_powr_of_int:
- fixes z :: complex
+ fixes z :: complex
assumes gderiv:"(g has_field_derivative gd) (at z within s)" and "g z\<noteq>0"
shows "((\<lambda>z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within s)"
proof -
@@ -1905,7 +1905,7 @@
case False
then have "n-1 \<ge>0" using \<open>n\<ge>0\<close> by auto
then have "g z powr (of_int (n - 1)) = g z ^ (nat n - 1)"
- using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] by (simp add: nat_diff_distrib')
+ using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] by (simp add: nat_diff_distrib')
then show ?thesis unfolding dd_def dd'_def by simp
qed (simp add:dd_def dd'_def)
then have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within s)
@@ -1958,7 +1958,7 @@
qed
lemma field_differentiable_powr_of_int:
- fixes z :: complex
+ fixes z :: complex
assumes gderiv:"g field_differentiable (at z within s)" and "g z\<noteq>0"
shows "(\<lambda>z. g z powr of_int n) field_differentiable (at z within s)"
using has_field_derivative_powr_of_int assms(2) field_differentiable_def gderiv by blast
@@ -1972,7 +1972,7 @@
apply (rule_tac holomorphic_cong)
using assms(2) by (auto simp add:powr_of_int)
moreover have "(\<lambda>z. (f z) ^ nat n) holomorphic_on s"
- using assms(1) by (auto intro:holomorphic_intros)
+ using assms(1) by (auto intro:holomorphic_intros)
ultimately show ?thesis by auto
next
case False
@@ -1980,7 +1980,7 @@
apply (rule_tac holomorphic_cong)
using assms(2) by (auto simp add:powr_of_int power_inverse)
moreover have "(\<lambda>z. inverse (f z) ^ nat (-n)) holomorphic_on s"
- using assms by (auto intro!:holomorphic_intros)
+ using assms by (auto intro!:holomorphic_intros)
ultimately show ?thesis by auto
qed
@@ -2194,7 +2194,7 @@
apply (auto simp: norm_divide norm_powr_real divide_simps)
apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
done
- then show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
+ then show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
by blast
qed
@@ -2504,7 +2504,7 @@
proof -
have nz0: "1 + \<i>*z \<noteq> 0"
using assms
- by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps
+ by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps
less_asym neg_equal_iff_equal)
have "z \<noteq> -\<i>" using assms
by auto
@@ -2847,7 +2847,7 @@
using arctan_bounds[of "1/5" 4]
arctan_bounds[of "1/239" 4]
by (simp_all add: eval_nat_numeral)
-
+
corollary pi_gt3: "pi > 3"
using pi_approx by simp
@@ -2987,7 +2987,7 @@
lemma has_field_derivative_Arcsin:
assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
-proof -
+proof -
have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
using assms one_minus_z2_notin_nonpos_Reals by force
then have "cos (Arcsin z) \<noteq> 0"
@@ -3682,8 +3682,8 @@
lemma homotopic_loops_imp_homotopic_circlemaps:
assumes "homotopic_loops S p q"
shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
- (p \<circ> (\<lambda>z. (Arg z / (2 * pi))))
- (q \<circ> (\<lambda>z. (Arg z / (2 * pi))))"
+ (p \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))
+ (q \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))"
proof -
obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
@@ -3693,41 +3693,41 @@
using assms
by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
define j where "j \<equiv> \<lambda>z. if 0 \<le> Im (snd z)
- then h (fst z, Arg (snd z) / (2 * pi))
- else h (fst z, 1 - Arg (cnj (snd z)) / (2 * pi))"
- have Arg_eq: "1 - Arg (cnj y) / (2 * pi) = Arg y / (2 * pi) \<or> Arg y = 0 \<and> Arg (cnj y) = 0" if "cmod y = 1" for y
- using that Arg_eq_0_pi Arg_eq_pi by (force simp: Arg_cnj divide_simps)
+ then h (fst z, Arg2pi (snd z) / (2 * pi))
+ else h (fst z, 1 - Arg2pi (cnj (snd z)) / (2 * pi))"
+ have Arg2pi_eq: "1 - Arg2pi (cnj y) / (2 * pi) = Arg2pi y / (2 * pi) \<or> Arg2pi y = 0 \<and> Arg2pi (cnj y) = 0" if "cmod y = 1" for y
+ using that Arg2pi_eq_0_pi Arg2pi_eq_pi by (force simp: Arg2pi_cnj divide_simps)
show ?thesis
proof (simp add: homotopic_with; intro conjI ballI exI)
- show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg (snd w) / (2 * pi)))"
+ show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi)))"
proof (rule continuous_on_eq)
- show j: "j x = h (fst x, Arg (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
- using Arg_eq that h01 by (force simp: j_def)
+ show j: "j x = h (fst x, Arg2pi (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
+ using Arg2pi_eq that h01 by (force simp: j_def)
have eq: "S = S \<inter> (UNIV \<times> {z. 0 \<le> Im z}) \<union> S \<inter> (UNIV \<times> {z. Im z \<le> 0})" for S :: "(real*complex)set"
by auto
- have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg (snd x) / (2 * pi)))"
- apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
- apply (auto simp: Arg)
- apply (meson Arg_lt_2pi linear not_le)
+ have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg2pi (snd x) / (2 * pi)))"
+ apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
+ apply (auto simp: Arg2pi)
+ apply (meson Arg2pi_lt_2pi linear not_le)
done
- have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg (cnj (snd x)) / (2 * pi)))"
- apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
- apply (auto simp: Arg)
- apply (meson Arg_lt_2pi linear not_le)
+ have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg2pi (cnj (snd x)) / (2 * pi)))"
+ apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
+ apply (auto simp: Arg2pi)
+ apply (meson Arg2pi_lt_2pi linear not_le)
done
show "continuous_on ({0..1} \<times> sphere 0 1) j"
apply (simp add: j_def)
apply (subst eq)
apply (rule continuous_on_cases_local)
apply (simp_all add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)
- using Arg_eq h01
+ using Arg2pi_eq h01
by force
qed
- have "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
- by (auto simp: Arg_ge_0 Arg_lt_2pi less_imp_le)
+ have "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
+ by (auto simp: Arg2pi_ge_0 Arg2pi_lt_2pi less_imp_le)
also have "... \<subseteq> S"
using him by blast
- finally show "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
+ finally show "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
qed (auto simp: h0 h1)
qed
@@ -3794,7 +3794,7 @@
assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
then have "homotopic_loops S p p"
by (simp add: homotopic_loops_refl)
- then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg z / (2 * pi))) (\<lambda>x. a)"
+ then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi))) (\<lambda>x. a)"
by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
proof (intro exI conjI)
@@ -3802,11 +3802,11 @@
using homotopic_with_imp_subset2 [OF homp]
by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
have teq: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk>
- \<Longrightarrow> t = Arg (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg (exp (2 * of_real pi * of_real t * \<i>)) = 0"
+ \<Longrightarrow> t = Arg2pi (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg2pi (exp (2 * of_real pi * of_real t * \<i>)) = 0"
apply (rule disjCI)
- using Arg_of_real [of 1] apply (auto simp: Arg_exp)
+ using Arg2pi_of_real [of 1] apply (auto simp: Arg2pi_exp)
done
- have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
+ have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
apply (rule homotopic_loops_eq [OF p])
using p teq apply (fastforce simp: pathfinish_def pathstart_def)
done
@@ -3855,45 +3855,45 @@
have "homotopic_loops (path_image \<gamma>) \<gamma> \<gamma>"
by (simp add: assms homotopic_loops_refl simple_path_imp_path)
then have hom: "homotopic_with (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
- (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
+ (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
by (rule homotopic_loops_imp_homotopic_circlemaps)
- have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) g"
+ have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) g"
proof (rule homeomorphism_compact)
- show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
+ show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
using hom homotopic_with_imp_continuous by blast
- show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (sphere 0 1)"
+ show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (sphere 0 1)"
proof
fix x y
assume xy: "x \<in> sphere 0 1" "y \<in> sphere 0 1"
- and eq: "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) y"
- then have "(Arg x / (2*pi)) = (Arg y / (2*pi))"
+ and eq: "(\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) y"
+ then have "(Arg2pi x / (2*pi)) = (Arg2pi y / (2*pi))"
proof -
- have "(Arg x / (2*pi)) \<in> {0..1}" "(Arg y / (2*pi)) \<in> {0..1}"
- using Arg_ge_0 Arg_lt_2pi dual_order.strict_iff_order by fastforce+
+ have "(Arg2pi x / (2*pi)) \<in> {0..1}" "(Arg2pi y / (2*pi)) \<in> {0..1}"
+ using Arg2pi_ge_0 Arg2pi_lt_2pi dual_order.strict_iff_order by fastforce+
with eq show ?thesis
- using \<open>simple_path \<gamma>\<close> Arg_lt_2pi unfolding simple_path_def o_def
+ using \<open>simple_path \<gamma>\<close> Arg2pi_lt_2pi unfolding simple_path_def o_def
by (metis eq_divide_eq_1 not_less_iff_gr_or_eq)
qed
with xy show "x = y"
- by (metis Arg Arg_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
+ by (metis Arg2pi Arg2pi_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
qed
- have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg z / (2*pi)) = \<gamma> x"
- by (metis Arg_ge_0 Arg_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
- moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
+ have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg2pi z / (2*pi)) = \<gamma> x"
+ by (metis Arg2pi_ge_0 Arg2pi_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
+ moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg2pi z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
proof (cases "x=1")
case True
then show ?thesis
apply (rule_tac x=1 in bexI)
- apply (metis loop Arg_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
+ apply (metis loop Arg2pi_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
done
next
case False
- then have *: "(Arg (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
- using that by (auto simp: Arg_exp divide_simps)
+ then have *: "(Arg2pi (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
+ using that by (auto simp: Arg2pi_exp divide_simps)
show ?thesis
by (rule_tac x="exp(\<i> * of_real(2*pi*x))" in bexI) (auto simp: *)
qed
- ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
+ ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
by (auto simp: path_image_def image_iff)
qed auto
then have "path_image \<gamma> homeomorphic sphere (0::complex) 1"