Theory Meromorphic_Forms_Valence_Formula
section ‹The valence formula for level 1 meromorphic forms›
theory Meromorphic_Forms_Valence_Formula
imports
"Winding_Number_Eval.Winding_Number_Eval"
"Path_Automation.Path_Automation"
Argument_Principle_Sparse
Detour_Calculus.Detour_Calculus
Modular_Forms
begin
text ‹
The following is an important ingedient in our evaluation of the integral in Theorem 2.4:
If a function has an isolated non-essential singularity at ‹u› and is not identically zero,
then consider the integral $\int_\gamma(\varepsilon) \frac{f'(w)}{f(w)}\,\text{d}w$ where
‹γ(ε)› is a circular arc with radius ‹ε› around ‹u› beginning at the angle
‹a(ε)› and ending at the angle ‹b(ε)›.
Assume that ‹a(ε) → a› and ‹b(ε) → b› as ‹ε → 0›.
Then as ‹ε → 0›, the value of that integral tends to ‹n (b - a) 𝗂›, where \<^term>‹n = zorder f u›.
This is in some sense a more precise version of the Argument Principle for circular paths:
The Residue Theorem would tell us in such a situation that the value of the integral will
tend to $2 i \pi n m$ for a circular path that winds ‹m› times around ‹u›
(where ‹m› is an integer). This proposition tells us that the same also holds for circular
paths that do not wind around ‹u› an integer number of times; i.e.\ ‹m› can be an arbitrary
real number.
›
proposition contour_integral_logderiv_part_circlepath_not_essential:
fixes f :: "complex ⇒ complex" and a b :: "real ⇒ real"
assumes "f meromorphic_on {u}"
assumes "eventually (λz. f z ≠ 0) (at u)"
assumes "(a ⤏ A) (at_right 0)" "(b ⤏ B) (at_right 0)"
assumes "K = (of_int (zorder f u) * (B - A)) *⇩R 𝗂"
defines "circ ≡ (λε. part_circlepath u ε (a ε) (b ε))"
shows "((λε. contour_integral (circ ε) (λz. deriv f z / f z)) ⤏ K) (at_right 0)"
proof -
note [tendsto_intros] = ‹(a ⤏ A) (at_right 0)› ‹(b ⤏ B) (at_right 0)›
note [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1
from assms(1) have iso: "isolated_singularity_at f u"
by (simp add: meromorphic_on_isolated_singularity)
from assms(1) obtain R1 where R1: "R1 > 0" "f analytic_on ball u R1 - {u}"
using iso unfolding isolated_singularity_at_def by blast
obtain R2 where R2: "R2 > 0" "⋀z. z ∈ ball u R2 - {u} ⟹ f z ≠ 0"
using ‹eventually (λz. f z ≠ 0) (at u)› unfolding eventually_at by (auto simp: dist_commute)
from R1(1) R2(1) obtain R where "R > 0" "R < R1" "R < R2"
using field_lbound_gt_zero by auto
have R: "R > 0" "f analytic_on cball u R - {u}" "⋀z. z ∈ cball u R - {u} ⟹ f z ≠ 0"
using R2 ‹R > 0› ‹R < R1› ‹R < R2› by (auto intro!: analytic_on_subset [OF R1(2)])
from assms(1) obtain F where F: "(λw. f (u + w)) has_laurent_expansion F"
by (auto simp: meromorphic_on_def)
have [simp]: "F ≠ 0"
using ‹eventually (λz. f z ≠ 0) (at u)› F
has_laurent_expansion_eventually_nonzero_iff[of f u F] by auto
define n where "n = zorder f u"
define G where "G = fls_base_factor_to_fps F"
define g where "g = (λz. if z = u then fps_nth G 0 else f z * (z - u) powi -n)"
define f' where "f' = (λz. of_int n * (z - u) powi (n - 1) * g z + (z - u) powi n * deriv g z)"
have f_eq: "f z = (z - u) powi n * g z" if z: "z ≠ u" for z
using z by (auto simp: g_def power_int_minus)
have n_eq: "n = fls_subdegree F"
using has_laurent_expansion_zorder[OF F] by (simp add: n_def)
have G: "(λw. g (u + w)) has_fps_expansion G"
unfolding g_def n_eq G_def using has_fps_expansion_fls_base_factor_to_fps[OF F]
by (auto cong: if_cong)
have g_ana [analytic_intros]: "g analytic_on cball u R"
proof -
obtain A where A: "open A" "cball u R - {u} ⊆ A" "f holomorphic_on A"
using R(2) unfolding analytic_on_holomorphic by blast
have "(λz. f z * (z - u) powi -n) holomorphic_on A - {u}"
by (intro holomorphic_intros holomorphic_on_subset [OF A(3)]) auto
also have "?this ⟷ g holomorphic_on A - {u}"
by (intro holomorphic_cong) (auto simp: g_def)
finally have "g analytic_on cball u R - {u}"
unfolding analytic_on_holomorphic using A by (intro exI[of _ "A-{u}"]) auto
moreover have "g analytic_on {u}"
using G has_fps_expansion_imp_analytic by blast
ultimately have "g analytic_on (cball u R - {u}) ∪ {u}"
by (subst analytic_on_Un) (auto simp: analytic_on_open)
also have "… = cball u R"
using R(1) by auto
finally show "g analytic_on cball u R" .
qed
have [derivative_intros]: "(g has_field_derivative deriv g z) (at z)" if "z ∈ cball u R" for z
proof -
obtain A where A: "open A" "cball u R ⊆ A" "g holomorphic_on A"
using g_ana unfolding analytic_on_holomorphic by blast
show ?thesis
by (rule holomorphic_derivI[of _ A]) (use A that in auto)
qed
have deriv_f_eq: "deriv f z = f' z" if "z ∈ ball u R - {u}" for z
proof (rule DERIV_imp_deriv)
have "((λz. (z - u) powi n * g z) has_field_derivative f' z) (at z)"
using that by (auto simp: f'_def intro!: derivative_eq_intros)
also have "?this ⟷ (f has_field_derivative f' z) (at z)"
proof (rule DERIV_cong_ev)
have "eventually (λw. w ∈ ball u R - {u}) (nhds z)"
by (intro eventually_nhds_in_open) (use that in auto)
thus "eventually (λw. (w - u) powi n * g w = f w) (nhds z)"
by eventually_elim (auto simp: g_def power_int_minus)
qed auto
finally show "(f has_field_derivative f' z) (at z)" .
qed
have "g u = fps_nth G 0"
by (simp add: g_def)
also have "… ≠ 0"
unfolding G_def using ‹F ≠ 0› fls_base_factor_to_fps_base by blast
finally have g_nz: "g z ≠ 0" if "z ∈ cball u R" for z
using that R(3)[of z] by (auto simp: g_def)
define h where "h = (λz. deriv g z / g z)"
have h_ana: "h analytic_on cball u R"
unfolding h_def by (intro analytic_intros g_nz) auto
hence "continuous_on (cball u R) h"
by (intro analytic_imp_holomorphic holomorphic_on_imp_continuous_on)
hence "compact (h ` cball u R)"
by (intro compact_continuous_image) auto
hence "bounded (h ` cball u R)"
by (rule compact_imp_bounded)
then obtain C where C: "⋀z. z ∈ cball u R ⟹ norm (h z) ≤ C"
unfolding bounded_iff by (auto simp: cball_def)
have "0 ≤ norm (h u)"
by simp
also have "… ≤ C"
by (intro C) (use ‹R > 0› in auto)
finally have "C ≥ 0" .
define result where "result = (λε. of_int n * (𝗂 * (b ε - a ε)))"
define err where "err = (λε. contour_integral (circ ε) h)"
have int_err: "(h has_contour_integral err ε) (circ ε)" if ε: "ε ∈ {0<..<R}" for ε
unfolding err_def circ_def
by (rule has_contour_integral_integral, rule analytic_imp_contour_integrable)
(use ε in ‹auto intro!: analytic_on_subset [OF h_ana]
simp: path_image_part_circlepath' dist_norm norm_mult›)
show ?thesis
proof (rule Lim_transform_eventually)
have "eventually (λε. ε ∈ {0<..<R}) (at_right 0)"
using ‹R > 0› eventually_at_right_real by blast
thus "eventually (λε. result ε + err ε = contour_integral (circ ε) (λz. deriv f z / f z))
(at_right 0)"
proof eventually_elim
case ε: (elim ε)
have "u ∉ path_image (circ ε)"
using ε by (auto simp: circ_def path_image_part_circlepath')
hence "((λw. 1 / (w - u)) has_contour_integral 𝗂 * (b ε - a ε)) (circ ε)"
using has_contour_integral_winding_number[of "circ ε" u] ε
winding_number_part_circlepath_centre[of ε u "a ε" "b ε"]
by (simp_all add: circ_def)
hence "((λw. of_int n * (1 / (w - u))) has_contour_integral result ε) (circ ε)"
unfolding result_def by (rule has_contour_integral_lmul)
hence "((λw. of_int n / (w - u) + h w) has_contour_integral (result ε + err ε)) (circ ε)"
using ε by (intro has_contour_integral_add int_err) simp_all
hence "contour_integral (circ ε) (λw. of_int n / (w - u) + h w) = result ε + err ε"
using contour_integral_unique by blast
also have "contour_integral (circ ε) (λw. of_int n / (w - u) + h w) =
contour_integral (circ ε) (λw. deriv f w / f w)"
proof (intro contour_integral_cong refl)
fix w assume "w ∈ path_image (circ ε)"
hence w: "w ∈ ball u R - {u}"
using ε by (auto simp: circ_def path_image_part_circlepath' dist_norm)
thus "of_int n / (w - u) + h w = deriv f w / f w"
using g_nz by (auto simp: h_def deriv_f_eq f_eq f'_def field_simps power_int_diff)
qed
finally show ?case ..
qed
next
have [tendsto_intros]: "(err ⤏ 0) (at_right 0)"
proof (rule Lim_null_comparison)
have "eventually (λε. ε ∈ {0<..<R}) (at_right 0)"
using ‹R > 0› eventually_at_right_real by blast
thus "eventually (λε. norm (err ε) ≤ C * ε * ¦b ε - a ε¦) (at_right 0)"
proof eventually_elim
case ε: (elim ε)
show "norm (err ε) ≤ C * ε * ¦b ε - a ε¦"
unfolding err_def circ_def
proof (rule contour_integral_bound_part_circlepath)
show "norm (h z) ≤ C" if "z ∈ path_image (part_circlepath u ε (a ε) (b ε))" for z
using that ε by (intro C) (auto simp: path_image_part_circlepath' dist_norm)
show "h contour_integrable_on part_circlepath u ε (a ε) (b ε)"
by (intro analytic_imp_contour_integrable analytic_intros
analytic_on_subset [OF h_ana])
(use ε in ‹auto simp: path_image_part_circlepath' dist_norm›)
qed (use ‹C ≥ 0› ε C in auto)
qed
next
show "((λε. C * ε * ¦b ε - a ε¦) ⤏ 0) (at_right 0)"
by (auto intro!: tendsto_eq_intros)
qed
have [tendsto_intros]: "(result ⤏ (of_int n * (B - A)) *⇩R 𝗂) (at_right 0)"
unfolding result_def by (auto intro!: tendsto_eq_intros simp: scaleR_conv_of_real)
show "((λε. result ε + err ε) ⤏ K) (at_right 0)"
by (auto intro!: tendsto_eq_intros simp: scaleR_conv_of_real n_def ‹K = _›)
qed
qed
lemma winding_preserving_inverse_upper_halfspace:
assumes "A ⊆ {z. Im z > 0}"
shows "winding_preserving A inverse (λx. x)"
proof
show "inj_on inverse A"
using assms by (auto simp: inj_on_def)
show "continuous_on A inverse"
using assms by (auto intro!: continuous_intros)
next
fix p z assume p: "path p" "path_image p ⊆ A" "pathstart p = pathfinish p"
assume z: "z ∈ A - path_image p"
have "winding_number (inverse ∘ p) (inverse z) = winding_number p z - winding_number p 0"
using p z assms by (subst winding_number_inverse) auto
also have "winding_number p 0 = 0"
using assms p z
by (intro winding_number_zero_outside[of _ "{z. Im z > 0}"])
(auto simp: convex_halfspace_Im_gt)
finally show "winding_number (inverse ∘ p) (inverse z) = winding_number p z"
by (simp add: o_def)
qed
lemmas [simp del] = pathstart_part_circlepath pathfinish_part_circlepath
text ‹
This is the contour around the fundamental region \<^term>‹ℛ⇩Γ› that we want to integrate on.
Unfortunately, since there may be roots and zeros on the contour, we will have to deform
it slightly later. But for now, we will show the basic properties of this contour: it is
a positively oriented (i.e.\ counter-clockwise) simple closed curve that contains all points
in \<^term>‹ℛ⇩Γ› with imaginary part ‹< b›, and it does not contain any points outside the
closure of \<^term>‹ℛ⇩Γ›.
›
definition mypath :: "real ⇒ real ⇒ complex" where
"mypath b = part_circlepath 0 1 (2/3*pi) (1/3*pi) +++
linepath (❙ρ + 1) (1 / 2 + b *⇩R 𝗂) +++
linepath (1 / 2 + b *⇩R 𝗂) (-1 / 2 + b *⇩R 𝗂) +++
linepath (-1 / 2 + b *⇩R 𝗂) ❙ρ"
lemma mypath_ends: "cis (pi / 3) = ❙ρ + 1" "cis (2 * pi / 3) = ❙ρ"
unfolding modfun_rho_altdef by (simp_all add: complex_eq_iff cos_60 cos_120 sin_60 sin_120)
lemma path_mypath [simp, intro]: "path (mypath b)"
and valid_path_mypath [simp, intro]: "valid_path (mypath b)"
and closed_mypath: "pathstart (mypath b) = pathfinish (mypath b)"
unfolding mypath_def
by (simp_all add: rcis_def mypath_ends pathfinish_part_circlepath' pathstart_part_circlepath')
lemma sin_not_gt_one [simp]: "¬sin (x :: real) > 1"
using sin_le_one[of x] by linarith
lemma cos_not_gt_one [simp]: "¬cos (x :: real) > 1"
using cos_le_one[of x] by linarith
lemma simple_path_mypath [simp, intro]:
assumes "b > 1"
shows "simple_path (mypath b)"
proof -
have "sqrt 3 ≤ 2"
by (rule real_le_lsqrt) auto
hence b: "b > sqrt 3 / 2"
using assms by linarith
note [simp] = mypath_ends closed_segment_same_Re closed_segment_same_Im
closed_segment_eq_real_ivl rcis_def cos_60 cos_120
show ?thesis
unfolding mypath_def
using [[goals_limit = 20]]
proof path
show "path_image (part_circlepath 0 1 (2 / 3 * pi) (1 / 3 * pi)) ∩
closed_segment (❙ρ + 1) (1 / 2 + b *⇩R 𝗂) ⊆ {rcis 1 (1 / 3 * pi)}" (is "?A ⊆ ?B")
proof
fix z assume "z ∈ ?A"
then obtain t where t: "cos t = cos (pi / 3)" "t ∈ {pi/3..2*pi/3}" "z = cis t"
using b by (auto simp: path_image_part_circlepath' complex_eq_iff)
have [simp]: "t = pi / 3"
by (rule cos_inj_pi) (use t in auto)
show "z ∈ ?B"
using t by auto
qed
next
show "path_image (part_circlepath 0 1 (2 / 3 * pi) (1 / 3 * pi)) ∩
closed_segment (- 1 / 2 + b *⇩R 𝗂) ❙ρ ⊆ {rcis 1 (2 / 3 * pi)} ∩ {❙ρ}" (is "?A ⊆ ?B")
proof
fix z assume "z ∈ ?A"
then obtain t where t: "cos t = cos (2 * pi / 3)" "t ∈ {pi/3..2*pi/3}" "z = cis t"
using b by (auto simp: path_image_part_circlepath' complex_eq_iff)
have [simp]: "t = 2 * pi / 3"
by (rule cos_inj_pi) (use t in auto)
show "z ∈ ?B"
using t by auto
qed
qed (use assms b in ‹auto simp: path_image_part_circlepath' complex_eq_iff›)
qed
lemma simple_loop_mypath [simp, intro]: "b > 1 ⟹ simple_loop (mypath b)"
by (auto simp: simple_loop_def closed_mypath)
lemma path_image_mypath:
assumes "b > sqrt 3 / 2"
shows "path_image (mypath b) =
{z. norm z = 1 ∧ Im z > 0 ∧ ¦Re z¦ ≤ 1 / 2} ∪
{z. Im z = b ∧ ¦Re z¦ ≤ 1 / 2} ∪
{z. ¦Re z¦ = 1 / 2 ∧ Im z ∈ {sqrt 3 / 2..b}}"
proof -
have "path_image (mypath b) =
path_image (part_circlepath 0 1 (2 * pi / 3) (pi / 3)) ∪
{z. Im z = b ∧ Re z ∈ {-1/2..1/2}} ∪
({z. Re z = 1 / 2 ∧ Im z ∈ {sqrt 3 / 2..b}} ∪
{z. Re z = - (1 / 2) ∧ Im z ∈ {sqrt 3 / 2..b}})" (is "_ = ?A ∪ ?B ∪ ?C")
using assms
by (simp add: mypath_def path_image_join mypath_ends rcis_def Un_ac
closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl
pathfinish_part_circlepath')
also have "?B = {z. Im z = b ∧ ¦Re z¦ ≤ 1 / 2}"
by auto
also have "?C = {z. ¦Re z¦ = 1 / 2 ∧ Im z ∈ {sqrt 3 / 2..b}}"
by auto
also have "?A = {z. norm z = 1 ∧ Im z > 0 ∧ ¦Re z¦ ≤ 1 / 2}"
proof safe
fix z assume "z ∈ ?A"
then obtain t where t: "t ∈ {pi/3..2*pi/3}" "z = cis t"
by (auto simp: path_image_part_circlepath' closed_segment_eq_real_ivl rcis_def)
show "norm z = 1"
by (simp add: t)
have "t > 0"
by (rule less_le_trans[of _ "pi / 3"]) (use t(1) in auto)
have "t < pi"
by (rule le_less_trans[of _ "2 * pi / 3"]) (use t(1) in auto)
show "Im z > 0" using ‹t > 0› ‹t < pi›
by (auto simp: t intro!: sin_gt_zero)
have "cos t ≤ cos (pi / 3)" "cos t ≥ cos (2 * pi / 3)"
by (subst cos_mono_le_eq; use t in simp; fail)+
thus "¦Re z¦ ≤ 1 / 2"
by (auto simp: t cos_60 cos_120)
next
fix z assume z: "norm z = 1" "Im z > 0" "¦Re z¦ ≤ 1 / 2"
have "cos (2 * pi / 3) ≤ cos (Arg z)"
using z by (subst cos_Arg) (auto simp: cos_120 cos_60 divide_simps)
hence "Arg z ≤ 2 * pi / 3"
using z by (subst (asm) cos_mono_le_eq) (auto simp: Arg_less_0 Arg_le_pi)
moreover have "cos (pi / 3) ≥ cos (Arg z)"
using z by (subst cos_Arg) (auto simp: cos_120 cos_60 divide_simps)
hence "Arg z ≥ pi / 3"
using z by (subst (asm) cos_mono_le_eq) (auto simp: Arg_less_0 Arg_le_pi)
ultimately have "Arg z ∈ {pi/3..2*pi/3}"
by auto
moreover have "cis (Arg z) = z"
using z by (subst cis_Arg) (auto simp: complex_sgn_def)
ultimately show "z ∈ path_image (part_circlepath 0 1 (2 * pi / 3) (pi / 3))"
by (subst path_image_part_circlepath) (auto simp: closed_segment_eq_real_ivl ‹norm z = 1›)
qed
finally show ?thesis .
qed
lemma path_image_mypath_subset:
assumes "b > 1"
shows "path_image (mypath b) ⊆ closure ℛ⇩Γ ∩ {z. Im z ≤ b}"
proof -
have "sqrt 3 < 2"
by (rule real_less_lsqrt) auto
have *: "sqrt 3 / 2 < b"
by (rule less_trans[OF _ ‹b > 1›]) (use ‹sqrt 3 < 2› in auto)
have "b > 0"
by (rule le_less_trans[OF _ assms]) auto
have **: "x ∈ {-1/2..1/2} ⟷ ¦x¦ ≤ 1 / 2" for x :: real
by auto
show ?thesis
unfolding path_image_mypath[OF *] **
proof (intro Un_least subsetI)
fix z assume z: "z ∈ {z. Im z = b ∧ ¦Re z¦ ≤ 1 / 2}"
have "1 < ¦Im z¦"
using z assms by simp
also have "… ≤ norm z"
by (rule abs_Im_le_cmod)
finally have "norm z > 1" .
thus "z ∈ closure ℛ⇩Γ ∩ {z. Im z ≤ b}"
using z ‹b > 0› by (auto simp: closure_std_fund_region)
next
fix z assume z: "z ∈ {z. ¦Re z¦ = 1 / 2 ∧ Im z ∈ {sqrt 3 / 2..b}}"
have "0 ≤ sqrt 3 / 2"
by simp
also have "… ≤ Im z"
using z by auto
finally have "Im z ≥ 0" .
have "1 = (1 / 2) ^ 2 + (sqrt 3 / 2) ^ 2"
by (simp add: power_divide)
also have "… ≤ norm z ^ 2"
unfolding cmod_power2 by (intro add_mono power2_mono) (use z in auto)
finally have "norm z ≥ 1"
by (simp add: power2_nonneg_ge_1_iff)
thus "z ∈ closure ℛ⇩Γ ∩ {z. Im z ≤ b}"
using z ‹b > 1› ‹Im z ≥ 0› by (auto simp: closure_std_fund_region)
next
fix z assume z: "z ∈ {z. cmod z = 1 ∧ 0 < Im z ∧ ¦Re z¦ ≤ 1 / 2}"
have "Im z ≤ norm z"
using abs_Im_le_cmod abs_le_iff by blast
also have "… = 1"
using z by auto
also have "… < b"
by fact
finally show "z ∈ closure ℛ⇩Γ ∩ {z. Im z ≤ b}"
using z by (auto simp: closure_std_fund_region)
qed
qed
lemma path_image_mypath_superset_frontier:
assumes "b > sqrt 3 / 2"
shows "frontier ℛ⇩Γ ∩ {z. Im z ≤ b} ⊆ path_image (mypath b)"
unfolding frontier_std_fund_region Int_Un_distrib2
proof (intro Un_least subsetI)
fix z assume z: "z ∈ {z. cmod z = 1 ∧ 0 < Im z ∧ ¦Re z¦ ≤ 1 / 2} ∩ {z. Im z ≤ b}"
thus "z ∈ path_image (mypath b)"
unfolding path_image_mypath[OF assms] by auto
next
fix z assume z: "z ∈ {z. 1 ≤ cmod z ∧ 0 < Im z ∧ ¦Re z¦ = 1 / 2} ∩ {z. Im z ≤ b}"
hence "1 ≤ norm z ^ 2"
by auto
also have "… = ¦Re z¦ ^ 2 + Im z ^ 2"
unfolding cmod_power2 by simp
also have "¦Re z¦ = 1 / 2"
using z by auto
finally have "Im z ^ 2 ≥ 3 / 4"
by (auto simp: field_simps simp del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
hence "2 * Im z ≥ sqrt 3"
using z by (intro real_le_lsqrt) (auto simp: field_simps)
thus "z ∈ path_image (mypath b)"
using z unfolding path_image_mypath[OF assms] by (intro UnI2) auto
qed
lemma frontier_subset_path_image_mypath:
assumes "b > 1"
shows "path_image (mypath b) ⊆ frontier ℛ⇩Γ ∩ {z. Im z ≤ b} ∪
closed_segment (-1/2 + b *⇩R 𝗂) (1/2 + b *⇩R 𝗂)" (is "_ ⊆ ?rhs")
proof -
have "sqrt 3 < 2"
by (rule real_less_lsqrt) auto
have *: "sqrt 3 / 2 < b"
by (rule less_trans[OF _ ‹b > 1›]) (use ‹sqrt 3 < 2› in auto)
show ?thesis
unfolding path_image_mypath[OF *]
proof (intro Un_least subsetI)
fix z assume z: "z ∈ {z. cmod z = 1 ∧ 0 < Im z ∧ ¦Re z¦ ≤ 1 / 2}"
have "Im z ≤ norm z"
using abs_Im_le_cmod abs_le_iff by blast
also have "… = 1"
using z by auto
also have "… < b"
using assms by auto
finally show "z ∈ ?rhs"
using z unfolding frontier_std_fund_region by (intro UnI1) auto
next
fix z assume z: "z ∈ {z. Im z = b ∧ ¦Re z¦ ≤ 1 / 2}"
thus "z ∈ ?rhs"
by (intro UnI2)
(auto simp: frontier_std_fund_region closed_segment_same_Im closed_segment_eq_real_ivl)
next
fix z assume z: "z ∈ {z. ¦Re z¦ = 1 / 2 ∧ Im z ∈ {sqrt 3 / 2..b}}"
have "0 < sqrt 3 / 2"
by simp
also have "… ≤ Im z"
using z by auto
finally have "Im z > 0" .
have "1 = (1 / 2) ^ 2 + (sqrt 3 / 2) ^ 2"
by (simp add: field_simps)
also have "… ≤ ¦Re z¦ ^ 2 + Im z ^ 2"
by (intro add_mono power2_mono) (use z ‹Im z > 0› in auto)
finally have "norm z ^ 2 ≥ 1"
unfolding cmod_power2 by simp
thus "z ∈ ?rhs"
using z ‹Im z > 0› unfolding frontier_std_fund_region
by (intro UnI1) (auto simp: frontier_std_fund_region power2_nonneg_ge_1_iff)
qed
qed
lemma path_image_mypath_conv_frontier:
assumes "b > 1"
shows "path_image (mypath b) =
frontier ℛ⇩Γ ∩ {z. Im z ≤ b} ∪ closed_segment (-1/2 + b *⇩R 𝗂) (1/2 + b *⇩R 𝗂)"
proof -
have "sqrt 3 < 2"
by (rule real_less_lsqrt) auto
have *: "sqrt 3 / 2 < b"
by (rule less_trans[OF _ ‹b > 1›]) (use ‹sqrt 3 < 2› in auto)
have "closed_segment (- 1 / 2 + b *⇩R 𝗂) (1 / 2 + b *⇩R 𝗂) ⊆ path_image (mypath b)"
unfolding path_image_mypath[OF *]
by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl)
thus ?thesis
using frontier_subset_path_image_mypath[OF assms] path_image_mypath_superset_frontier[OF *]
by blast
qed
lemma winding_number_mypath_inside:
assumes "z ∈ ℛ⇩Γ" "Im z < b" "b > 1"
shows "winding_number (mypath b) z = 1"
proof -
note [simp] = closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl
rcis_def mypath_ends cos_60 cos_120 sin_60 sin_120 in_std_fund_region_iff
path_image_part_circlepath' sin_arccos Let_def jumpF_pathstart_part_circlepath
jumpF_pathfinish_part_circlepath
have 1: "arccos (1/2) < arccos (Re z)"
by (intro arccos_less_arccos) (use assms in auto)
have 2: "arccos (-1/2) > arccos (Re z)"
by (intro arccos_less_arccos) (use assms in auto)
hence 3: "Im z > sqrt (1 - (Re z)⇧2)"
proof -
have "norm z ^ 2 > 1"
using assms by simp
hence "Im z ^ 2 > 1 - Re z ^ 2"
unfolding cmod_power2 by linarith
hence "sqrt (Im z ^ 2) > sqrt (1 - Re z ^ 2)"
by (subst real_sqrt_less_iff)
also have "sqrt (Im z ^ 2) = Im z"
using assms by simp
finally show ?thesis .
qed
have part1: "cindex_pathE (linepath (❙ρ + 1) (1 / 2 + b *⇩R 𝗂)) z = 0"
and part2: "cindex_pathE (linepath (1 / 2 + b *⇩R 𝗂) (- 1 / 2 + b *⇩R 𝗂)) z = -1"
and part3: "cindex_pathE (linepath (- 1 / 2 + b *⇩R 𝗂) ❙ρ) z = 0"
by (subst cindex_pathE_linepath; use assms in simp; fail)+
have "cindex_pathE (part_circlepath 0 1 (2 / 3 * pi) (1 / 3 * pi)) z =
-cindex_pathE (part_circlepath 0 1 (1 / 3 * pi) (2 / 3 * pi)) z"
by (subst cindex_pathE_reversepath', subst reversepath_part_circlepath) (rule refl)
also have "… = -1"
by (subst cindex_pathE_part_circlepath) (use assms 1 2 3 in auto)
finally have part4: "cindex_pathE (part_circlepath 0 1 (2 / 3 * pi) (1 / 3 * pi)) z = -1" .
show ?thesis
unfolding mypath_def
by eval_winding
(use assms part1 part2 part3 part4
in ‹auto simp: pathstart_part_circlepath' pathfinish_part_circlepath'›)
qed
lemma simple_loop_ccw_mypath:
assumes "b > 1"
shows "simple_loop_ccw (mypath b)"
proof -
have "sqrt 3 < 2"
by (rule real_less_lsqrt) auto
have *: "sqrt 3 / 2 < b"
by (rule less_trans[OF _ ‹b > 1›]) (use ‹sqrt 3 < 2› in auto)
from assms obtain y where y: "1 < y" "y < b"
using dense by blast
define z where "z = y *⇩R 𝗂"
have z: "z ∈ ℛ⇩Γ" "Im z < b" using assms y
by (auto simp: in_std_fund_region_iff z_def)
hence "winding_number (mypath b) z = 1"
using assms z by (intro winding_number_mypath_inside)
moreover have "z ∉ path_image (mypath b)"
using y * by (subst path_image_mypath) (auto simp: z_def)
ultimately show ?thesis using assms
by (intro simple_loop_ccwI[of _ z]) auto
qed
lemma simple_loop_orientation_mypath [simp]:
assumes "b > 1"
shows "simple_loop_orientation (mypath b) = 1"
using simple_loop_ccw_mypath[OF assms]
unfolding simple_loop_orientation_def by auto
lemma winding_number_mypath_outside:
assumes "z ∉ closure ℛ⇩Γ ∩ {z. Im z ≤ b}" "b > 1"
shows "winding_number (mypath b) z = 0"
proof -
consider "z ∉ closure ℛ⇩Γ" | "z ∈ closure ℛ⇩Γ" "Im z > b"
using assms(1) by force
thus ?thesis
proof cases
assume z: "z ∉ closure ℛ⇩Γ"
show ?thesis
proof (rule simply_connected_imp_winding_number_zero)
show "simply_connected (closure ℛ⇩Γ)"
by (fact simply_connected_closure_std_fund_region)
show "path_image (mypath b) ⊆ closure ℛ⇩Γ"
using path_image_mypath_subset[of b] assms by blast
qed (use z in ‹auto simp: closed_mypath›)
next
assume z: "z ∈ closure ℛ⇩Γ" "Im z > b"
have "sqrt 3 < 2"
by (rule real_less_lsqrt) auto
have *: "sqrt 3 / 2 < b"
by (rule less_trans[OF _ ‹b > 1›]) (use ‹sqrt 3 < 2› in auto)
show ?thesis
proof (rule winding_number_zero_outside)
show "path_image (mypath b) ⊆ cbox (-1/2) (1/2 + b *⇩R 𝗂)"
using path_image_mypath_subset[OF assms(2)]
by (auto simp: in_cbox_complex_iff closure_std_fund_region)
show "z ∉ cbox (- 1 / 2) (1 / 2 + b *⇩R 𝗂)"
using z by (auto simp: in_cbox_complex_iff)
qed (use assms in ‹auto simp: closed_mypath in_cbox_complex_iff›)
qed
qed
lemma inside_mypath:
assumes "b > 1"
shows "inside (path_image (mypath b)) = ℛ⇩Γ ∩ {z. Im z < b}"
proof -
have "sqrt 3 < 2"
by (rule real_less_lsqrt) auto
have *: "sqrt 3 / 2 < b"
by (rule less_trans[OF _ ‹b > 1›]) (use ‹sqrt 3 < 2› in auto)
show ?thesis
proof (intro equalityI subsetI)
fix z assume z: "z ∈ inside (path_image (mypath b))"
hence ind: "norm (winding_number (mypath b) z) = 1"
using assms simple_closed_path_norm_winding_number_inside simple_path_mypath by blast
from z have z': "z ∉ path_image (mypath b)"
by (simp add: inside_outside)
show "z ∈ ℛ⇩Γ ∩ {z. Im z < b}"
proof (rule ccontr)
assume z: "z ∉ ℛ⇩Γ ∩ {z. Im z < b}"
moreover have "z ∉ frontier ℛ⇩Γ ∩ {z. Im z ≤ b}"
using path_image_mypath_superset_frontier[OF *] z' by auto
ultimately have "z ∉ (ℛ⇩Γ ∪ frontier ℛ⇩Γ) ∩ {z. Im z ≤ b}" using z'
unfolding frontier_std_fund_region std_fund_region_def path_image_mypath[OF *] by force
also have "ℛ⇩Γ ∪ frontier ℛ⇩Γ = closure ℛ⇩Γ"
by (simp add: closure_Un_frontier)
finally have "winding_number (mypath b) z = 0"
by (intro winding_number_mypath_outside) (use assms in auto)
with ind show False
by simp
qed
next
fix z assume z: "z ∈ ℛ⇩Γ ∩ {z. Im z < b}"
hence "winding_number (mypath b) z = 1"
by (intro winding_number_mypath_inside) (use assms in auto)
moreover have "z ∉ path_image (mypath b)"
unfolding path_image_mypath_conv_frontier[OF assms] frontier_std_fund_region using z
by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl in_std_fund_region_iff)
ultimately show "z ∈ inside (path_image (mypath b))"
using simple_loop_winding_number_cases[OF simple_loop_mypath[OF assms], of z]
by (auto split: if_splits)
qed
qed
lemma outside_mypath:
assumes "b > 1"
shows "outside (path_image (mypath b)) = -(closure ℛ⇩Γ ∩ {z. Im z ≤ b})"
proof -
define L where "L = closed_segment (- 1 / 2 + b *⇩R 𝗂) (1 / 2 + b *⇩R 𝗂)"
have "outside (path_image (mypath b)) = - (path_image (mypath b) ∪ ℛ⇩Γ ∩ {z. Im z < b})"
unfolding outside_inside inside_mypath[OF assms] ..
also have "… = -((frontier ℛ⇩Γ ∩ {z. Im z ≤ b}) ∪ L ∪ (ℛ⇩Γ ∩ {z. Im z < b}))"
unfolding path_image_mypath_conv_frontier[OF assms] L_def ..
also have "x ∈ frontier ℛ⇩Γ" if "x ∉ L" "x ∈ ℛ⇩Γ" "b = Im x" for x
using that unfolding L_def frontier_std_fund_region
by (auto simp: in_std_fund_region_iff closed_segment_same_Im closed_segment_eq_real_ivl)
hence "((frontier ℛ⇩Γ ∩ {z. Im z ≤ b}) ∪ L ∪ (ℛ⇩Γ ∩ {z. Im z < b})) =
(frontier ℛ⇩Γ ∪ ℛ⇩Γ) ∩ {z. Im z ≤ b} ∪ L"
by auto
also have "frontier ℛ⇩Γ ∪ ℛ⇩Γ = closure ℛ⇩Γ"
by (simp add: closure_Un_frontier Un_commute)
also {
have "L ⊆ path_image (mypath b)"
by (subst path_image_mypath_conv_frontier) (use assms in ‹auto simp: L_def›)
also have "… ⊆ closure ℛ⇩Γ ∩ {z. Im z ≤ b}"
using path_image_mypath_subset[OF assms] by blast
finally have "closure ℛ⇩Γ ∩ {z. Im z ≤ b} ∪ L = closure ℛ⇩Γ ∩ {z. Im z ≤ b}"
by blast
}
finally show ?thesis .
qed
subsection ‹Constructing the deformed path›
definition mypath'_circ1 where
"mypath'_circ1 ε = part_circlepath (❙ρ + 1) ε (5 * pi / 6 + arcsin (ε / 2)) (pi / 2)"
definition mypath'_circ2 where
"mypath'_circ2 ε = part_circlepath ❙ρ ε (pi / 2) (pi / 6 - arcsin (ε / 2))"
definition mypath'_circ3 where
"mypath'_circ3 ε = part_circlepath 𝗂 ε (pi + arcsin (ε / 2)) (- arcsin (ε / 2))"
definition mypath'_line where
"mypath'_line b = linepath (1/2 + b *⇩R 𝗂) (-1/2 + b *⇩R 𝗂)"
locale mypath_detour = meromorphic_form_full g k for g k +
fixes A :: "complex set" and b :: real
defines "A ≡ {z. Im z > 0 ∧ g z = 0} ∪ {z. Im z > 0 ∧ is_pole g z}"
assumes g_nonzero: "g ≠ 0"
assumes subset_zeros_poles: "A ⊆ {z. Im z ∈ {0<..<b}}"
assumes b_gt: "b > 1"
begin
definition f where "f = (λz. deriv g z / g z)"
lemma sparse_A: "A sparse_in {z. Im z > 0}"
proof -
have "eventually (λz. eval_mero_uhp g z ≠ 0 ∧ ¬is_pole g z) (cosparse ℋ)"
by (intro eventually_conj eval_mero_uhp_avoid_0 meromorphic_on_imp_not_pole_cosparse
meromorphic_intros open_halfspace_Im_gt) (use g_nonzero in auto)
hence "{z. eval_mero_uhp g z = 0 ∨ is_pole g z} sparse_in ℋ"
by (simp add: eventually_cosparse)
thus "A sparse_in ℋ"
by (rule sparse_in_subset2) (auto simp: A_def)
qed
lemma open_A_compl [intro]: "open ({z. Im z > 0} - A)"
using sparse_A by (simp add: open_diff_sparse_pts open_halfspace_Im_gt)
lemma open_A_compl_subset: "X ⊆ A ⟹ open ({z. Im z > 0} - X)"
by (rule open_diff_sparse_pts open_halfspace_Im_gt sparse_in_subset2[OF sparse_A])+
lemma g_has_field_derivative [derivative_intros]:
"Im z > 0 ⟹ z ∉ A ⟹ (g has_field_derivative deriv g z) (at z within X)"
by (intro analytic_derivI analytic_intros) (auto simp: A_def)
lemma g_has_field_derivative' [derivative_intros]:
assumes "(h has_field_derivative h') (at z within X)" "Im (h z) > 0" "h z ∉ A"
shows "((λx. g (h x)) has_field_derivative deriv g (h z) * h') (at z within X)"
using DERIV_chain [of g "deriv g (h z)" h z h' X, OF g_has_field_derivative assms(1)] assms(2-)
by (auto simp: o_def)
lemma f_holomorphic: "f holomorphic_on ({z. Im z > 0} - A)"
unfolding f_def by (intro holomorphic_intros open_A_compl) (auto simp: A_def)
lemma f_analytic: "f analytic_on X" if "X ⊆ {z. Im z > 0} - A" for X
proof (rule analytic_on_subset)
show "f analytic_on ({z. Im z > 0} - A)"
by (subst analytic_on_open) (auto intro: open_A_compl f_holomorphic)
qed (fact that)
lemma g_plus1: "g (z + 1) = g z"
using plus_1[of z] by simp
lemma g_invariant: "g (-(1 / z)) = z powi k * eval_mero_uhp g z"
proof -
have "-(1 / z) = apply_modgrp S_modgrp z"
by simp
also have "g … = z powi k * eval_mero_uhp g z"
by (subst invariant_apply_modgrp) auto
finally show ?thesis .
qed
lemma A_invariant1: "z + 1 ∈ A ⟷ z ∈ A"
using rel_imp_is_pole_iff[of "z" "z + 1"] unfolding A_def by (auto simp: g_plus1)
lemma A_invariant2: "-(1 / z) ∈ A ⟷ z ∈ A"
unfolding A_def using rel_imp_is_pole_iff[of "z" "-1/z"] rel_imp_eval_eq_0_iff[of "z" "-1/z"]
by auto
lemma deriv_g_invariant:
assumes "Im z > 0" "z ∉ A"
shows "deriv g (z + 1) = deriv g z"
and "deriv g (-(1 / z)) = deriv g z * z powi (k + 2) + of_int k * z * g (- 1 / z)"
proof -
have "((λz. g (z + 1)) has_field_derivative deriv g (z + 1)) (at z)"
using assms by (auto intro!: derivative_eq_intros simp del: g_plus1) (auto simp: A_invariant1)
also have "?this ⟷ (g has_field_derivative deriv g (z + 1)) (at z)"
by (simp add: g_plus1)
finally show "deriv g (z + 1) = deriv g z"
by (simp add: DERIV_imp_deriv)
let ?D1 = "deriv g (-1 / z) * z powi (-k - 2)"
let ?D2 = "-of_int k * z powi (-k - 1) * g (-1 / z)"
from assms have [simp]: "z ≠ 0"
by auto
have "Im (-1 / z) > 0" if "Im z > 0" for z
using Im_complex_div_gt_0 that by fastforce
hence "((λz. z powi (-k) * g (-1 / z)) has_field_derivative ?D1 + ?D2) (at z)"
using assms A_invariant2[of z]
by (auto intro!: derivative_eq_intros simp: power2_eq_square power_int_diff)
also have "?this ⟷ (g has_field_derivative ?D1 + ?D2) (at z)"
proof (rule DERIV_cong_ev)
have "eventually (λw. w ∈ {w. Im w > 0} - A) (nhds z)"
by (intro eventually_nhds_in_open) (use assms in ‹auto intro!: open_A_compl›)
thus "∀⇩F x in nhds z. x powi (-k) * g (-1 / x) = g x"
proof eventually_elim
case (elim x)
thus ?case
by (auto simp: power_int_minus field_simps g_invariant)
qed
qed auto
finally have "deriv g z = ?D1 + ?D2"
by (intro DERIV_imp_deriv)
thus "deriv g (-(1 / z)) = deriv g z * z powi (k + 2) + of_int k * z * g (- 1 / z)"
by (simp add: field_simps power_int_diff power_int_minus power_int_add power2_eq_square)
qed
lemma f_invariant:
assumes "Im z > 0" "z ∉ A"
shows "f (z + 1) = f z" and "f (-1 / z) = f z * z ^ 2 + of_int k * z"
proof -
have [simp]: "z ≠ 0" "g z ≠ 0"
using assms by (auto simp: A_def)
show "f (z + 1) = f z"
using assms by (simp_all add: f_def g_invariant deriv_g_invariant g_plus1)
have "f (-1 / z) = (deriv g z * z powi (k + 2) + of_int k * z * (z powi k * g z)) /
(z powi k * g z)"
using assms by (simp add: f_def g_invariant deriv_g_invariant)
also have "… = deriv g z * z ^ 2 / g z + of_int k * z"
by (auto simp: field_simps power_int_add)
also have "deriv g z * z ^ 2 / g z = f z * z ^ 2"
by (simp add: f_def)
finally show "f (-1 / z) = f z * z ^ 2 + of_int k * z" .
qed
text ‹
The singularities on the left vertical line and on the circular arc at the bottom, respectively:
›
definition S_l where "S_l = {z∈A∩closure ℛ⇩Γ-{❙ρ}. Re z = -1/2}"
definition S_arc where "S_arc = {z∈A∩closure ℛ⇩Γ-{❙ρ, 𝗂, ❙ρ+1}. norm z = 1}"
text ‹
The vertical positions of the singularities on the vertical lines.
›
definition Y where "Y = Im ` S_l"
definition ys where "ys = sorted_list_of_set Y"
text ‹
The angles of the singularities on the circular arc.
›
definition Φ where "Φ = Arg ` {z∈S_arc. Arg z < pi / 2}"
definition phis where "phis = sorted_list_of_set Φ"
definition phis' where "phis' = phis @ [pi/2] @ rev (map (λx. pi - x) phis)"
text ‹
The following two functions turn a vertical position on the left/right line into
the actual point.
›
definition lv :: "real ⇒ complex" where "lv y = -1/2 + y *⇩R 𝗂"
definition rv :: "real ⇒ complex" where "rv y = 1/2 + y *⇩R 𝗂"
text ‹
The only points on the original contour that we want to include in the deformed contour
are the singularities on the right vertical line (except for ‹ρ + 1›).
›
definition I where "I = S_l ∪ cis ` (λx. pi - x) ` Φ"
text ‹
The points on the original contour that we want to exclude ar the singularities on the
left vertical line and on the circular arc at the bottom (including ‹ρ›, ‹i›, and ‹ρ + 1›).
›
definition X where "X = (+) 1 ` S_l ∪ cis ` Φ ∪ {❙ρ, 𝗂, ❙ρ+1}"
text ‹
All the singularities not lying on the original curve should be preserved, i.e.\ they should
be (strictly) inside the new curve if and only if they were inside before and (strictly) outside
it if and only if they were outside before.
›
definition P where "P = {z. Im z ≤ 0} ∪ (A - frontier ℛ⇩Γ)"
lemma finite_A: "finite (A ∩ closure ℛ⇩Γ)"
proof -
have "finite ((closure ℛ⇩Γ ∩ {z. Im z ≤ b}) ∩ A)"
proof (rule sparse_in_compact_finite)
show "A sparse_in closure ℛ⇩Γ ∩ {z. Im z ≤ b}"
using sparse_A by (rule sparse_in_subset) (use closure_std_fund_region_Im_pos in auto)
have "closed (closure ℛ⇩Γ ∩ {z. Im z ≤ b})"
by (auto intro: closed_halfspace_Im_le)
moreover have "bounded (closure ℛ⇩Γ ∩ {z. Im z ≤ b})"
proof (rule bounded_subset)
show "closure ℛ⇩Γ ∩ {z. Im z ≤ b} ⊆ cbox (-1) (1 + 𝗂 * b)"
by (auto simp: in_closure_std_fund_region_iff in_cbox_complex_iff)
qed auto
ultimately show "compact (closure ℛ⇩Γ ∩ {z. Im z ≤ b})"
using compact_eq_bounded_closed by blast
qed
also have "(closure ℛ⇩Γ ∩ {z. Im z ≤ b}) ∩ A = A ∩ closure ℛ⇩Γ"
using subset_zeros_poles unfolding A_def by force
finally show ?thesis .
qed
lemma Y_finite: "finite Y"
unfolding Y_def by (intro finite_imageI finite_subset[OF _ finite_A])
(use std_fund_region'_subset in ‹auto simp: S_l_def›)
definition vjunc where "vjunc = (Min (insert b Y) + sqrt 3 / 2) / 2"
definition arcjunc where
"arcjunc = (if Φ = {} then pi/3 + pi/18 else (Min (insert (pi/2) Φ) + pi / 3) / 2)"
definition arcjunc' where
"arcjunc' = (if Φ = {} then pi/3 + 2*pi/18 else (pi / 2 + Max (insert (pi / 3) Φ)) / 2)"
lemma b_gt': "b > sqrt 3 / 2"
proof -
have "sqrt 3 < 2"
by (intro real_less_lsqrt) auto
hence "sqrt 3 / 2 < 1"
by simp
thus ?thesis
by (rule less_trans [OF _ b_gt])
qed
lemma Y_subset: "Y ⊆ {sqrt 3 / 2 <..< b}"
proof
fix y assume y: "y ∈ Y"
then obtain z where z: "Im z = y" "z ∈ S_l"
by (auto simp: Y_def)
hence "Re z = -1/2" "z ≠ ❙ρ"
by (auto simp: S_l_def)
hence z_eq: "z = -1/2 + 𝗂 * y"
using z by (auto simp: complex_eq_iff)
have "y < b" "y > 0"
using z subset_zeros_poles by (auto simp: S_l_def)
have "(1 / 2) ^ 2 + (sqrt 3 / 2) ^ 2 = 1"
by (simp add: power2_eq_square)
also have "… ≤ norm z ^ 2"
using z by (auto simp: S_l_def closure_std_fund_region)
also have "… = (1 / 2) ^ 2 + y ^ 2"
unfolding cmod_power2 by (simp add: z_eq)
finally have "y ≥ sqrt 3 / 2"
using ‹y > 0› by (simp flip: abs_le_square_iff)
moreover have "y ≠ sqrt 3 / 2"
using ‹z ≠ ❙ρ› by (auto simp: complex_eq_iff z_eq)
ultimately show "y ∈ {sqrt 3 / 2 <..< b}"
using ‹y < b› by auto
qed
lemma ys: "set ys = Y" "sorted_wrt (<) ys"
unfolding ys_def using Y_finite by auto
lemma vjunc: "vjunc ∈ {sqrt 3 / 2 <..< b}" "∀y∈Y. vjunc < y"
proof -
have "Min (insert b Y) > sqrt 3 / 2"
using Y_subset Y_finite b_gt' by (subst Min_gr_iff) auto
hence *: "vjunc > sqrt 3 / 2"
by (simp add: vjunc_def)
moreover have "Min (insert b Y) ≤ b"
using Y_finite by (subst Min_le_iff) auto
hence "vjunc < b" using b_gt'
by (simp add: vjunc_def)
ultimately show "vjunc ∈ {sqrt 3 / 2 <..< b}" by auto
show "∀y∈Y. vjunc < y"
proof safe
fix y assume y: "y ∈ Y"
have "vjunc < Min (insert b Y)"
using * unfolding vjunc_def add_divide_distrib by linarith
also have "Min (insert b Y) ≤ y"
by (rule Min.coboundedI) (use Y_finite y in auto)
finally show "vjunc < y" .
qed
qed
lemma vjunc_pos: "vjunc > 0"
proof -
have "0 < sqrt 3 / 2"
by simp
also have "… < vjunc"
using vjunc by auto
finally show ?thesis .
qed
lemma Φ_finite: "finite Φ"
unfolding Φ_def by (intro finite_imageI finite_subset[OF _ finite_A])
(use std_fund_region'_subset in ‹auto simp: S_arc_def›)
lemma Arg_S_arc_gt:
assumes "z ∈ S_arc"
shows "Arg z > pi / 3"
proof -
from assms have z: "norm z = 1" "Im z ≥ 0" "z ≠ ❙ρ + 1" "z ∈ closure ℛ⇩Γ" "Re z ≤ 1 / 2"
by (auto simp: S_arc_def closure_std_fund_region)
have [simp]: "z ≠ 0"
using z by auto
have "Re z ≠ 1 / 2"
proof
assume "Re z = 1 / 2"
have "1 = norm z ^ 2"
using z by simp
also have "… = Re z ^ 2 + Im z ^ 2"
unfolding cmod_power2 ..
finally have *: "Im z ^ 2 = 3 / 4"
by (simp add: ‹Re z = 1 / 2› power_divide)
have "sqrt (Im z ^ 2) = sqrt 3 / 2"
using ‹Im z ≥ 0› by (subst *) (auto simp: real_sqrt_divide)
with ‹Re z = 1 / 2› show False
using ‹z ≠ ❙ρ + 1› ‹Im z ≥ 0› by (simp add: complex_eq_iff)
qed
with ‹Re z ≤ 1 / 2› have "Re z < 1 / 2"
by linarith
also have "z = cis (Arg z)"
by (simp add: cis_Arg complex_sgn_def z)
also have "Re … = cos (Arg z)"
by simp
finally have "cos (Arg z) < cos (pi / 3)"
by (simp add: cos_60)
thus ?thesis
using Arg_bounded [of z] Arg_less_0[of z] ‹Im z ≥ 0›
by (subst (asm) cos_mono_less_eq) auto
qed
lemma Φ_subset: "Φ ⊆ {pi / 3 <..< pi / 2}"
using Arg_S_arc_gt unfolding Φ_def by auto
lemma phis: "set phis = Φ" "sorted_wrt (<) phis"
unfolding phis_def using Φ_finite by auto
lemma arcjunc: "arcjunc ∈ {pi/3 <..< pi/2}" "⋀x. x ∈ Φ ⟹ arcjunc < x"
proof -
have *: "Min (insert (pi / 2) Φ) > pi / 3"
using Φ_subset Φ_finite by (subst Min_gr_iff) auto
show "arcjunc ∈ {pi/3 <..< pi/2}"
proof (cases "Φ = {}")
case False
have eq: "arcjunc = (Min (insert (pi / 2) Φ) + pi / 3)/2"
unfolding arcjunc_def using False by auto
have "arcjunc > pi / 3"
using * by (simp add: arcjunc_def)
moreover have "Min (insert (pi / 2) Φ) ≤ pi / 2"
using Φ_finite by (subst Min_le_iff) auto
hence "arcjunc < pi / 2"
unfolding eq add_divide_distrib using pi_gt_zero by linarith
ultimately show "arcjunc ∈ {pi/3 <..< pi/2}" by auto
qed (auto simp: arcjunc_def)
show "arcjunc < y" if y: "y ∈ Φ" for y
proof -
have eq: "arcjunc = (Min (insert (pi / 2) Φ) + pi / 3)/2"
unfolding arcjunc_def using y by auto
have "arcjunc < Min (insert (pi/2) Φ)"
using * unfolding eq add_divide_distrib by linarith
also have "Min (insert (pi/2) Φ) ≤ y"
by (rule Min.coboundedI) (use Φ_finite y in auto)
finally show "arcjunc < y" .
qed
qed
lemma arcjunc': "arcjunc' ∈ {pi/3 <..< pi/2}" "⋀x. x ∈ Φ ⟹ arcjunc' > x"
proof -
have *: "Max (insert (pi / 3) Φ) < pi / 2"
using Φ_subset Φ_finite by (subst Max_less_iff) auto
show "arcjunc' ∈ {pi/3 <..< pi/2}"
proof (cases "Φ = {}")
case False
have eq: "arcjunc' = (pi / 2 + Max (insert (pi / 3) Φ)) / 2"
unfolding arcjunc'_def using False by auto
from * have "arcjunc' < pi / 2"
by (simp add: arcjunc'_def)
moreover have "Max (insert (pi / 3) Φ) ≥ pi / 3"
using Φ_finite by (subst Max_ge_iff) auto
hence "arcjunc' > pi / 3"
unfolding eq add_divide_distrib using pi_gt_zero by linarith
ultimately show "arcjunc' ∈ {pi/3 <..< pi/2}" by auto
qed (auto simp: arcjunc'_def)
show "arcjunc' > y" if y: "y ∈ Φ" for y
proof -
have eq: "arcjunc' = (pi / 2 + Max (insert (pi / 3) Φ)) / 2"
unfolding arcjunc'_def using y by auto
have "y ≤ Max (insert (pi/3) Φ)"
by (rule Max.coboundedI) (use Φ_finite y in auto)
also have "Max (insert (pi/3) Φ) < arcjunc'"
using * unfolding eq add_divide_distrib by linarith
finally show "arcjunc' > y" .
qed
qed
lemma arcjunc_less_arcjunc': "arcjunc < arcjunc'"
proof (cases "Φ = {}")
case False
then obtain y where "y ∈ Φ"
by blast
with arcjunc(2)[of y] arcjunc'(2)[of y] show ?thesis
by linarith
qed (auto simp: arcjunc_def arcjunc'_def)
lemma sorted1: "sorted_wrt (<) (vjunc # ys @ [b])"
using vjunc ys Y_subset by (auto simp: sorted_wrt_append)
lemma sorted2: "sorted_wrt (<) (arcjunc # phis @ [arcjunc'])"
using phis arcjunc_less_arcjunc' arcjunc arcjunc' by (auto simp: sorted_wrt_append)
lemma minus_cnj_in_A_iff: "norm z = 1 ⟹ -cnj z ∈ A ⟷ z ∈ A"
using A_invariant2[of z] by (simp add: divide_conv_cnj)
lemma minus_cnj_eq_rho_iff [simp]: "-cnj z = ❙ρ ⟷ z = ❙ρ + 1"
and minus_cnj_eq_rho'_iff [simp]: "-cnj z = ❙ρ + 1 ⟷ z = ❙ρ"
and minus_cnj_eq_i_iff [simp]: "-cnj z = 𝗂 ⟷ z = 𝗂"
by (auto simp: complex_eq_iff)
lemma minus_cnj_in_S_arc_iff [simp]: "-cnj z ∈ S_arc ⟷ z ∈ S_arc"
proof -
have "-cnj z ∈ S_arc" if "z ∈ S_arc" for z
using that unfolding S_arc_def
by (auto simp: closure_std_fund_region minus_cnj_in_A_iff)
from this[of z] this[of "-cnj z"] show ?thesis
by auto
qed
lemma minus_cnj_in_closure_std_fund_region_iff [simp]:
"- cnj z ∈ closure ℛ⇩Γ ⟷ z ∈ closure ℛ⇩Γ"
by (auto simp: closure_std_fund_region)
lemma S_arc_decompose: "S_arc = cis ` Φ ∪ cis ` (λx. pi - x) ` Φ"
proof
have 1: "cis (Arg z) = z" if "norm z = 1" for z
using that by (subst cis_Arg) (auto simp: complex_sgn_def)
have "z ∈ S_arc" if "z ∈ cis ` Φ ∪ cis ` (-) pi ` Φ" for z using that
by (auto simp: S_arc_def Φ_def 1 norm_divide divide_conv_cnj minus_cnj_in_A_iff
simp flip: cis_divide)
thus "cis ` Φ ∪ cis ` (-) pi ` Φ ⊆ S_arc"
by blast
show "S_arc ⊆ cis ` Φ ∪ cis ` (-) pi ` Φ"
proof
fix z assume z: "z ∈ S_arc"
have [simp]: "z ≠ 0" "norm z = 1"
using z by (auto simp: S_arc_def)
have "Im z ≥ 0"
using z by (auto simp: S_arc_def closure_std_fund_region)
thus "z ∈ cis ` Φ ∪ cis ` (-) pi ` Φ"
proof (cases "Arg z" "pi / 2" rule: linorder_cases)
case less
have "z ∈ {z ∈ S_arc. Arg z < pi / 2}"
using less z by auto
moreover have "z = cis (Arg z)"
by (subst cis_Arg) (use z in ‹auto simp: S_arc_def complex_sgn_def›)
ultimately show "z ∈ cis ` Φ ∪ cis ` (-) pi ` Φ"
unfolding Φ_def image_image by blast
next
case greater
have "Arg z < 2 * pi"
by (rule le_less_trans[of _ pi]) (use Arg_bounded[of z] in auto)
hence "Arg (-cnj z) = pi - Arg z"
using z greater ‹Im z ≥ 0›
by (intro cis_Arg_unique)
(auto simp: complex_sgn_def scaleR_conv_of_real S_arc_def divide_conv_cnj
cis_Arg Arg_less_0 simp flip: cis_divide)
hence "-cnj z ∈ {z ∈ S_arc. Arg z < pi / 2}"
using greater z by (auto simp: S_arc_def minus_cnj_in_A_iff)
moreover have "z = cis (pi - Arg (-cnj z))"
by (auto simp: cis_Arg complex_sgn_def divide_conv_cnj simp flip: cis_divide)
ultimately show "z ∈ cis ` Φ ∪ cis ` (-) pi ` Φ"
unfolding Φ_def image_image by blast
next
case equal
have "cis (Arg z) = z"
by (simp add: cis_Arg complex_sgn_def)
also have "Arg z = pi / 2"
using equal by simp
finally have "z = 𝗂"
by simp
with z have False
by (auto simp: S_arc_def)
thus ?thesis ..
qed
qed
qed
subsubsection ‹The vertical segments›
fun mypath'_vert :: "bool ⇒ real ⇒ real ⇒ real list ⇒ real ⇒ real ⇒ complex" where
"mypath'_vert left l u [] ε = linepath (rv l) (rv u)"
| "mypath'_vert left l u [y] ε = avoid_linepath left (rv l) (rv u) (rv y) ε"
| "mypath'_vert left l u (y1 # y2 # ys') ε =
avoid_linepath left (rv l) (rv ((y1 + y2) / 2)) (rv y1) ε +++
mypath'_vert left ((y1 + y2) / 2) u (y2 # ys') ε"
definition mypath'_vert'
where "mypath'_vert' left l u ys' ε = reversepath ((+) (-1) ∘ mypath'_vert left l u ys' ε)"
lemma detour_rel_mypath'_vert:
assumes "sorted_wrt (<) (l # ys' @ [u])"
shows "detour_rel {} (rv ` set ys') (linepath (rv l) (rv u))
(mypath'_vert False l u ys') (mypath'_vert True l u ys')"
using assms
proof (induction ys' arbitrary: l rule: induct_list012)
case 1
thus ?case by auto
next
case (2 y l)
thus ?case
by (auto intro!: detour_rel_linepath_semicircle_right
simp: open_segment_eq_real_ivl rv_def open_segment_same_Re)
next
case (3 y1 y2 ys l)
define m where "m = (y1 + y2) / 2"
have "detour_rel ({} ∪ {}) ({rv y1} ∪ rv ` set (y2 # ys))
(linepath (rv l) (rv m) +++ linepath (rv m) (rv u))
(λε. avoid_linepath False (rv l) (rv m) (rv y1) ε +++
mypath'_vert False m u (y2 # ys) ε)
(λε. avoid_linepath True (rv l) (rv m) (rv y1) ε +++
mypath'_vert True m u (y2 # ys) ε)"
using "3.prems"
by (intro detour_rel_join detour_rel_linepath_semicircle_right "3.IH")
(auto simp: rv_def m_def open_segment_same_Re open_segment_eq_real_ivl)
also have "linepath (rv l) (rv m) +++ linepath (rv m) (rv u) ≡⇩p
linepath (rv l) (rv u)"
using "3.prems"
by (intro eq_paths_linepaths)
(auto simp: rv_def m_def closed_segment_same_Re closed_segment_eq_real_ivl complex_eq_iff)
finally show ?case
by (simp add: m_def insert_commute)
qed
lemma pathstart_mypath'_vert [simp]: "pathstart (mypath'_vert left l u ys' ε) = rv l"
and pathfinish_mypath'_vert [simp]: "pathfinish (mypath'_vert left l u ys' ε) = rv u"
by (induction left l u ys' ε rule: mypath'_vert.induct;
simp add: avoid_linepath_def rcis_def Let_def; fail)+
lemma valid_path_mypath'_vert:
"sorted_wrt (<) (l # ys' @ [u]) ⟹ valid_path (mypath'_vert left l u ys' ε)"
proof (induction ys' arbitrary: l rule: induct_list012)
case 1
thus ?case by auto
next
case (2 y l)
thus ?case
by (auto intro!: valid_path_avoid_linepath simp: rv_def)
next
case (3 y1 y2 ys l)
define m where "m = (y1 + y2) / 2"
have "valid_path (mypath'_vert left m u (y2 # ys) ε)"
using "3.prems" by (intro "3.IH") (auto simp: m_def)
moreover have "pathfinish (avoid_linepath left (rv l) (rv ((y1 + y2) / 2)) (rv y1) ε) =
rv ((y1 + y2) / 2)"
by (auto simp: avoid_linepath_def)
moreover have "rv l ≠ rv m"
using "3.prems" by (auto simp: rv_def m_def)
ultimately show ?case using "3.prems"
by (auto intro!: valid_path_join valid_path_avoid_linepath simp: m_def)
qed
lemma detour_rel_mypath'_vert':
assumes "sorted_wrt (<) (l # ys' @ [u])"
shows "detour_rel (lv ` set ys') {} (linepath (lv u) (lv l))
(mypath'_vert' False l u ys') (mypath'_vert' True l u ys')"
proof -
have "detour_rel ((+) (-1) ` {}) ((+) (-1) ` rv ` set ys') ((+) (-1) ∘ linepath (rv l) (rv u))
(λε. (+) (-1) ∘ mypath'_vert False l u ys' ε) (λε. (+) (-1) ∘ mypath'_vert True l u ys' ε)"
by (intro detour_rel_translate detour_rel_mypath'_vert[OF assms])
also have "((+) (-1) ` rv ` set ys') = lv ` set ys'"
unfolding image_image by (intro image_cong) (auto simp: rv_def lv_def)
also have "((+) (-1) ` {}) = ({} :: complex set)"
by auto
also have "(+) (-1) ∘ linepath (rv l) (rv u) = linepath (lv l) (lv u)"
unfolding linepath_translate by (simp add: rv_def lv_def)
finally have "detour_rel (lv ` set ys') {} (reversepath (linepath (lv l) (lv u)))
(mypath'_vert' False l u ys') (mypath'_vert' True l u ys')"
unfolding mypath'_vert'_def by (rule detour_rel_reverse)
thus ?thesis
by simp
qed
lemma pathstart_mypath'_vert' [simp]: "pathstart (mypath'_vert' left l u ys' ε) = lv u"
and pathfinish_mypath'_vert' [simp]: "pathfinish (mypath'_vert' left l u ys' ε) = lv l"
by (simp_all add: mypath'_vert'_def lv_def rv_def pathfinish_compose pathstart_compose)
lemma valid_path_mypath'_vert':
"sorted_wrt (<) (l # ys' @ [u]) ⟹ valid_path (mypath'_vert' left l u ys' ε)"
unfolding mypath'_vert'_def valid_path_reversepath valid_path_translation_eq
by (rule valid_path_mypath'_vert)
subsubsection ‹The circular arcs›
text ‹
On one half of the arc we will simply place circular arcs to avoid the bad points.
›
fun arc_aux where
"arc_aux left l u [] ε = [part_circlepath 0 1 u l]"
| "arc_aux left l u [y] ε = [avoid_part_circlepath left 0 1 u l y ε]"
| "arc_aux left l u (y1 # y2 # ys') ε =
avoid_part_circlepath left 0 1 u ((y1 + y2) / 2) y1 ε #
arc_aux left l ((y1 + y2) / 2) (y2 # ys') ε"
definition mypath'_arcm :: "bool ⇒ real ⇒ real ⇒ complex" where
"mypath'_arcm left ε =
avoid_part_circlepath left 0 1 (pi - arcjunc') arcjunc' (pi / 2) ε"
definition mypath'_arcr :: "bool ⇒ real ⇒ real ⇒ complex"
where "mypath'_arcr left = joinpaths_list ∘ arc_aux left arcjunc arcjunc' (rev phis)"
definition mypath'_arcl :: "bool ⇒ real ⇒ real ⇒ complex"
where "mypath'_arcl left ε = (λz. -(1/z)) ∘ reversepath (mypath'_arcr left ε)"
definition mypath'_arc :: "bool ⇒ real ⇒ real ⇒ complex" where
"mypath'_arc left ε = mypath'_arcl left (ε/2) +++ mypath'_arcm left ε +++ mypath'_arcr left (ε/2)"
lemma arc_aux_not_empty [simp]: "arc_aux left l u ys' ε ≠ []"
by (induction left l u ys' ε rule: arc_aux.induct) simp_all
lemma detour_rel_arc_aux:
assumes "ys' = [] ∨ sorted_wrt (>) (u # ys' @ [l])"
shows "detour_rel {} (cis ` set ys') (part_circlepath 0 1 u l)
(λε. joinpaths_list (arc_aux False l u ys' ε))
(λε. joinpaths_list (arc_aux True l u ys' ε))"
using assms
proof (induction ys' arbitrary: u rule: induct_list012)
case 1
thus ?case by auto
next
case (2 y l)
thus ?case
by (auto intro!: detour_rel_part_circlepath_semicircle_right
simp: open_segment_eq_real_ivl open_segment_same_Re rcis_def)
next
case (3 y1 y2 ys u)
define m where "m = (y1 + y2) / 2"
have "detour_rel ({} ∪ {}) ({cis y1} ∪ cis ` set (y2 # ys))
(part_circlepath 0 1 u m +++ part_circlepath 0 1 m l)
(λε. avoid_part_circlepath False 0 1 u m y1 ε +++
joinpaths_list (arc_aux False l m (y2 # ys) ε))
(λε. avoid_part_circlepath True 0 1 u m y1 ε +++
joinpaths_list (arc_aux True l m (y2 # ys) ε))"
using "3.prems"
by (intro detour_rel_join detour_rel_part_circlepath_semicircle_right "3.IH")
(auto simp: m_def open_segment_same_Re open_segment_eq_real_ivl rcis_def sorted_wrt_append
pathfinish_part_circlepath' pathstart_part_circlepath')
also have "part_circlepath 0 1 u m +++ part_circlepath 0 1 m l ≡⇩p
part_circlepath 0 1 u l"
using "3.prems"
by (intro eq_paths_part_circlepaths)
(auto simp: m_def closed_segment_same_Re closed_segment_eq_real_ivl complex_eq_iff)
finally show ?case
by (simp add: m_def insert_commute pathfinish_part_circlepath' pathstart_part_circlepath')
qed
lemma detour_rel_arcr_aux:
"detour_rel {} (cis ` Φ) (part_circlepath 0 1 arcjunc' arcjunc)
(mypath'_arcr False) (mypath'_arcr True)"
proof -
have "phis = [] ∨ sorted_wrt (>) (rev (arcjunc # phis @ [arcjunc']))"
using sorted2 unfolding sorted_wrt_rev by auto
hence "detour_rel {} (cis ` set (rev phis)) (part_circlepath 0 1 arcjunc' arcjunc)
(mypath'_arcr False) (mypath'_arcr True)"
unfolding mypath'_arcr_def o_def by (intro detour_rel_arc_aux) simp_all
also have "cis ` set (rev phis) = cis ` Φ"
by (simp add: image_Un phis)
finally show ?thesis .
qed
lemma detour_rel_arcr:
"detour_rel {} (cis ` Φ) (part_circlepath 0 1 arcjunc' arcjunc)
(λε. mypath'_arcr False (ε / 2)) (λε. mypath'_arcr True (ε / 2))"
using detour_rel_arcr_aux by (rule detour_rel_rescale) auto
lemma detour_rel_arcl:
"detour_rel (cis ` (λx. pi - x) ` Φ) {} (part_circlepath 0 1 (pi - arcjunc) (pi - arcjunc'))
(λε. mypath'_arcl False (ε / 2)) (λε. mypath'_arcl True (ε / 2))"
proof -
define f where "f = (λz. -(1 / z) :: complex)"
have "detour_rel (cis ` Φ) {} (reversepath (part_circlepath 0 1 arcjunc' arcjunc))
(λε. reversepath (mypath'_arcr False ε)) (λε. reversepath (mypath'_arcr True ε))"
unfolding o_def by (intro detour_rel_reverse detour_rel_arcr_aux)
also have "reversepath (part_circlepath 0 1 arcjunc' arcjunc) =
part_circlepath 0 1 arcjunc arcjunc'" by simp
finally have "detour_rel (f ` cis ` Φ) (f ` {})
(f ∘ part_circlepath 0 1 arcjunc arcjunc')
(λε. mypath'_arcl False (ε / 2)) (λε. mypath'_arcl True (ε / 2))"
unfolding mypath'_arcl_def f_def
proof (intro detour_rel_image, fold f_def)
have "winding_preserving {z. Im z ≥ sqrt 2 / 2} (λz. - inverse z) (λz. z)"
proof (rule winding_preserving_comp' [OF winding_preserving_uminus _ order.refl],
rule winding_preserving_inverse_upper_halfspace)
show "{z. sqrt 2 / 2 ≤ Im z} ⊆ {z. 0 < Im z}"
by safe (erule less_le_trans [rotated], auto)
qed
thus "winding_preserving {z. Im z ≥ sqrt 2 / 2} f (λx. x)"
by (simp add: f_def field_simps)
next
show "2-lipschitz_on {z. sqrt 2 / 2 ≤ Im z} f"
unfolding f_def using lipschitz_on_complex_inverse[of "sqrt 2 / 2"]
by (intro lipschitz_intros) (auto simp: field_simps)
next
show "f analytic_on {z. sqrt 2 / 2 ≤ Im z}"
unfolding f_def by (auto intro!: analytic_intros)
next
show "closed {z. sqrt 2 / 2 ≤ Im z}"
by (rule closed_halfspace_Im_ge)
next
show "path_image (part_circlepath 0 1 arcjunc arcjunc') ⊆ interior {z. sqrt 2 / 2 ≤ Im z}"
unfolding path_image_part_circlepath'
proof safe
fix t assume t: "t ∈ closed_segment arcjunc arcjunc'"
have "sqrt 2 / 2 < sin (pi / 3)"
by (simp add: sin_60)
also have "sin (pi / 3) ≤ sin t"
using t arcjunc arcjunc' arcjunc_less_arcjunc'
by (intro sin_monotone_2pi_le) (auto simp: closed_segment_eq_real_ivl)
finally show "0 + rcis 1 t ∈ interior {z. sqrt 2 / 2 ≤ Im z}"
unfolding interior_halfspace_Im_ge by (simp add: sin_60)
qed
qed (auto simp: closed_halfspace_Im_ge)
also have "f ` cis ` Φ = cis ` (λx. pi - x) ` Φ"
unfolding image_image by (intro image_cong) (auto simp: f_def simp flip: cis_divide)
also have "f ∘ part_circlepath 0 1 arcjunc arcjunc' = part_circlepath 0 1 (pi - arcjunc) (pi - arcjunc')"
by (simp add: f_def part_circlepath_altdef rcis_def o_def linepath_def ring_distribs mult_ac
flip: cis_mult cis_divide)
finally show ?thesis
by simp
qed
lemma detour_rel_arcm:
"detour_rel {} {𝗂} (part_circlepath 0 1 (pi - arcjunc') arcjunc')
(mypath'_arcm False) (mypath'_arcm True)"
unfolding mypath'_arcm_def
by (rule detour_rel_part_circlepath_semicircle_right)
(use arcjunc' in ‹auto simp: open_segment_eq_real_ivl rcis_def›)
lemma detour_rel_arc:
"detour_rel (cis ` (λx. pi - x) ` Φ) (insert 𝗂 (cis ` Φ))
(part_circlepath 0 1 (pi - arcjunc) arcjunc)
(mypath'_arc False) (mypath'_arc True)"
proof -
have "detour_rel (cis ` (λx. pi - x) ` Φ ∪ {} ∪ {}) ({} ∪ {𝗂} ∪ cis ` Φ)
(part_circlepath 0 1 (pi - arcjunc) (pi - arcjunc') +++
part_circlepath 0 1 (pi - arcjunc') arcjunc' +++
part_circlepath 0 1 arcjunc' arcjunc)
(λε. mypath'_arc False ε) (λε. mypath'_arc True ε)"
unfolding mypath'_arc_def Un_assoc
by (intro detour_rel_join detour_rel_arcr detour_rel_arcm detour_rel_arcl)
(auto simp: pathfinish_part_circlepath' pathstart_part_circlepath')
also have "(part_circlepath 0 1 (pi - arcjunc) (pi - arcjunc') +++
part_circlepath 0 1 (pi - arcjunc') arcjunc' +++
part_circlepath 0 1 arcjunc' arcjunc) ≡⇩p part_circlepath 0 1 (pi - arcjunc) arcjunc"
using arcjunc_less_arcjunc' arcjunc(1) arcjunc'(1)
by (intro eq_paths_joinpaths_part_circlepath)
(auto simp: closed_segment_eq_real_ivl pathfinish_part_circlepath' pathstart_part_circlepath')
finally show ?thesis
by (simp add: pathfinish_part_circlepath' pathstart_part_circlepath')
qed
lemma pathstart_mypath'_arc_aux [simp]: "pathstart (hd (arc_aux left l u ys' ε)) = cis u"
and pathfinish_mypath'_arc_aux [simp]: "pathfinish (last (arc_aux left l u ys' ε)) = cis l"
by (induction left l u ys' ε rule: arc_aux.induct;
simp add: avoid_part_circlepath_def rcis_def Let_def
pathfinish_part_circlepath' pathstart_part_circlepath'; fail)+
lemma pathstart_mypath'_arcr [simp]: "pathstart (mypath'_arcr left ε) = cis arcjunc'"
and pathfinish_mypath'_arcr [simp]: "pathfinish (mypath'_arcr left ε) = cis arcjunc"
by (simp_all add: mypath'_arcr_def)
lemma pathstart_mypath'_arcl [simp]: "pathstart (mypath'_arcl left ε) = cis (pi - arcjunc)"
and pathfinish_mypath'_arcl [simp]: "pathfinish (mypath'_arcl left ε) = cis (pi - arcjunc')"
by (simp_all add: mypath'_arcl_def pathstart_compose pathfinish_compose divide_conv_cnj
flip: cis_divide)
lemma pathstart_mypath'_arcm [simp]: "pathstart (mypath'_arcm left ε) = cis (pi - arcjunc')"
and pathfinish_mypath'_arcm [simp]: "pathfinish (mypath'_arcm left ε) = cis arcjunc'"
by (simp_all add: mypath'_arcm_def avoid_part_circlepath_def Let_def rcis_def
pathfinish_part_circlepath' pathstart_part_circlepath')
lemma pathstart_mypath'_arc [simp]: "pathstart (mypath'_arc left ε) = cis (pi - arcjunc)"
and pathfinish_mypath'_arc [simp]: "pathfinish (mypath'_arc left ε) = cis arcjunc"
by (simp_all add: mypath'_arc_def)
lemma valid_path_arc_aux:
"ε ∈ {0<..<2} ⟹ ys' = [] ∨ sorted_wrt (>) (u # ys' @ [l]) ⟹
valid_path (joinpaths_list (arc_aux left l u ys' ε))"
proof (induction ys' arbitrary: u rule: induct_list012)
case 1
thus ?case by auto
next
case (2 y u)
thus ?case
by (auto intro!: valid_path_avoid_part_circlepath)
next
case (3 y1 y2 ys u)
define m where "m = (y1 + y2) / 2"
have "valid_path (joinpaths_list (arc_aux left l m (y2 # ys) ε))"
using "3.prems" by (intro "3.IH") (auto simp: m_def sorted_wrt_append)
moreover have "pathfinish (avoid_part_circlepath left 0 1 u ((y1 + y2) / 2) y1 ε) =
cis ((y1 + y2) / 2)"
by (auto simp: avoid_part_circlepath_def Let_def rcis_def
pathfinish_part_circlepath' pathstart_part_circlepath')
ultimately show ?case using "3.prems"
by (auto intro!: valid_path_join valid_path_avoid_part_circlepath simp: m_def)
qed
lemma valid_path_arcm: "ε ∈ {0<..<2} ⟹ valid_path (mypath'_arcm left ε)"
using arcjunc' by (auto simp: mypath'_arcm_def intro!: valid_path_avoid_part_circlepath)
lemma valid_path_arcr:
assumes "ε ∈ {0<..<2}"
shows "valid_path (mypath'_arcr left ε)"
proof -
have "phis = [] ∨ sorted_wrt (>) (rev (arcjunc # phis @ [arcjunc']))"
using sorted2 unfolding sorted_wrt_rev by auto
thus ?thesis
unfolding mypath'_arcr_def o_def using assms by (intro valid_path_arc_aux) simp_all
qed
lemma valid_path_arcl: "eventually (λε. valid_path (mypath'_arcl left (ε / 2))) (at_right 0)"
proof -
have "simple_path (part_circlepath 0 1 (pi - arcjunc) (pi - arcjunc'))"
"valid_path (part_circlepath 0 1 (pi - arcjunc) (pi - arcjunc'))"
using arcjunc_less_arcjunc' arcjunc(1) arcjunc'(1) by (auto simp: simple_path_part_circlepath)
from detour_rel_imp_valid_simple_path [OF detour_rel_arcl this] show ?thesis
by eventually_elim (cases left, auto)
qed
subsection ‹The corners›
definition mypath'_lcorner where
"mypath'_lcorner left ε = avoid_linepath_circlepath left vjunc (pi - arcjunc) ε"
definition mypath'_rcorner where
"mypath'_rcorner left ε = (λz. -cnj z) ∘ reversepath (mypath'_lcorner left ε)"
lemma pathstart_mypath'_lcorner [simp]: "pathstart (mypath'_lcorner left ε) = lv vjunc"
and pathfinish_mypath'_lcorner [simp]: "pathfinish (mypath'_lcorner left ε) = cis (pi - arcjunc)"
by (simp_all add: mypath'_lcorner_def avoid_linepath_circlepath_def Let_def lv_def rcis_def
pathstart_part_circlepath' pathfinish_part_circlepath')
lemma pathstart_mypath'_rcorner [simp]: "pathstart (mypath'_rcorner left ε) = cis arcjunc"
and pathfinish_mypath'_rcorner [simp]: "pathfinish (mypath'_rcorner left ε) = rv vjunc"
by (simp_all add: mypath'_rcorner_def pathstart_compose pathfinish_compose flip: cis_divide
add: avoid_linepath_circlepath_def Let_def lv_def rv_def rcis_def divide_conv_cnj)
lemma valid_path_lcorner: "ε ∈ {0..2} ⟹ valid_path (mypath'_lcorner left ε)"
unfolding mypath'_lcorner_def by (intro valid_path_avoid_linepath_circlepath) auto
lemma valid_path_rcorner:
assumes "ε ∈ {0..2}"
shows "valid_path (mypath'_rcorner left ε)"
proof -
have "valid_path (uminus ∘ (cnj ∘
reversepath (avoid_linepath_circlepath left vjunc (pi - arcjunc) ε)))"
unfolding valid_path_cnj valid_path_uminus_comp valid_path_reversepath
by (intro valid_path_avoid_linepath_circlepath) (use assms in auto)
thus ?thesis
by (simp add: mypath'_rcorner_def mypath'_lcorner_def o_def)
qed
lemma detour_rel_mypath'_lcorner:
"detour_rel {} {❙ρ}
(linepath (lv vjunc) ❙ρ +++ part_circlepath 0 1 (2 / 3 * pi) (pi - arcjunc))
(mypath'_lcorner False) (mypath'_lcorner True)"
unfolding mypath'_lcorner_def lv_def modfun_rho_def times_divide_eq_left
by (rule detour_rel_avoid_linepath_circlepath_right) (use vjunc arcjunc in auto)
lemma detour_rel_mypath'_rcorner:
"detour_rel {} {❙ρ + 1}
(part_circlepath 0 1 arcjunc (pi / 3) +++ linepath (❙ρ + 1) (rv vjunc))
(mypath'_rcorner False) (mypath'_rcorner True)"
proof -
define h where "h = (λx. -x) ∘ cnj"
have "detour_rel {❙ρ} {}
(reversepath (linepath (lv vjunc) ❙ρ +++ part_circlepath 0 1 (2 * pi / 3) (pi - arcjunc)))
(λε. reversepath (mypath'_lcorner False ε))
(λε. reversepath (mypath'_lcorner True ε))"
using detour_rel_reverse [OF detour_rel_mypath'_lcorner] by simp
also have "reversepath (linepath (lv vjunc) ❙ρ +++ part_circlepath 0 1 (2 * pi / 3) (pi - arcjunc)) =
part_circlepath 0 1 (pi - arcjunc) (2 * pi / 3) +++ linepath ❙ρ (lv vjunc)"
by (subst reversepath_joinpaths)
(simp_all add: rcis_def modfun_rho_def pathfinish_part_circlepath' pathstart_part_circlepath')
finally have "detour_rel (h ` {}) (h ` {❙ρ})
(h ∘ (part_circlepath 0 1 (pi - arcjunc) (2 * pi / 3) +++ linepath ❙ρ (lv vjunc)))
(λε. h ∘ reversepath (mypath'_lcorner False ε))
(λε. h ∘ reversepath (mypath'_lcorner True ε))"
unfolding h_def o_assoc [symmetric] image_comp [symmetric]
by (intro detour_rel_uminus detour_rel_cnj)
also have "(λε. h ∘ reversepath (mypath'_lcorner True ε)) = mypath'_rcorner True"
by (simp add: mypath'_rcorner_def [abs_def] h_def mypath'_lcorner_def o_def)
also have "(λε. h ∘ reversepath (mypath'_lcorner False ε)) = mypath'_rcorner False"
by (simp add: mypath'_rcorner_def [abs_def] h_def mypath'_lcorner_def o_def)
also have "(h ` {❙ρ}) = {❙ρ + 1}"
by (auto simp: h_def complex_eq_iff sin_60 cos_60 sin_120 cos_120)
also have "h ` {} = {}"
by auto
also have "h ∘ (part_circlepath 0 1 (pi - arcjunc) (2 * pi / 3) +++ linepath ❙ρ (lv vjunc)) =
(h ∘ part_circlepath 0 1 (pi - arcjunc) (2 * pi / 3)) +++ (h ∘ linepath ❙ρ (lv vjunc))"
by (simp add: path_compose_join)
also have "h ∘ linepath ❙ρ (lv vjunc) =
linepath (- cnj (cis ((2 * pi / 3)))) (rv vjunc)"
by (simp add: h_def o_def fun_eq_iff linepath_cnj lv_def rv_def modfun_rho_def flip: linepath_minus)
also have "h ∘ part_circlepath 0 1 (pi - arcjunc) (2 * pi / 3) = part_circlepath 0 1 arcjunc (pi / 3)"
by (simp add: h_def fun_eq_iff part_circlepath_cnj minus_part_circlepath)
also have "- cnj (cis (2 * pi / 3)) = ❙ρ + 1"
by (auto simp: complex_eq_iff sin_60 cos_60 sin_120 cos_120)
finally show ?thesis .
qed
subsection ‹Putting everything together›
definition mypath' where
"mypath' left ε = (
mypath'_lcorner left ε +++
mypath'_arc left ε +++
mypath'_rcorner left ε +++
mypath'_vert left vjunc b ys ε +++
linepath (rv b) (lv b) +++
mypath'_vert' left vjunc b ys ε)"
definition mypath_shifted :: "real ⇒ complex" where
"mypath_shifted =
(linepath (lv vjunc) ❙ρ +++
part_circlepath 0 1 (2/3*pi) (pi - arcjunc)) +++
part_circlepath 0 1 (pi - arcjunc) arcjunc +++
(part_circlepath 0 1 arcjunc (pi / 3) +++
linepath (❙ρ + 1) (rv vjunc)) +++
linepath (rv vjunc) (rv b) +++
linepath (rv b) (lv b) +++
linepath (lv b) (lv vjunc)"
lemma valid_path_mypath_shifted: "valid_path mypath_shifted"
unfolding mypath_shifted_def
by (intro valid_path_join valid_path_linepath valid_path_part_circlepath)
(simp_all add: complex_eq_iff cos_60 sin_60 cos_120 sin_120
pathfinish_part_circlepath' pathstart_part_circlepath')
lemma eq_loops_mypath_shifted: "mypath b ≡⇩○ mypath_shifted"
proof -
have "mypath b ≡⇩p
(part_circlepath 0 1 (2/3*pi) (pi - arcjunc) +++
part_circlepath 0 1 (pi - arcjunc) arcjunc +++
part_circlepath 0 1 arcjunc (1/3*pi)) +++
(linepath (❙ρ + 1) (1 / 2 + vjunc *⇩R 𝗂) +++
linepath (1 / 2 + vjunc *⇩R 𝗂) (1 / 2 + b *⇩R 𝗂)) +++
linepath (1 / 2 + b *⇩R 𝗂) (-1 / 2 + b *⇩R 𝗂) +++
(linepath (-1 / 2 + b *⇩R 𝗂) (-1 / 2 + vjunc *⇩R 𝗂) +++
linepath (-1 / 2 + vjunc *⇩R 𝗂) ❙ρ)"
unfolding mypath_def using vjunc vjunc_pos arcjunc
by (intro eq_paths_join eq_paths_refl eq_paths_linepaths'
eq_paths_joinpaths_part_circlepath')
(auto simp: rcis_def complex_eq_iff sin_60 cos_60 closed_segment_eq_real_ivl
closed_segment_same_Re pathfinish_part_circlepath' pathstart_part_circlepath')
also have "… ≡⇩○ mypath_shifted"
unfolding mypath_shifted_def
by path (simp_all add: complex_eq_iff sin_60 cos_60 sin_120 cos_120 lv_def rv_def)
finally show ?thesis .
qed
lemma eventually_detour:
"eventually (λε. detour ε I X P (mypath b) mypath_shifted (mypath' True ε)) (at_right 0)"
proof (rule detour_ccw)
show "mypath b ≡⇩○ mypath_shifted"
by (fact eq_loops_mypath_shifted)
show "simple_loop_ccw (mypath b)"
using b_gt simple_loop_ccw_mypath [of b] by simp
show "P ∩ path_image (mypath b) = {}"
unfolding P_def using b_gt subset_zeros_poles
by (subst path_image_mypath_conv_frontier)
(auto simp: closed_segment_same_Im closed_segment_eq_real_ivl frontier_std_fund_region)
show "closed P"
proof -
have *: "A - frontier ℛ⇩Γ sparse_in {z. 0 < Im z}"
using sparse_A by (rule sparse_in_subset2) auto
have "closed (-({z. Im z > 0} - (A - frontier ℛ⇩Γ)))"
by (rule closed_Compl open_diff_sparse_pts open_halfspace_Im_gt *)+
also have "… = P"
by (auto simp: P_def)
finally show "closed P" .
qed
have eq1: "complex_of_real (Im z) * 𝗂 - 1 / 2 = z" if "Re z = - 1 / 2" for z
using that by (auto simp: complex_eq_iff)
have "lv ` Y = S_l"
by (auto simp: S_l_def Y_def lv_def complex_eq_iff scaleR_conv_of_real eq1)
hence [simp]: "lv ` Y = S_l"
by (auto simp: Y_def S_l_def lv_def complex_eq_iff)
have "rv ` Y = (+) 1 ` lv ` Y"
unfolding image_image by (intro image_cong) (auto simp: lv_def rv_def)
hence [simp]: "rv ` Y = (+) 1 ` S_l"
by simp
have [simp]: "x ≠ 0" if "x ∈ ℛ⇩Γ'" for x
using that by (auto simp: in_std_fund_region'_iff)
have [simp]: "sgn z = z" if "norm z = 1" for z :: complex
using that by (simp add: complex_sgn_def)
have [simp]: "S_arc = cis ` Φ ∪ cis ` (λx. pi - x) ` Φ"
by (rule S_arc_decompose)
have "detour_rel
({} ∪ cis ` (λx. pi - x) ` Φ ∪ {} ∪ {} ∪ {} ∪ lv ` set ys)
({❙ρ} ∪ insert 𝗂 (cis ` Φ) ∪ {❙ρ+1} ∪ rv ` set ys ∪ {} ∪ {})
mypath_shifted (mypath' False) (mypath' True)"
unfolding mypath_shifted_def mypath'_def Un_assoc
by (intro detour_rel_join detour_rel_mypath'_lcorner detour_rel_mypath'_rcorner
detour_rel_arc detour_rel_mypath'_vert detour_rel_mypath'_vert'
detour_rel_refl sorted1 sorted2)
(auto simp: pathfinish_part_circlepath' pathstart_part_circlepath')
thus "detour_rel I X mypath_shifted (mypath' False) (mypath' True)"
by (simp add: I_def X_def insert_commute Un_ac phis'_def phis ys image_Un)
qed (fact valid_path_mypath_shifted)
lemmas valid_intros =
valid_path_join valid_path_lcorner valid_path_rcorner
valid_path_mypath'_vert' valid_path_mypath'_vert
lemmas path_intros = valid_intros [THEN valid_path_imp_path]
lemma A_decompose: "A ⊆ I ∪ X ∪ P"
proof
fix z assume z: "z ∈ A"
show "z ∈ I ∪ X ∪ P"
proof (cases "z ∈ frontier ℛ⇩Γ")
case False
hence "z ∈ P"
using z by (auto simp: P_def)
thus ?thesis by blast
next
case True
hence z': "Im z > 0" "norm z ≥ 1"
using True by (auto simp: frontier_std_fund_region)
hence [simp]: "z ≠ 0"
by auto
consider "Re z = 1 / 2" | "Re z = -1 / 2" | "norm z = 1" "¦Re z¦ < 1 / 2"
using True unfolding frontier_std_fund_region
by (force simp: abs_if split: if_splits)
thus ?thesis
proof cases
assume z'': "Re z = -1 / 2"
have "z ∈ I ∪ X"
using z'' z' ‹z ∈ A› ‹Im z > 0›
by (auto simp: I_def X_def S_l_def closure_std_fund_region)
thus ?thesis by blast
next
assume z'': "Re z = 1 / 2"
define y where "y = Im z"
have z_eq: "z = 1 / 2 + y * 𝗂"
by (simp add: complex_eq_iff y_def z'')
have norm_z_minus_1: "norm (z - 1) = norm z"
by (simp add: norm_complex_def z_eq)
show ?thesis
proof (cases "z = ❙ρ + 1")
case False
hence "z - 1 ≠ ❙ρ"
by Groebner_Basis.algebra
hence "z - 1 ∈ S_l"
using ‹z ∈ A› z' norm_z_minus_1 A_invariant1[of "z - 1"]
by (auto simp: S_l_def closure_std_fund_region z'' )
hence "z ∈ (+) 1 ` S_l"
by (rule rev_image_eqI) auto
thus ?thesis
by (auto simp: X_def)
qed (auto simp: X_def)
next
assume z'': "norm z = 1" "¦Re z¦ < 1 / 2"
show ?thesis
proof (cases "z = 𝗂")
case False
hence "z ∈ S_arc"
using z ‹z ∈ frontier _› z'' by (auto simp: S_arc_def frontier_def)
also note S_arc_decompose
finally show ?thesis
by (auto simp: X_def I_def)
qed (auto simp: X_def)
qed
qed
qed
lemma Int_cong1: "(⋀x. x ∈ A ⟹ x ∈ B ⟷ x ∈ C) ⟹ A ∩ B = A ∩ C"
by blast
lemma S_l_in_region: "S_l ⊆ ℛ⇩Γ'"
using closure_std_fund_region_Im_pos
unfolding S_l_def closure_std_fund_region std_fund_region'_def
by (auto simp: in_std_fund_region_iff)
lemma S_r_not_in_region: "(+) 1 ` S_l ∩ ℛ⇩Γ' = {}"
using closure_std_fund_region_Im_pos
unfolding S_l_def closure_std_fund_region std_fund_region'_def
by (auto simp: in_std_fund_region_iff)
lemma S_arc_left_in_region: "(λφ. cis (pi - φ)) ` Φ ⊆ ℛ⇩Γ'"
proof safe
fix φ assume "φ ∈ Φ"
hence "φ ∈ {pi/3<..<pi/2}"
using Φ_subset by auto
thus "cis (pi - φ) ∈ ℛ⇩Γ'"
by (subst cis_in_std_fund_region'_iff) auto
qed
lemma S_arc_right_not_in_region: "cis ` Φ ∩ ℛ⇩Γ' = {}"
proof safe
fix φ assume "φ ∈ Φ" "cis φ ∈ ℛ⇩Γ'"
hence "φ ∈ {pi/3<..<pi/2}"
using Φ_subset by auto
hence "cis φ ∉ ℛ⇩Γ'"
by (subst cis_in_std_fund_region'_iff) auto
with ‹cis φ ∈ ℛ⇩Γ'› show "cis φ ∈ {}"
by contradiction
qed
lemma I_subset_region: "I ⊆ ℛ⇩Γ'"
unfolding I_def using S_arc_left_in_region S_l_in_region by auto
lemma X_inter_region_eq: "X ∩ ℛ⇩Γ' = {❙ρ, 𝗂}"
unfolding X_def using S_arc_right_not_in_region S_r_not_in_region
by auto
definition err :: "real ⇒ complex" where
"err ε = k * 𝗂 * (pi / 6 - 4 * arcsin (ε / 2))"
lemma eventually_between_0_and_onehalf:
"eventually (λx. x ∈ {0<..<1/2}) (at_right (0 :: real))"
by (intro eventually_at_right_real) auto
lemma integral_eq1:
"eventually (λε. (∑p←[mypath'_circ1 ε, mypath'_circ2 ε, mypath'_circ3 ε, mypath'_line b].
contour_integral p f) + err ε =
of_real (2 * pi) * 𝗂 * (∑z∈A ∩ ℛ⇩Γ'-{𝗂, ❙ρ}. zorder g z)) (at_right 0)"
using eventually_detour eventually_between_0_and_onehalf
proof eventually_elim
case (elim ε)
interpret detour ε I X P "mypath b" mypath_shifted "mypath' True ε"
by (rule elim)
have [simp]: "valid_path (mypath'_arc True ε)"
using valid unfolding mypath'_def by auto
hence [simp]: "path (mypath'_arc True ε)"
by (rule valid_path_imp_path)
have [simp]: "cnj ❙ρ = -❙ρ - 1"
by (simp add: complex_eq_iff cos_60 sin_60)
note [simp] = pathfinish_part_circlepath' pathstart_part_circlepath'
have "arcsin (ε / 2) > 0"
using elim(2) by (auto intro!: arcsin_pos)
moreover have "arcsin (ε / 2) < arcsin (1 / 2)"
using elim by (subst arcsin_less_mono) auto
ultimately have arcsin: "arcsin (ε / 2) > 0" "arcsin (ε / 2) < pi / 6"
by auto
have "path_image (mypath' True ε) ⊆ {z. Im z > 0}"
using P_not_on_path by (force simp: P_def)
moreover have "path_image (mypath' True ε) ∩ A = {}"
using A_decompose I_not_on_path X_not_on_path P_not_on_path by blast
ultimately have subset: "path_image (mypath' True ε) ⊆ {z. Im z > 0} - A"
by blast
have subset': "path_image p ⊆ {z. Im z > 0} - A" if "p ≤⇩p mypath' True ε" for p
using that is_subpath_imp_path_image_subset subset by blast
define β where "β = pi / 3 + arcsin (ε / 2)"
define err1 where "err1 = k * 𝗂 * (pi/3 + 2 * arcsin (ε / 2) - arcjunc)"
define err2 where "err2 = k * 𝗂 * (arcjunc - arcjunc')"
define err3 where "err3 = k * 𝗂 * (arcjunc' + 2 * arcsin (ε / 2) - pi / 2)"
define plc where "plc = mypath'_lcorner True ε"
define plc' where "plc' = part_circlepath ❙ρ ε (pi / 2) (pi / 6 - arcsin (ε / 2))"
define prc where "prc = mypath'_rcorner True ε"
define prc' where "prc' = (λz. -z) ∘ (cnj ∘ reversepath plc')"
define pa where "pa = mypath'_arc True ε"
define pam2 where "pam2 = part_circlepath 𝗂 ε (pi + arcsin (ε / 2)) (- arcsin (ε / 2))"
define pr where "pr = mypath'_vert True vjunc b ys ε"
define pu where "pu = linepath (rv b) (lv b)"
define pl where "pl = mypath'_vert' True vjunc b ys ε"
note defs = plc_def pa_def prc_def pr_def pu_def pl_def
write contour_integral ("∫⇩c")
have [simp, intro]: "valid_path plc" "valid_path prc"
unfolding defs using elim by (auto intro!: valid_intros)
note [simp] = valid_path_cnj contour_integral_negatepath contour_integral_cnj
contour_integral_reversepath contour_integral_translate
rcis_def scaleR_conv_of_real
have [simp]: "cnj (cis (pi * 2 / 3)) = -cis (pi / 3)"
by (auto simp: complex_eq_iff cos_120' sin_120' cos_60 sin_60)
note [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1
have inside_eq:"A ∩ inside (path_image (mypath' True ε))
= A ∩ (ℛ⇩Γ' - {❙ρ, 𝗂})"
proof (intro Int_cong1)
fix z assume "z ∈ A"
hence "Im z > 0" "Im z < b"
using subset_zeros_poles by auto
from ‹z ∈ A› have "z ∈ I ∪ X ∪ P"
using A_decompose by blast
thus "z ∈ inside (path_image (mypath' True ε)) ⟷ z ∈ ℛ⇩Γ' - {❙ρ, 𝗂}"
proof (elim UnE)
assume z: "z ∈ I"
hence "z ∈ inside (path_image (mypath' True ε))"
using I_inside by auto
moreover from z have "z ∉ {❙ρ, 𝗂}"
using I_X_disjoint ‹z ∈ I› by (auto simp: X_def)
moreover have "z ∈ ℛ⇩Γ'"
using I_subset_region ‹z ∈ I› by auto
ultimately show ?thesis by blast
next
assume z: "z ∈ X"
hence "z ∈ outside (path_image (mypath' True ε))"
using X_outside by auto
hence "z ∉ inside (path_image (mypath' True ε))"
by (meson disjoint_iff inside_Int_outside)
moreover have "z ∉ ℛ⇩Γ' - {❙ρ, 𝗂}"
using ‹z ∈ X› X_inter_region_eq by auto
ultimately show ?thesis by blast
next
assume z: "z ∈ P"
hence "z ∉ {❙ρ, 𝗂}"
using X_P_disjoint unfolding X_def by blast
hence "z ∈ inside (path_image (mypath' True ε)) ⟷ z ∈ inside (path_image (mypath b))"
by (intro P_inside_iff z)
also have "inside (path_image (mypath b)) = ℛ⇩Γ ∩ {z. Im z < b}"
by (intro inside_mypath b_gt)
also have "z ∈ … ⟷ z ∈ ℛ⇩Γ"
using ‹Im z < b› by auto
also from ‹z ∈ P› and ‹Im z > 0› have "z ∉ frontier ℛ⇩Γ"
by (auto simp: P_def)
hence "z ∈ ℛ⇩Γ ⟷ z ∈ ℛ⇩Γ'"
by (rule in_std_fund_region'_not_on_frontier_iff [symmetric])
finally show ?thesis
using ‹z ∉ {❙ρ, 𝗂}› by blast
qed
qed
have "contour_integral (mypath' True ε) f =
of_real (2 * pi) * 𝗂 * (∑z∈A ∩ inside (path_image (mypath' True ε)). zorder g z)"
unfolding f_def
proof (rule argument_principle_ccw_analytic)
show "eval_mero_uhp g analytic_on {z. Im z > 0} - A"
using A_def analytic_on_eval_mero_uhp by force
show "valid_path (mypath' True ε)" by simp
have "simple_loop_orientation (mypath' True ε) = 1"
using same_orientation simple_loop_orientation_mypath[of b] b_gt by simp
thus "simple_loop_ccw (mypath' True ε)"
by (auto simp: simple_loop_orientation_def split: if_splits)
show "path_image (mypath' True ε) ⊆ {z. 0 < Im z} - A"
by (rule subset)
have "z ∉ inside (path_image (mypath' True ε))" if z: "Im z ≤ 0" for z
proof -
from z have "z ∈ P"
by (auto simp: P_def)
hence "winding_number (mypath' True ε) z = winding_number (mypath b) z"
using winding_number_unchanged by simp
also have "… = 0"
using z closure_std_fund_region_Im_pos by (intro winding_number_mypath_outside b_gt) auto
finally show ?thesis
using ‹z ∈ P› P_not_on_path simple_loop
simple_closed_path_norm_winding_number_inside[of "mypath' True ε" z] by auto
qed
thus "inside (path_image (mypath' True ε)) ⊆ {z. 0 < Im z}"
by force
show "∀p∈A. not_essential (eval_mero_uhp g) p"
by (metis (no_types, lifting) A_def analytic_on_eval_mero_uhp
is_pole_imp_not_essential mem_Collect_eq mem_simps(3)
not_essential_analytic singletonD)
show "A sparse_in {z. 0 < Im z}" using sparse_A by auto
show "⋀z. z ∈ {z. 0 < Im z} - A ⟹ eval_mero_uhp g z ≠ 0"
using A_def by blast
qed
also have "A ∩ inside (path_image (mypath' True ε)) = A ∩ (ℛ⇩Γ' - {❙ρ, 𝗂})"
proof (intro Int_cong1)
fix z assume "z ∈ A"
hence "Im z > 0" "Im z < b"
using subset_zeros_poles by auto
from ‹z ∈ A› have "z ∈ I ∪ X ∪ P"
using A_decompose by blast
thus "z ∈ inside (path_image (mypath' True ε)) ⟷ z ∈ ℛ⇩Γ' - {❙ρ, 𝗂}"
proof (elim UnE)
assume z: "z ∈ I"
hence "z ∈ inside (path_image (mypath' True ε))"
using I_inside by auto
moreover from z have "z ∉ {❙ρ, 𝗂}"
using I_X_disjoint ‹z ∈ I› by (auto simp: X_def)
moreover have "z ∈ ℛ⇩Γ'"
using I_subset_region ‹z ∈ I› by auto
ultimately show ?thesis by blast
next
assume z: "z ∈ X"
hence "z ∈ outside (path_image (mypath' True ε))"
using X_outside by auto
hence "z ∉ inside (path_image (mypath' True ε))"
by (meson disjoint_iff inside_Int_outside)
moreover have "z ∉ ℛ⇩Γ' - {❙ρ, 𝗂}"
using ‹z ∈ X› X_inter_region_eq by auto
ultimately show ?thesis by blast
next
assume z: "z ∈ P"
hence "z ∉ {❙ρ, 𝗂}"
using X_P_disjoint unfolding X_def by blast
hence "z ∈ inside (path_image (mypath' True ε)) ⟷ z ∈ inside (path_image (mypath b))"
by (intro P_inside_iff z)
also have "inside (path_image (mypath b)) = ℛ⇩Γ ∩ {z. Im z < b}"
by (intro inside_mypath b_gt)
also have "z ∈ … ⟷ z ∈ ℛ⇩Γ"
using ‹Im z < b› by auto
also from ‹z ∈ P› and ‹Im z > 0› have "z ∉ frontier ℛ⇩Γ"
by (auto simp: P_def)
hence "z ∈ ℛ⇩Γ ⟷ z ∈ ℛ⇩Γ'"
by (rule in_std_fund_region'_not_on_frontier_iff [symmetric])
finally show ?thesis
using ‹z ∉ {❙ρ, 𝗂}› by blast
qed
qed
also have "… = A ∩ ℛ⇩Γ'-{❙ρ, 𝗂}"
by blast
finally have "contour_integral (mypath' True ε) f =
of_real (2 * pi) * 𝗂 * of_int (sum (zorder g) (A ∩ ℛ⇩Γ'-{❙ρ, 𝗂}))"
by simp
also have "contour_integral (mypath' True ε) f =
(∫⇩c plc f + ∫⇩c prc f) + (∫⇩c pl f + ∫⇩c pr f) + ∫⇩c pa f + ∫⇩c pu f"
unfolding mypath'_def
proof (path, fold mypath'_def)
show "f analytic_on path_image (mypath' True ε)"
by (rule f_analytic) (use subset in auto)
qed (use elim subset in ‹auto intro!: valid_intros sorted1 sorted2 simp: defs add_ac›)
also have "∫⇩c pl f + ∫⇩c pr f = 0"
proof -
have "∫⇩c pl f = - ∫⇩c pr (λx. f (x - 1))"
unfolding pl_def pr_def mypath'_vert'_def
by (subst contour_integral_reversepath)
(auto intro!: valid_intros sorted1 sorted2
simp: contour_integral_translate valid_path_translation_eq)
also have "∫⇩c pr (λx. f (x - 1)) = ∫⇩c pr f"
proof (intro contour_integral_cong refl)
fix z assume z: "z ∈ path_image pr"
have "pr ≤⇩p mypath' True ε"
unfolding pr_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
from subset' [OF this] and z have "Im z > 0 ∧ z ∉ A"
by auto
with f_invariant(1)[of "z - 1"] A_invariant1[of "z - 1"] show "f (z - 1) = f z"
by auto
qed
finally show ?thesis
by simp
qed
also have "∫⇩c plc f + ∫⇩c prc f = ∫⇩c plc' f + ∫⇩c prc' f - err1"
proof -
have ends1: "cis (2 * pi / 3) + complex_of_real ε * cis (pi / 6 - arcsin (ε / 2)) =
cis (2 * pi / 3 - 2 * arcsin (ε / 2))"
proof -
interpret avoid_linepath_circlepath_locale vjunc "pi - arcjunc" ε
by unfold_locales (use elim in auto)
show ?thesis
using ends(1) ends(2)[of False] by (auto simp: bad_def α_def β_def)
qed
define plc1 where "plc1 = linepath (- 1 / 2 + vjunc *⇩R 𝗂) (cis (2 * pi / 3) + ε *⇩R 𝗂)"
define plc2 where "plc2 = part_circlepath 0 1 (2 * pi / 3 - 2 * arcsin (ε / 2)) (pi - arcjunc)"
define prc1 where "prc1 = (λx. -x) ∘ (cnj ∘ reversepath plc1)"
define prc2 where "prc2 = (λx. -x) ∘ (cnj ∘ reversepath plc2)"
have [simp]: "pathfinish plc1 = pathstart plc'" "pathfinish plc' = pathstart plc2"
using ends1 by (simp_all add: plc1_def plc'_def plc2_def modfun_rho_def)
have plc_eq: "plc = plc1 +++ plc' +++ plc2"
unfolding plc_def mypath'_lcorner_def avoid_linepath_circlepath_def Let_def
plc1_def plc2_def plc'_def modfun_rho_def by simp
have [simp, intro]: "valid_path plc1" "valid_path plc2"
using ‹valid_path plc› unfolding plc_eq by auto
have "plc1 ≤⇩p plc" unfolding plc_eq
by path (use ends1 in ‹auto simp: plc1_def plc'_def plc2_def modfun_rho_def›)
also have "plc ≤⇩p mypath' True ε"
unfolding plc_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
finally have subpath_plc1: "plc1 ≤⇩p …" .
have "plc2 ≤⇩p plc" unfolding plc_eq
by path (use ends1 in ‹auto simp: plc1_def plc'_def plc2_def modfun_rho_def›)
also have "plc ≤⇩p mypath' True ε"
unfolding plc_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
finally have subpath_plc2: "plc2 ≤⇩p …" .
have "prc = (λz. - cnj z) ∘ reversepath (plc1 +++ plc' +++ plc2)"
using plc_eq by (simp add: prc_def plc_def mypath'_rcorner_def)
also have "reversepath (plc1 +++ plc' +++ plc2) = reversepath (plc' +++ plc2) +++ reversepath plc1"
by (subst reversepath_joinpaths)
(auto simp: prc1_def o_def plc1_def plc'_def modfun_rho_def)
also have "reversepath (plc' +++ plc2) = reversepath plc2 +++ reversepath plc'"
using ends1 by (subst reversepath_joinpaths) (auto simp: plc'_def plc2_def modfun_rho_def)
also have "(λz. -cnj z) ∘ (… +++ reversepath plc1) = (prc2 +++ prc') +++ prc1"
unfolding path_compose_join by (simp add: prc2_def prc'_def prc1_def o_def)
finally have prc_eq: "prc = (prc2 +++ prc') +++ prc1" .
have "∫⇩c prc f = ∫⇩c prc1 f + ∫⇩c prc' f + ∫⇩c prc2 f"
unfolding prc_eq
proof (path, fold prc_eq)
have "prc ≤⇩p mypath' True ε"
unfolding prc_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
from subset' [OF this] have "path_image prc ⊆ {z. Im z > 0} - A"
by auto
thus "f analytic_on path_image prc"
by (rule f_analytic)
qed (use ends1 in ‹auto simp: prc1_def prc'_def prc2_def rcis_def pathfinish_compose
pathstart_compose scaleR_conv_of_real modfun_rho_def valid_path_cnj plc2_def
plc'_def plc1_def›)
also have "prc1 = (+) 1 ∘ reversepath plc1"
unfolding prc1_def plc1_def
by (auto simp: complex_eq_iff cos_120' sin_120' cos_60 sin_60 fun_eq_iff
linepath_def reversepath_def algebra_simps scaleR_conv_of_real)
also have "∫⇩c … f = - ∫⇩c plc1 (λx. f (x + 1))"
by simp
also have "∫⇩c plc1 (λx. f (x + 1)) = ∫⇩c plc1 f"
proof (intro contour_integral_cong refl)
fix z assume z: "z ∈ path_image plc1"
from subset' [OF subpath_plc1] and z have "Im z > 0 ∧ z ∉ A"
by auto
with f_invariant(1)[of z] show "f (z + 1) = f z"
by blast
qed
also have "prc2 = uminus ∘ (cnj ∘ reversepath plc2)"
unfolding prc2_def ..
also have "… = (λz. -1/z) ∘ reversepath plc2"
by (auto simp: fun_eq_iff reversepath_def plc2_def part_circlepath_altdef divide_conv_cnj)
also have "∫⇩c … f = ∫⇩c (reversepath plc2) (λw. deriv (λz. -1 / z) w * f (- 1 / w))"
proof (rule contour_integral_comp_analyticW)
show "(λz. -1 / z) analytic_on {z. Im z > 0}"
by (intro analytic_intros) auto
from subset' [OF subpath_plc2] show "path_image (reversepath plc2) ⊆ {z. 0 < Im z}"
by auto
qed (auto simp: plc2_def)
also have "… = - ∫⇩c plc2 (λw. deriv (λz. -1 / z) w * f (- 1 / w))"
by simp
also have "∫⇩c plc2 (λw. deriv (λz. -1 / z) w * f (- 1 / w)) =
∫⇩c plc2 (λw. f w + k / w)"
proof (intro contour_integral_cong refl)
fix z assume "z ∈ path_image plc2"
with subset'[OF subpath_plc2] have z: "Im z > 0 ∧ z ∉ A"
by auto
from z have [simp]: "z ≠ 0"
by auto
from z have "deriv (λz. -1 / z) z * f (-1 / z) = f (-1 / z) / z ^ 2"
by (subst deriv_divide) auto
also have "… = (f z * z ^ 2 + k * z) / z ^ 2"
using z by (subst f_invariant(2)) auto
also have "(f z * z⇧2 + of_int k * z) / z⇧2 = f z + k / z"
by (simp add: field_simps power2_eq_square)
finally show "deriv (λz. -1 / z) z * f (-1 / z) = f z + k / z" .
qed
also have "… = ∫⇩c plc2 f + ∫⇩c plc2 (λw. k / w)"
using subset'[OF subpath_plc2]
by (subst contour_integral_add)
(auto intro!: analytic_imp_contour_integrable analytic_intros f_analytic)
also have "∫⇩c plc2 (λw. k / w) = k * ln (pathfinish plc2) - k * ln (pathstart plc2)"
(is "_ = ?rhs")
proof -
have "((λw. k / w) has_contour_integral ?rhs) plc2"
proof (rule contour_integral_primitive)
show "path_image plc2 ⊆ {z. 0 < Im z} - A"
using subset'[OF subpath_plc2] .
qed (auto intro!: derivative_eq_intros simp: field_simps elim!: nonpos_Reals_cases)
thus ?thesis
using contour_integral_unique by blast
qed
also have "… = k * (ln (cis (pi - arcjunc)) - ln (cis (2 * pi / 3 - 2 * arcsin (ε / 2))))"
by (simp add: plc2_def algebra_simps)
also have "… = err1"
using arcjunc arcsin by (subst (1 2) ln_cis) (auto simp: field_simps err1_def)
finally have int_prc_eq: "∫⇩c prc f = ∫⇩c prc' f - ∫⇩c plc1 f - ∫⇩c plc2 f - err1"
by simp
have "∫⇩c plc f = ∫⇩c plc1 f + ∫⇩c plc' f + ∫⇩c plc2 f"
unfolding plc_eq
proof (path, fold plc_eq)
have "plc ≤⇩p mypath' True ε"
unfolding plc_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
from subset' [OF this] have "path_image plc ⊆ {z. Im z > 0} - A"
by auto
thus "f analytic_on path_image plc"
by (rule f_analytic)
qed (use ends1 in ‹auto simp: plc1_def plc'_def plc2_def rcis_def
scaleR_conv_of_real modfun_rho_def›)
with int_prc_eq show ?thesis
by simp
qed
also have "∫⇩c pa f = ∫⇩c pam2 f - err2 - err3"
proof -
define pal where "pal = mypath'_arcl True (ε / 2)"
define pam where "pam = mypath'_arcm True ε"
define par where "par = mypath'_arcr True (ε / 2)"
have val [simp, intro]: "valid_path pal" "valid_path par" "valid_path pam"
using ‹valid_path (mypath'_arc True ε)›
unfolding mypath'_arc_def pal_def par_def pam_def by auto
hence [simp]: "path pal" "path par" "path pam"
using valid_path_imp_path by blast+
have pa_eq: "pa = pal +++ pam +++ par"
by (simp add: pa_def pal_def pam_def par_def mypath'_arc_def)
have [simp]: "pathfinish pal = pathstart pam" "pathfinish pam = pathstart par"
by (simp_all add: pal_def pam_def par_def)
define pam1 where "pam1 = part_circlepath 0 1 (pi - arcjunc') (pi / 2 + 2 * arcsin (ε / 2))"
define pam3 where "pam3 = part_circlepath 0 1 (pi / 2 - 2 * arcsin (ε / 2)) arcjunc'"
interpret pam: avoid_part_circlepath_locale 0 1 "pi - arcjunc'" arcjunc' "pi/2" ε
by standard (use elim arcjunc(1) arcjunc'(1) in auto)
have pam_eq: "pam = pam1 +++ pam2 +++ pam3"
using arcjunc(1) arcjunc'(1)
by (simp add: pam_def pam1_def pam2_def pam3_def mypath'_arcm_def
avoid_part_circlepath_def Let_def)
have ends: "𝗂 + complex_of_real ε * cis (- arcsin (ε / 2)) = cis (pi / 2 - 2 * arcsin (ε / 2))"
"cis (pi / 2 + 2 * arcsin (ε / 2)) = 𝗂 + complex_of_real ε * cis (pi + arcsin (ε / 2))"
using pam.ends(1)[of True] pam.ends(2) arcjunc(1) arcjunc'(1)
by (auto simp: pam.bad_def pam.s_def pam.α_def pam.β_def)
have "par ≤⇩p pa"
unfolding pa_eq by path auto
also have "… ≤⇩p mypath' True ε"
unfolding pa_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
finally have "par ≤⇩p mypath' True ε" .
from subset' [OF this] have par_subset: "path_image (reversepath par) ⊆ {z. Im z > 0} - A"
by auto
have "pam ≤⇩p pa"
unfolding pa_eq by path auto
also have "… ≤⇩p mypath' True ε"
unfolding pa_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
finally have "pam ≤⇩p mypath' True ε" .
from subset' [OF this] have pam_subset: "path_image (reversepath pam) ⊆ {z. Im z > 0} - A"
by auto
have "pam1 ≤⇩p pam"
unfolding pam_eq by path (use ends in ‹auto simp: pam1_def pam2_def pam3_def›)
also have "… ≤⇩p mypath' True ε"
by fact
finally have "pam1 ≤⇩p mypath' True ε" .
from subset' [OF this] have pam1_subset: "path_image pam1 ⊆ {z. Im z > 0} - A"
by auto
have valid_pam1 [simp, intro]: "valid_path pam1"
unfolding pam1_def by auto
have valid_pam1': "valid_path ((λz. -(1/z)) ∘ pam1)"
by (intro valid_path_compose_holomorphic[OF _ _ _ pam1_subset] holomorphic_intros)
(auto simp: open_halfspace_Im_gt pam1_def)
have "∫⇩c pa f = ∫⇩c pal f + ∫⇩c par f + ∫⇩c pam f"
unfolding pa_def mypath'_arc_def
proof (path, fold pa_def mypath'_arc_def)
have "pa ≤⇩p mypath' True ε"
unfolding pa_def mypath'_def
by path (use elim in ‹auto intro!: path_intros sorted1 sorted2›)
from subset' [OF this] have "path_image pa ⊆ {z. Im z > 0} - A"
by auto
thus "f analytic_on path_image pa"
by (rule f_analytic)
qed (use val[unfolded pal_def par_def pam_def] in ‹auto simp: pal_def par_def pam_def›)
also have "∫⇩c pal f = - ∫⇩c par (λw. deriv (λz. - (1 / z)) w * f (- (1 / w)))"
unfolding pal_def mypath'_arcl_def par_def [symmetric]
proof (subst contour_integral_comp_analyticW)
show "(λz. -(1/z)) analytic_on {z. Im z > 0}"
by (auto simp: open_halfspace_Im_gt intro!: analytic_intros)
qed (use par_subset in auto)
also have "∫⇩c par (λw. deriv (λz. - (1 / z)) w * f (- (1 / w))) = ∫⇩c par (λw. f w + k / w)"
proof (intro contour_integral_cong refl)
fix z assume "z ∈ path_image par"
with par_subset have z: "Im z > 0" "z ∉ A"
by auto
from z have [simp]: "z ≠ 0"
by auto
from z have "deriv (λz. -1 / z) z * f (-1 / z) = f (-1 / z) / z ^ 2"
by (subst deriv_divide) auto
also have "… = (f z * z ^ 2 + k * z) / z ^ 2"
using z by (subst f_invariant(2)) auto
also have "(f z * z⇧2 + of_int k * z) / z⇧2 = f z + k / z"
by (simp add: field_simps power2_eq_square)
finally show "deriv (λz. - (1 / z)) z * f (- (1 / z)) = f z + of_int k / z"
by simp
qed
also have "… = ∫⇩c par f + ∫⇩c par (λw. k / w)"
using par_subset
by (subst contour_integral_add)
(auto intro!: analytic_imp_contour_integrable analytic_intros f_analytic)
also have "∫⇩c par (λw. k / w) = k * ln (pathfinish par) - k * ln (pathstart par)"
(is "_ = ?rhs")
proof -
have "((λw. k / w) has_contour_integral ?rhs) par"
proof (rule contour_integral_primitive)
show "path_image par ⊆ {z. 0 < Im z} - A"
using par_subset by auto
qed (auto intro!: derivative_eq_intros simp: field_simps elim!: nonpos_Reals_cases)
thus ?thesis
using contour_integral_unique by blast
qed
also have "… = k * (ln (cis arcjunc) - ln (cis arcjunc'))"
by (simp add: par_def algebra_simps)
also have "… = err2"
using arcjunc arcjunc' by (subst (1 2) ln_cis) (auto simp: field_simps err2_def)
also have "∫⇩c pam f = ∫⇩c pam1 f + ∫⇩c pam2 f + ∫⇩c pam3 f"
unfolding pam_eq
proof (path, fold pam_eq)
show "f analytic_on path_image pam"
by (rule f_analytic) (use pam_subset in auto)
qed (use ends in ‹auto simp: pam1_def pam2_def pam3_def›)
also have "pam3 = reversepath ((λz. -(1/z)) ∘ pam1)"
by (auto simp: pam3_def pam1_def fun_eq_iff part_circlepath_altdef linepath_def ring_distribs
add_divide_distrib diff_divide_distrib reversepath_def mult_ac
simp flip: cis_mult cis_divide)
also have "∫⇩c … f = -∫⇩c ((λz. -(1/z)) ∘ pam1) f"
by (subst contour_integral_reversepath) (use valid_pam1' in auto)
also have "∫⇩c ((λz. -(1/z)) ∘ pam1) f = ∫⇩c pam1 (λw. deriv (λz. - (1 / z)) w * f (- (1 / w)))"
proof (subst contour_integral_comp_analyticW)
show "(λz. -(1/z)) analytic_on {z. Im z > 0}"
by (auto simp: open_halfspace_Im_gt intro!: analytic_intros)
qed (use pam1_subset in ‹auto simp: pam1_def›)
also have "… = ∫⇩c pam1 (λw. f w + k / w)"
proof (intro contour_integral_cong refl)
fix z assume "z ∈ path_image pam1"
with pam1_subset have z: "Im z > 0" "z ∉ A"
by auto
from z have [simp]: "z ≠ 0"
by auto
from z have "deriv (λz. -1 / z) z * f (-1 / z) = f (-1 / z) / z ^ 2"
by (subst deriv_divide) auto
also have "… = (f z * z ^ 2 + k * z) / z ^ 2"
using z by (subst f_invariant(2)) auto
also have "(f z * z⇧2 + of_int k * z) / z⇧2 = f z + k / z"
by (simp add: field_simps power2_eq_square)
finally show "deriv (λz. - (1 / z)) z * f (- (1 / z)) = f z + of_int k / z"
by simp
qed
also have "… = ∫⇩c pam1 f + ∫⇩c pam1 (λw. k / w)"
using pam1_subset
by (subst contour_integral_add)
(auto intro!: analytic_imp_contour_integrable analytic_intros f_analytic)
also have "∫⇩c pam1 (λw. k / w) = k * ln (pathfinish pam1) - k * ln (pathstart pam1)"
(is "_ = ?rhs")
proof -
have "((λw. k / w) has_contour_integral ?rhs) pam1"
proof (rule contour_integral_primitive)
show "path_image pam1 ⊆ {z. 0 < Im z} - A"
using pam1_subset by auto
qed (auto intro!: derivative_eq_intros simp: field_simps elim!: nonpos_Reals_cases)
thus ?thesis
using contour_integral_unique by blast
qed
also have "… = k * (ln (cis (pi / 2 + 2 * arcsin (ε / 2))) - ln (cis (pi - arcjunc')))"
by (simp add: pam1_def algebra_simps)
also have "… = err3"
using arcjunc' arcsin by (subst (1 2) ln_cis) (auto simp: field_simps err3_def)
finally show ?thesis
by simp
qed
also have "∫⇩c plc' f + ∫⇩c prc' f - err1 + 0 + (∫⇩c pam2 f - err2 - err3) + ∫⇩c pu f =
∫⇩c plc' f + ∫⇩c prc' f + ∫⇩c pam2 f + ∫⇩c pu f + -(err1 + err2 + err3)"
by (simp add: algebra_simps)
also have "-(err1 + err2 + err3) = err ε"
unfolding err1_def err2_def err3_def err_def by (simp add: field_simps)
also have i_times_cis: "𝗂 * cis x = cis (x + pi / 2)" for x
by (simp flip: cis_mult)
have "cnj (cis (pi / 3)) = -cis (2 * pi / 3)" "cis (5 / 6 * pi) = 𝗂 * cis (pi / 3)"
by (simp_all add: complex_eq_iff cos_60 cos_120 sin_60 sin_120 i_times_cis)
hence "prc' = part_circlepath (❙ρ + 1) ε (5 * pi / 6 + arcsin (ε / 2)) (pi / 2)"
unfolding prc'_def plc'_def
by (auto simp: fun_eq_iff part_circlepath_altdef linepath_def ring_distribs add_divide_distrib
diff_divide_distrib reversepath_def mult_ac divide_conv_cnj
simp flip: cis_mult cis_divide )
finally show ?case
by (simp add: plc'_def pam2_def pu_def mypath'_circ1_def mypath'_circ2_def mypath'_circ3_def
mypath'_line_def add_ac rv_def lv_def insert_commute)
qed
lemma circ1:
"((λε. contour_integral (mypath'_circ1 ε) f) ⤏ -of_int (zorder g ❙ρ) * 𝗂 * pi / 3) (at_right 0)"
unfolding mypath'_circ1_def f_def
proof (rule contour_integral_logderiv_part_circlepath_not_essential)
have "❙ρ + 1 ∈ {z. Im z > 0}"
by auto
show "eval_mero_uhp g meromorphic_on {❙ρ + 1}"
by (auto intro!: meromorphic_intros)
show "eventually (λw. g w ≠ 0) (at (❙ρ + 1))"
using eval_mero_uhp_avoid_0[OF g_nonzero]
by (auto simp: eventually_cosparse_open_eq open_halfspace_Im_gt)
show "((λε. 5 * pi / 6 + arcsin (ε / 2)) ⤏ 5 * pi / 6) (at_right 0)"
by (auto intro!: tendsto_eq_intros)
show "((λε::real. pi / 2) ⤏ pi / 2) (at_right 0)"
by (rule tendsto_const)
have "zorder g (❙ρ + 1) = zorder (λw. g (w + 1)) ❙ρ"
by (simp add: zorder_shift' algebra_simps)
also have "… = zorder g ❙ρ"
proof (rule zorder_cong)
have "eventually (λw. w ∈ ({w. Im w > 0} - (A - {❙ρ})) - {❙ρ}) (at ❙ρ)"
by (intro eventually_at_in_open open_A_compl_subset) auto
thus "eventually (λw. g (w + 1) = g w) (at ❙ρ)"
by eventually_elim (auto simp: g_plus1)
qed auto
finally show "-of_int (zorder g ❙ρ) * 𝗂 * complex_of_real pi / 3 =
(real_of_int (zorder g (❙ρ + 1)) * (pi / 2 - 5 * pi / 6)) *⇩R 𝗂"
by (simp add: scaleR_conv_of_real)
qed
lemma circ2:
"((λε. contour_integral (mypath'_circ2 ε) f) ⤏ -of_int (zorder g ❙ρ) * 𝗂 * pi / 3) (at_right 0)"
unfolding mypath'_circ2_def f_def
proof (rule contour_integral_logderiv_part_circlepath_not_essential)
have "❙ρ ∈ {z. Im z > 0}"
by auto
show "eval_mero_uhp g meromorphic_on {❙ρ}"
by (auto intro!: meromorphic_intros)
show "eventually (λw. g w ≠ 0) (at ❙ρ)"
using eval_mero_uhp_avoid_0[OF g_nonzero]
by (auto simp: eventually_cosparse_open_eq open_halfspace_Im_gt)
show "((λε::real. pi / 2) ⤏ pi / 2) (at_right 0)"
by (rule tendsto_const)
show "((λε. pi / 6 - arcsin (ε / 2)) ⤏ pi / 6) (at_right 0)"
by (auto intro!: tendsto_eq_intros)
qed (auto simp: field_simps scaleR_conv_of_real)
lemma circ3:
"((λε. contour_integral (mypath'_circ3 ε) f) ⤏ -of_int (zorder g 𝗂) * 𝗂 * pi) (at_right 0)"
unfolding mypath'_circ3_def f_def
proof (rule contour_integral_logderiv_part_circlepath_not_essential)
have "𝗂 ∈ {z. Im z > 0}"
by auto
show "eval_mero_uhp g meromorphic_on {𝗂}"
by (auto intro!: meromorphic_intros)
show "eventually (λw. g w ≠ 0) (at 𝗂)"
using eval_mero_uhp_avoid_0[OF g_nonzero]
by (auto simp: eventually_cosparse_open_eq open_halfspace_Im_gt)
show "((λε::real. pi + arcsin (ε / 2)) ⤏ pi) (at_right 0)"
by (auto intro!: tendsto_eq_intros)
show "((λε. -arcsin (ε / 2)) ⤏ 0) (at_right 0)"
by (auto intro!: tendsto_eq_intros)
qed (auto simp: field_simps scaleR_conv_of_real)
lemma err: "(err ⤏ k * 𝗂 * pi / 6) (at_right 0)"
unfolding err_def by (auto intro!: tendsto_eq_intros)
lemma integral_eq2:
"contour_integral (mypath'_line b) f =
of_real (2 * pi) * 𝗂 * (-of_int k / 12 + of_int (zorder g ❙ρ) / 3 + of_int (zorder g 𝗂) / 2 +
(∑z∈A∩ℛ⇩Γ'-{𝗂,❙ρ}. of_int (zorder g z)))"
proof -
note [tendsto_intros] = circ1 circ2 circ3
note [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1
define I where
"I = (λε. (∑p←[mypath'_circ1 ε, mypath'_circ2 ε, mypath'_circ3 ε]. contour_integral p f) + err ε)"
define C1 where
"C1 = -2 * 𝗂 * of_real pi * (of_int (zorder g ❙ρ) / 3 + of_int (zorder g 𝗂) / 2 - of_int k / 12)"
define C2 where
"C2 = of_real (2 * pi) * 𝗂 * (∑z∈A∩ℛ⇩Γ'-{𝗂,❙ρ}. of_int (zorder g z)) - contour_integral (mypath'_line b) f"
have "C1 = C2"
proof (rule tendsto_unique)
show "(I ⤏ C1) (at_right 0)"
unfolding sum_list.Cons sum_list.Nil list.map add_0_right C1_def I_def
by (rule tendsto_eq_intros err refl)+ (auto simp: field_simps)
next
have "eventually (λε. I ε = C2) (at_right 0)"
using integral_eq1 unfolding C2_def I_def by eventually_elim (auto simp: algebra_simps)
thus "(I ⤏ C2) (at_right 0)"
using tendsto_eventually by blast
qed auto
thus "contour_integral (mypath'_line b) f =
of_real (2 * pi) * 𝗂 * (-of_int k / 12 + of_int (zorder g ❙ρ) / 3 + of_int (zorder g 𝗂) / 2 +
(∑z∈A∩ℛ⇩Γ'-{𝗂,❙ρ}. of_int (zorder g z)))"
by (simp add: C1_def C2_def algebra_simps)
qed
end
text ‹Theorem 6.1›
theorem MeForms_valence_formula:
assumes "f ∈ MeForms[k] - {0}"
shows "(∑z∈zeros_mero_uhp f ∪ poles_mero_uhp f - {𝗂,❙ρ}. real_of_int (zorder f z)) +
of_int (zorder f ❙ρ) / 3 + of_int (zorder f 𝗂) / 2 + of_int (zorder_at_ii_inf 1 f) =
of_int k / 12"
proof -
interpret meromorphic_form_full f k
proof -
interpret meromorphic_form f k UNIV
using assms by auto
show "meromorphic_form_full f k" ..
qed
from assms have [simp]: "f ≠ 0"
by auto
define f' where "f' = fourier_expansion (Suc 0) f"
let ?γ = mypath'_line
let ?ord = "λz. zorder f z"
define A where "A = {z. Im z > 0 ∧ (eval_mero_uhp f z = 0 ∨ is_pole f z)}"
define h where "h = (λb. contour_integral (?γ b) (λz. deriv f z / f z))"
define C where "C = 2 * pi * 𝗂 * ((∑z∈A∩ℛ⇩Γ'-{𝗂, ❙ρ}. ?ord z) - k / 12 + ?ord ❙ρ / 3 + ?ord 𝗂 / 2)"
define g where "g = (λz. deriv f z / f z)"
define g' where "g' = (λz. deriv f' z / f' z)"
define circ where "circ = (λb. part_circlepath 0 (exp (-2*pi*b)) pi (-pi))"
define Z where "Z = zeros_mero_uhp f ∪ poles_mero_uhp f"
let ?q = "to_q (Suc 0)"
have [simp]: "deriv ?q z = 2 * complex_of_real pi * 𝗂 * ?q z" for z
by (subst deriv_to_q) auto
have "eventually (λz. f z ≠ 0 ∧ ¬is_pole f z ∧ Im z > 1) at_𝗂∞"
using ‹f ≠ 0› by (intro eventually_conj eventually_neq_at_ii_inf eventually_no_poles_at_ii_inf eventually_at_ii_inf) auto
then obtain b0 where b0: "⋀z. Im z ≥ b0 ⟹ f z ≠ 0 ∧ ¬is_pole f z ∧ Im z > 1"
unfolding eventually_at_ii_inf_iff' by blast
from b0[of "𝗂 * of_real b0"] have "b0 > 1"
by simp
have "C = -2 * of_real pi * 𝗂 * of_int (zorder_at_ii_inf 1 f)"
proof (rule tendsto_unique)
show "(h ⤏ -2 * of_real pi * 𝗂 * of_int (zorder_at_ii_inf 1 f)) at_top"
proof (rule Lim_transform_eventually)
show "eventually (λb. contour_integral (circ b) g' = h b) at_top"
using eventually_gt_at_top[of 0] eventually_gt_at_top[of b0]
proof eventually_elim
case (elim b)
have "contour_integral (?γ b) (λz. deriv f z / f z) =
contour_integral (?γ b)
(λz. deriv f' (?q z) / f' (?q z) * (of_real (2 * pi) * 𝗂 * ?q z))"
proof (intro contour_integral_cong refl, goal_cases)
case (1 z)
hence [simp]: "Im z = b"
by (auto simp: mypath'_line_def closed_segment_same_Im)
have "deriv f' (?q z) / f' (?q z) * (complex_of_real (2 * pi) * 𝗂 * ?q z) =
eval_mero_uhp (deriv_mero_uhp f) z / eval_mero_uhp f z"
using elim b0[of z] unfolding f'_def by (subst deriv_fourier[OF _ _ refl]) auto
also have "eval_mero_uhp (deriv_mero_uhp f) z = deriv (eval_mero_uhp f) z"
using elim b0[of z]by (simp add: eval_deriv_mero_uhp)
finally show ?case ..
qed
also have "… = contour_integral (?q ∘ ?γ b) g'"
unfolding g'_def
by (subst contour_integral_comp_analyticW[of _ UNIV])
(auto intro!: analytic_intros simp: mypath'_line_def mult_ac)
also have "?q ∘ ?γ b = circ b"
unfolding circ_def
apply (rule ext)
apply (simp add: circ_def to_q_def o_def mypath'_line_def part_circlepath_def)
apply (simp add: scaleR_conv_of_real algebra_simps linepath_def exp_add exp_diff exp_minus of_real_exp)
apply (simp add: field_simps)
done
finally show ?case
by (simp add: h_def)
qed
next
show "((λb. contour_integral (circ b) g') ⤏ -2 * of_real pi * 𝗂 * of_int (zorder_at_ii_inf 1 f)) at_top"
unfolding circ_def g'_def
proof (rule filterlim_compose, rule contour_integral_logderiv_part_circlepath_not_essential)
show "filterlim (λb::real. exp (-2 * pi * b)) (at_right 0) at_top"
by real_asymp
show "f' meromorphic_on {0}" unfolding f'_def
by (intro meromorphic_intros) auto
show "eventually (λz. f' z ≠ 0) (at 0)" unfolding f'_def
by (simp add: eventually_neq_fourier)
show "-2 * of_real pi * 𝗂 * of_int (zorder_at_ii_inf 1 f) =
(real_of_int (zorder f' 0) * (-pi - pi)) *⇩R 𝗂"
using zorder_at_ii_inf_conv_fourier by (simp add: scaleR_conv_of_real f'_def)
qed auto
qed
next
have "eventually (λb. A ⊆ {z. Im z < b}) at_top"
proof -
show ?thesis
using eventually_gt_at_top[of b0]
proof eventually_elim
case (elim b)
have "A ⊆ {z. Im z ≤ b0}"
using b0 elim unfolding A_def
by (force simp: inv_image_mero_uhp_def poles_mero_uhp_def)
also have "… ⊆ {z. Im z < b}"
using elim by force
finally show ?case .
qed
qed
hence "eventually (λb. h b = C) at_top"
using eventually_gt_at_top[of b0]
proof eventually_elim
case (elim b)
interpret mypath_detour f k A b
proof unfold_locales
show "f ≠ 0"
by fact
show "b > 1"
using elim ‹b0 > 1› by simp
show "{z. 0 < Im z ∧ eval_mero_uhp f z = 0} ∪ {z. 0 < Im z ∧ is_pole (eval_mero_uhp f) z}
⊆ {z. Im z ∈ {0<..<b}}"
using not_is_pole_eval_mero_uhp_outside[of _ f] b0 elim by force
show "A ≡ {z. 0 < Im z ∧ eval_mero_uhp f z = 0} ∪ {z. Im z > 0 ∧ is_pole (eval_mero_uhp f) z}"
using not_is_pole_eval_mero_uhp_outside[of _ f] b0 elim unfolding A_def
by (force intro!: eq_reflection)
qed
from integral_eq2 show ?case
by (simp add: f_def h_def C_def algebra_simps)
qed
thus "(h ⤏ C) at_top"
by (simp add: tendsto_eventually)
qed auto
hence "-of_int (zorder_at_ii_inf 1 f) = C / (2 * of_real pi * 𝗂)"
by simp
also have "… = (∑z∈A∩ℛ⇩Γ'-{𝗂,❙ρ}. ?ord z) - k / 12 + ?ord ❙ρ / 3 + ?ord 𝗂 / 2"
by (simp add: C_def)
also have "(∑z∈A∩ℛ⇩Γ'-{𝗂,❙ρ}. ?ord z) = (∑z∈Z-{𝗂,❙ρ}. ?ord z)"
proof (intro sum.mono_neutral_right ballI)
have "A ∩ ℛ⇩Γ' - {𝗂, ❙ρ} ⊆ zeros_mero_uhp f ∪ poles_mero_uhp f"
by (auto simp: A_def inv_image_mero_uhp_def poles_mero_uhp_def)
moreover have "finite (zeros_mero_uhp f ∪ poles_mero_uhp f)"
using ‹f ≠ 0› by auto
ultimately show "finite (A ∩ ℛ⇩Γ' - {𝗂, ❙ρ})"
using finite_subset by blast
next
fix z assume z: "z ∈ A ∩ ℛ⇩Γ' - {𝗂, ❙ρ} - (Z - {𝗂, ❙ρ})"
hence z': "Im z > 0" "z ∉ Z"
by (auto simp: in_std_fund_region'_iff)
thus "zorder f z = 0"
unfolding Z_def using z by (auto simp: inv_image_mero_uhp_def poles_mero_uhp_def)
next
have "z ∈ Z - {𝗂, ❙ρ} ⟶ z ∈ A ∩ ℛ⇩Γ' - {𝗂, ❙ρ}" for z
using not_is_pole_eval_mero_uhp_outside[of z f]
by (cases "Im z > 0")
(auto simp: A_def Z_def inv_image_mero_uhp_def poles_mero_uhp_def in_std_fund_region'_iff)
thus "Z - {𝗂, ❙ρ} ⊆ A ∩ ℛ⇩Γ' - {𝗂, ❙ρ}"
by blast
qed
finally show ?thesis
by (simp add: complex_eq_iff Z_def)
qed
lemma MeForms_valence_formula':
assumes "f ∈ MeForms[k] - {0}"
defines "C ≡ (∑z∈zeros_mero_uhp f ∪ poles_mero_uhp f - {𝗂, ❙ρ}. zorder_mero_uhp f z)"
shows "12 * C + 4 * zorder_mero_uhp f ❙ρ + 6 * zorder_mero_uhp f 𝗂 + 12 * zorder_at_ii_inf 1 f = k"
(is "?lhs = _")
proof -
have "12 * (real_of_int k / 12) = ?lhs"
by (subst MeForms_valence_formula[OF assms(1), symmetric]) (simp add: algebra_simps C_def)
also have "12 * (real_of_int k / 12) = k"
by simp
finally show ?thesis
by linarith
qed
lemma MForms_valence_formula':
assumes "f ∈ MForms[k] - {0}"
defines "C ≡ (∑z∈zeros_mero_uhp f - {𝗂, ❙ρ}. zorder_mero_uhp f z)"
shows "12 * C + 4 * zorder_mero_uhp f ❙ρ + 6 * zorder_mero_uhp f 𝗂 + 12 * zorder_at_ii_inf 1 f = k"
proof -
interpret modular_form f k UNIV
using assms(1) by auto
have f': "f ∈ MeForms[k] - {0}"
using assms(1) by (auto simp: MeForms_def meromorphic_form_axioms)
from assms have "poles_mero_uhp f = {}"
by (auto simp: poles_mero_uhp_def)
thus ?thesis
using MeForms_valence_formula'[OF f'] by (simp add: C_def)
qed
end