Theory Detour_Prerequisites
section ‹Prerequisites for the Detour Calculus›
theory Detour_Prerequisites
imports
"HOL-Complex_Analysis.Residue_Theorem"
"Winding_Number_Eval.Missing_Analysis"
"Winding_Number_Eval.Missing_Transcendental"
"Path_Automation.Path_Automation"
Path_Nhds
"HOL-Library.Real_Mod"
begin
subsection ‹Miscellaneous›
lemma inverse_conv_cnj: "norm z = 1 ⟹ inverse z = cnj z"
by (simp add: divide_conv_cnj inverse_eq_divide)
lemma dist_cnj: "dist (cnj x) (cnj y) = dist x y"
by (simp add: dist_norm norm_complex_def power2_commute)
lemma closed_segment_cnj: "closed_segment (cnj w) (cnj z) = cnj ` closed_segment w z"
using closed_segment_linear_image linear_cnj by blast
lemma closed_segment_mult:
"(*) (c :: 'a :: real_algebra_1) ` closed_segment a b = closed_segment (c * a) (c * b)"
by (rule closed_segment_linear_image [symmetric]) auto
lemma arcsin_pos: "x ∈ {0<..1} ⟹ arcsin x > 0"
by (metis arcsin_0 arcsin_less_arcsin greaterThanAtMost_iff neg_le_0_iff_le zero_less_one_class.zero_le_one)
lemma sin_lt_zero': "x ∈ {-pi<..<0} ⟹ sin x < 0"
by (metis greaterThanLessThan_iff minus_less_iff neg_0_less_iff_less sin_gt_zero sin_minus)
lemma tan_arcsin: "x ∈ {-1..1} ⟹ tan (arcsin x) = x / sqrt (1 - x ^ 2)"
by (simp add: tan_def cos_arcsin)
lemma Arg_neg_real [simp]: "Im x = 0 ⟹ Re x < 0 ⟹ Arg x = pi"
using Arg_eq_pi by blast
lemma cis_eq_1_iff':
assumes "¦x¦ < 2 * pi"
shows "cis x = 1 ⟷ x = 0"
proof
assume "cis x = 1"
then obtain n where n: "x = of_int n * 2 * pi"
by (auto simp: cis_eq_1_iff)
with assms have "n = 0"
by (auto simp: abs_mult simp flip: of_int_abs)
with n show "x = 0"
by simp
qed auto
lemma DeMoivre_int: "cis x powi n = cis (of_int n * x)"
proof (cases "n ≥ 0")
case True
hence "cis x powi n = cis x ^ nat n"
by (simp add: power_int_def)
also have "… = cis (real (nat n) * x)"
by (rule Complex.DeMoivre)
finally show ?thesis
using True by simp
next
case False
hence "cis x powi n = cis (-x) ^ nat (-n)"
by (simp add: power_int_def)
also have "… = cis (-real (nat (-n)) * x)"
by (subst Complex.DeMoivre) auto
finally show ?thesis
using False by simp
qed
lemma cis_of_int_times_pi_half: "cis (of_int n * pi / 2) = 𝗂 powi n"
using DeMoivre_int[of "pi / 2" n] by simp
lemma cis_of_nat_times_pi_half: "cis (real n * pi / 2) = 𝗂 ^ n"
using cis_of_int_times_pi_half[of "int n"] by simp
lemma cis_of_int_times_pi: "cis (of_int n * pi) = (-1) powi n"
using DeMoivre_int[of pi n] by simp
lemma cis_of_nat_times_pi: "cis (real n * pi) = (-1) ^ n"
using cis_of_int_times_pi[of "int n"] by simp
lemma power3_i [simp]: "𝗂 ^ 3 = -𝗂"
and power4_i [simp]: "𝗂 ^ 4 = 1"
by (simp_all add: eval_nat_numeral)
lemma i_power_mod4: "𝗂 ^ n = 𝗂 ^ (n mod 4)"
proof -
have "𝗂 ^ n = 𝗂 ^ (4 * (n div 4) + n mod 4)"
by simp
also have "… = 𝗂 ^ (n mod 4)"
by (subst power_add) (simp add: power_mult)
finally show ?thesis .
qed
lemma cis_numeral_times_pi_half [simp]:
"cis (numeral num * pi / 2) = 𝗂 ^ (numeral num mod 4)"
proof -
have "cis (numeral num * pi / 2) = 𝗂 ^ numeral num"
using cis_of_nat_times_pi_half[of "numeral num"] by simp
also have "… = 𝗂 ^ (numeral num mod 4)"
by (rule i_power_mod4)
finally show ?thesis .
qed
lemma cis_numeral_pi_times_numeral_half [simp]:
"cis (pi * numeral num / 2) = 𝗂 ^ (numeral num mod 4)"
by (subst mult.commute) simp
lemma cis_numeral_times_pi [simp]:
"cis (numeral num * pi) = (-1) ^ (numeral num mod 2)"
proof -
have "cis (numeral num * pi) = (-1) ^ numeral num"
using cis_of_nat_times_pi[of "numeral num"] by simp
also have "… = (-1) ^ (numeral num mod 2)"
by (metis even_mod_2_iff neg_one_even_power neg_one_odd_power)
finally show ?thesis .
qed
lemma cis_pi_times_numeral [simp]:
"cis (pi * numeral num) = (-1) ^ (numeral num mod 2)"
by (subst mult.commute) simp
lemma cis_minus_numeral_times_pi_half [simp]:
"cis (-(numeral num * pi / 2)) = (-𝗂) ^ (numeral num mod 4)"
by (subst cis_cnj [symmetric]) auto
lemma cis_minus_numeral_times_pi [simp]:
"cis (-(numeral num * pi)) = (-1) ^ (numeral num mod 2)"
by (subst cis_cnj [symmetric]) auto
lemma cis_minus_pi_times_numeral_half [simp]:
"cis (-(pi * numeral num / 2)) = (-𝗂) ^ (numeral num mod 4)"
by (subst cis_cnj [symmetric]) auto
lemma cis_minus_pi_times_numeral_pi [simp]:
"cis (-(pi * numeral num)) = (-1) ^ (numeral num mod 2)"
by (subst cis_cnj [symmetric]) auto
lemma cis_minus_pi [simp]: "cis (-pi) = -1"
by (simp flip: cis_cnj)
lemma inner_mult_both_complex: "(z * x :: complex) ∙ (z * y) = norm z ^ 2 * (x ∙ y)"
unfolding cmod_power2 by (simp add: inner_complex_def algebra_simps power2_eq_square)
lemma orthogonal_transformation_mult_complex [intro]:
"norm z = 1 ⟹ orthogonal_transformation ((*) (z :: complex))"
unfolding orthogonal_transformation_def
by (auto intro!: linear_times simp: inner_mult_both_complex)
lemma contour_integral_affine:
assumes "valid_path γ" "c ≠ 0"
shows "contour_integral ((λx. c * x + b) ∘ γ) f = contour_integral γ (λw. c * f (c * w + b))"
proof -
define ff where "ff=(λx. c*x+b)"
have "contour_integral (ff ∘ γ) f = contour_integral γ (λw. deriv ff w * f (ff w))"
proof (rule contour_integral_comp_analyticW)
show "ff analytic_on UNIV" "path_image γ ⊆ UNIV" "valid_path γ"
unfolding ff_def using ‹valid_path γ›
by (auto intro: analytic_intros)
qed
also have "… = contour_integral γ (λw. c * f (c * w + b))"
proof -
have "deriv ff x = c" "ff x = c*x+b" for x
unfolding ff_def by auto
then show ?thesis by auto
qed
finally show ?thesis unfolding ff_def .
qed
lemma finite_imp_eventually_sparse_at_0:
assumes "finite X"
shows "eventually (λε. sparse ε X) (at_right 0)"
proof (cases "X = {} ∨ is_singleton X")
case False
hence ne: "Sigma X (λx. X - {x}) ≠ {}"
unfolding is_singleton_def by auto
define m where "m = Min ((λ(x,y). dist x y) ` (Sigma X (λx. X - {x})))"
have "m > 0"
unfolding m_def using ne by (subst Min_gr_iff) (use assms in auto)
show ?thesis
using eventually_at_right_real[OF ‹m > 0›]
proof eventually_elim
case (elim ε)
show ?case
proof (intro sparseI)
fix x y assume xy: "x ∈ X" "y ∈ X" "x ≠ y"
have "ε < m"
using elim by simp
also have "m ≤ dist x y"
using xy unfolding m_def by (intro Min.coboundedI) (use assms in auto)
finally show "dist x y > ε" .
qed
qed
qed (auto elim!: is_singletonE)
subsection ‹Lipschitz continuity›
lemma complex_derivative_on_convex_imp_lipschitz:
fixes f' :: "complex ⇒ complex"
assumes deriv: "⋀z. z ∈ A ⟹ (f has_field_derivative f' z) (at z within A)"
assumes A: "convex A" and C: "⋀x. x ∈ A ⟹ norm (f' x) ≤ C" "C ≥ 0"
shows "C-lipschitz_on A f"
proof (rule lipschitz_onI)
fix x y assume xy: "x ∈ A" "y ∈ A"
let ?l = "linepath y x"
have "(f' has_contour_integral f (pathfinish ?l) - f (pathstart ?l)) ?l"
proof (rule contour_integral_primitive)
show "(f has_field_derivative f' z) (at z within A)" if "z ∈ A" for z
using deriv[OF that] .
show "path_image (linepath y x) ⊆ A"
unfolding path_image_linepath by (intro closed_segment_subset xy A)
qed auto
hence "norm (f (pathfinish ?l) - f (pathstart ?l)) ≤ C * norm (x - y)"
proof (rule has_contour_integral_bound_linepath)
fix z assume "z ∈ closed_segment y x"
also have "closed_segment y x ⊆ A"
by (intro closed_segment_subset xy A)
finally show "norm (f' z) ≤ C"
using C(1)[of z] by auto
qed fact+
thus "dist (f x) (f y) ≤ C * dist x y"
by (simp add: dist_norm norm_minus_commute)
qed fact+
lemma analytic_on_compact_convex_imp_lipschitz:
assumes "f analytic_on A" "convex A" "compact A"
obtains C where "C-lipschitz_on A f"
proof -
have "deriv f analytic_on A"
by (intro analytic_intros assms)
define C where "C = Sup (norm ` (insert 0 (deriv f ` A)))"
have "compact (insert 0 (deriv f ` A))"
by (intro compact_insert compact_continuous_image analytic_imp_holomorphic
holomorphic_on_imp_continuous_on analytic_intros assms)
hence "bounded (insert 0 (deriv f ` A))"
by (rule compact_imp_bounded)
hence bdd: "bdd_above (norm ` insert 0 (deriv f ` A))"
unfolding bdd_above_norm .
show ?thesis
proof (rule that[of C], rule complex_derivative_on_convex_imp_lipschitz)
show "C ≥ 0"
unfolding C_def by (intro cSup_upper bdd) auto
next
show "(f has_field_derivative deriv f z) (at z within A)" if "z ∈ A" for z
using that assms(1) analytic_on_holomorphic holomorphic_derivI by blast
next
show "norm (deriv f z) ≤ C" if "z ∈ A" for z
proof -
have "norm (deriv f z) ∈ norm ` insert 0 (deriv f ` A)"
using that by auto
moreover have "norm ` insert 0 (deriv f ` A) ≠ {}"
by blast
ultimately show "norm (deriv f z) ≤ C"
unfolding C_def using bdd by (intro cSup_upper)
qed
qed fact+
qed
lemma lipschitz_on_complex_inverse:
assumes "C > 0"
shows "(1/C^2)-lipschitz_on {z. Im z ≥ C} (λz. inverse z :: complex)"
proof (rule complex_derivative_on_convex_imp_lipschitz)
show "((λz. inverse z :: complex) has_field_derivative (-1 / z ^ 2)) (at z within {z. Im z ≥ C})"
if "z ∈ {z. Im z ≥ C}" for z
using that assms by (auto intro!: derivative_eq_intros simp: power2_eq_square field_simps)
show "convex {z. Im z ≥ C}"
by (simp add: convex_halfspace_Im_ge)
show "cmod (- 1 / z⇧2) ≤ 1 / C⇧2" if "z ∈ {z. Im z ≥ C}" for z
proof -
from that and assms have [simp]: "z ≠ 0"
by auto
have "C ^ 2 ≤ Im z ^ 2"
using assms that by (intro power_mono) auto
also have "… ≤ norm z ^ 2"
unfolding cmod_power2 by simp
finally show ?thesis
using assms by (simp add: field_simps norm_divide norm_power)
qed
qed (use assms in auto)
lemma lipschitz_on_cnj [lipschitz_intros]:
fixes f::"'a::metric_space ⇒ complex"
assumes "C-lipschitz_on U f"
shows "C-lipschitz_on U (λx. cnj (f x))"
proof (rule lipschitz_onI)
fix x y assume xy: "x ∈ U" "y ∈ U"
have "dist (cnj (f x)) (cnj (f y)) = norm (cnj (f x) - cnj (f y))"
by (simp add: dist_norm)
also have "cnj (f x) - cnj (f y) = cnj (f x - f y)"
by simp
also have "norm … = dist (f x) (f y)"
by (subst complex_mod_cnj) (auto simp: dist_norm)
also have "… ≤ C * dist x y"
by (rule lipschitz_onD[OF assms]) fact+
finally show "dist (cnj (f x)) (cnj (f y)) ≤ C * dist x y"
by (simp add: mult_ac)
qed (use assms lipschitz_on_nonneg in blast)
lemma lipschitz_on_cmult_complex [lipschitz_intros]:
fixes f::"'a::metric_space ⇒ complex"
assumes "C-lipschitz_on U f"
shows "(norm c * C)-lipschitz_on U (λx. c * f x)"
proof (rule lipschitz_onI)
have "C ≥ 0"
using assms lipschitz_on_nonneg by blast
thus "norm c * C ≥ 0"
by simp
next
fix x y assume xy: "x ∈ U" "y ∈ U"
have "dist (c * f x) (c * f y) = norm c * dist (f x) (f y)"
by (metis dist_norm norm_mult vector_space_over_itself.scale_right_diff_distrib)
also have "… ≤ norm c * (C * dist x y)"
by (intro mult_left_mono lipschitz_onD[OF assms]) (use xy in auto)
finally show "dist (c * f x) (c * f y) ≤ cmod c * C * dist x y"
by (simp add: mult_ac)
qed
lemma lipschitz_on_cmult_complex' [lipschitz_intros]:
fixes f::"'a::metric_space ⇒ complex"
assumes "C-lipschitz_on U f" "C' ≥ norm c * C"
shows "C'-lipschitz_on U (λx. c * f x)"
using lipschitz_on_cmult_complex[OF assms(1), of c] assms(2) lipschitz_on_le by blast
lemma lipschitz_on_cadd_left [lipschitz_intros]:
fixes f :: "_ ⇒ 'b :: real_normed_vector"
assumes "C-lipschitz_on A f"
shows "C-lipschitz_on A (λx. c + f x)"
proof (rule lipschitz_onI)
fix x y assume "x ∈ A" "y ∈ A"
thus "dist (c + f x) (c + f y) ≤ C * dist x y"
using lipschitz_onD[OF assms, of x y] by (simp add: dist_norm)
qed (use assms lipschitz_on_nonneg in blast)
lemma lipschitz_on_cadd_right [lipschitz_intros]:
fixes f :: "_ ⇒ 'b :: real_normed_vector"
assumes "C-lipschitz_on A f"
shows "C-lipschitz_on A (λx. f x + c)"
by (subst add.commute, rule lipschitz_on_cadd_left [OF assms])
subsection ‹Homotopy›
lemma simply_connected_imp_homotopic_paths:
fixes S :: "'a :: real_normed_vector set"
assumes "simply_connected S" "path p" "path_image p ⊆ S" "path q" "path_image q ⊆ S"
assumes "pathstart q = pathstart p ∧ pathfinish q = pathfinish p"
shows "homotopic_paths S p q"
using assms unfolding simply_connected_eq_homotopic_paths by blast
lemma homotopic_loops_part_circlepath_circlepath:
assumes "b = a + 2 * pi" "sphere x r ⊆ A" "r ≥ 0"
shows "homotopic_loops A (part_circlepath x r a b) (circlepath x r)"
proof -
have "homotopic_loops A (shiftpath' (a / (2 * pi)) (circlepath x r)) (circlepath x r)"
using assms by (intro homotopic_loops_shiftpath'_left) auto
also have "shiftpath' (a / (2 * pi)) (circlepath x r) = part_circlepath x r a ((a / pi + 2) * pi)"
by (simp add: shiftpath'_circlepath)
also have "(a / pi + 2) * pi = b"
using assms by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1)
finally show ?thesis .
qed
lemma homotopic_loops_reversepath_D:
"homotopic_loops A p q ⟹ homotopic_loops A (reversepath p) (reversepath q)"
apply (simp add: homotopic_loops_def homotopic_with_def, clarify)
apply (rule_tac x="h ∘ (λx. (fst x, 1 - snd x))" in exI)
apply (rule conjI continuous_intros)+
apply (auto simp: reversepath_def pathstart_def pathfinish_def elim!: continuous_on_subset)
done
lemma homotopic_loops_reversepath:
"homotopic_loops A (reversepath p) (reversepath q) ⟷ homotopic_loops A p q"
using homotopic_loops_reversepath_D reversepath_reversepath by metis
lemmas [trans] = homotopic_loops_trans
lemma homotopic_paths_split:
assumes p: "path p" and A: "path_image p ⊆ A"
assumes a: "a ∈ {0..1}"
assumes eq1: "⋀x. x ∈ {0..1} ⟹ p1 x = subpath 0 a p x"
assumes eq2: "⋀x. x ∈ {0..1} ⟹ p2 x = subpath a 1 p x"
shows "homotopic_paths A p (p1 +++ p2)"
proof -
have "homotopic_paths (path_image p) (subpath 0 a p +++ subpath a 1 p) (subpath 0 1 p)"
by (rule homotopic_join_subpaths) (use a p in auto)
hence "homotopic_paths (path_image p) (subpath 0 1 p) (subpath 0 a p +++ subpath a 1 p)"
by (simp add: homotopic_paths_sym_eq)
also have "homotopic_paths (path_image p) (subpath 0 a p +++ subpath a 1 p) (p1 +++ p2)"
using assms
apply (intro homotopic_paths_eq)
apply auto
apply (subst (asm) path_image_join)
apply auto
apply (auto simp: joinpaths_def path_image_def split: if_splits)
apply (metis (no_types, opaque_lifting) atLeastAtMost_iff image_subset_iff le_numeral_extra(3) path_image_def path_image_subpath_subset zero_less_one_class.zero_le_one)
apply (metis (full_types) atLeastAtMost_iff image_subset_iff le_numeral_extra(4) path_image_def path_image_subpath_subset zero_less_one_class.zero_le_one)
done
also have "subpath 0 1 p = p"
by simp
finally show ?thesis
by (rule homotopic_paths_subset) fact
qed
subsection ‹Winding numbers›
lemma winding_number_comp_plus:
assumes "path γ" "z ∉ path_image γ"
shows "winding_number ((+) c ∘ γ) (z + c) = winding_number γ z"
proof (rule winding_number_unique)
define f where "f = (λx. c+x)"
have f_alt:"f = (λx. x+c)" unfolding f_def by auto
show "∃p. winding_number_prop (f ∘ γ)
(z + c) e p (winding_number γ z)"
if "e>0" for e
proof -
obtain p where "winding_number_prop γ z e p (winding_number γ z)"
using ‹0 < e› assms winding_number by blast
then have p:"valid_path p" "z ∉ path_image p"
"pathstart p = pathstart γ"
"pathfinish p = pathfinish γ"
"(∀t∈{0..1}. cmod (γ t - p t) < e)" and
p_cont:"contour_integral p (λw. 1 / (w - z)) =
complex_of_real (2 * pi) * 𝗂 * winding_number γ z"
unfolding winding_number_prop_def by auto
have "valid_path (f ∘ p)"
using p(1) unfolding f_def valid_path_translation_eq by simp
moreover have "z + c ∉ path_image (f ∘ p)"
using p(2) unfolding f_def by (auto simp add:path_image_def)
moreover have "pathstart (f ∘ p) = pathstart (f ∘ γ)"
using p(3) by (simp add:pathstart_compose)
moreover have "pathfinish (f ∘ p) = pathfinish (f ∘ γ)"
using p(4) by (simp add:pathfinish_compose)
moreover have "(∀t∈{0..1}. cmod ((f ∘ γ) t
- (f ∘ p) t) < e)"
using p(5) unfolding f_def by simp
moreover have "contour_integral (f ∘ p)
(λw. 1 / (w - (z + c))) =
complex_of_real (2 * pi) * 𝗂 * winding_number γ z"
unfolding f_alt
apply (subst contour_integral_affine[where c=1,simplified])
using p_cont p(1,2) by auto
ultimately show ?thesis
apply (rule_tac x="f ∘ p" in exI)
unfolding winding_number_prop_def by auto
qed
show "path (f ∘ γ)"
using ‹path γ› unfolding f_def by (simp add:path_translation_eq)
show "z + c ∉ path_image (f ∘ γ)"
using ‹z ∉ path_image γ› unfolding path_image_def f_def by auto
qed
lemma winding_number_comp_times:
assumes "path γ"
and "z ∉ path_image γ"
and "c ≠ 0"
shows "winding_number ((*) c ∘ γ) (z * c) = winding_number γ z"
proof (rule winding_number_unique)
define f where "f = (λx. c*x)"
have f_alt:"f = (λx. x*c)" unfolding f_def by auto
show "∃p. winding_number_prop (f ∘ γ)
(z * c) e p (winding_number γ z)"
if "e>0" for e
proof -
have "cmod c>0" using ‹c≠0› by simp
then have "(1/cmod c) * e>0"
using that by auto
from winding_number[OF assms(1,2) this]
obtain p where "winding_number_prop γ z ((1/cmod c) * e)
p (winding_number γ z)"
by blast
then have p:"valid_path p" "z ∉ path_image p"
"pathstart p = pathstart γ"
"pathfinish p = pathfinish γ"
"(∀t∈{0..1}. cmod (γ t - p t) < ((1/cmod c) * e))" and
p_cont:"contour_integral p (λw. 1 / (w - z)) =
complex_of_real (2 * pi) * 𝗂 * winding_number γ z"
unfolding winding_number_prop_def by auto
have "valid_path (f ∘ p)"
using p(1) ‹c≠0› valid_path_times
unfolding f_def by auto
moreover have "z * c ∉ path_image (f ∘ p)"
using p(2) ‹c≠0› unfolding f_def
by (auto simp add:path_image_def)
moreover have "pathstart (f ∘ p) = pathstart (f ∘ γ)"
using p(3) by (simp add:pathstart_compose)
moreover have "pathfinish (f ∘ p) = pathfinish (f ∘ γ)"
using p(4) by (simp add:pathfinish_compose)
moreover have "cmod ((f ∘ γ) t - (f ∘ p) t) < e"
if "t∈{0..1}" for t
proof -
have "cmod ((f ∘ γ) t - (f ∘ p) t) = cmod (c*(γ t - p t))"
unfolding f_def by (auto simp:algebra_simps)
also have "… = cmod c * cmod (γ t - p t)"
by (auto simp:norm_mult)
also have "… < cmod c * (1 / cmod c * e)"
using p(5)[rule_format,OF that] ‹cmod c>0›
using mult_less_cancel_left_pos by blast
also have "… = e"
using ‹cmod c>0› by auto
finally show ?thesis .
qed
moreover have "contour_integral (f ∘ p)
(λw. 1 / (w - (z * c))) =
complex_of_real (2 * pi) * 𝗂 * winding_number γ z" (is "?L=?R")
proof -
have "?L = contour_integral p (λw. c / (c * (w - z)))"
unfolding f_def
apply (subst contour_integral_affine[where b=0,simplified])
using p(1,2) ‹c≠0› by (auto simp:algebra_simps)
also have "… = contour_integral p (λw. 1 / ( w - z))"
using ‹c≠0› by simp
also have "… = ?R" using p_cont .
finally show ?thesis .
qed
ultimately show ?thesis
apply (rule_tac x="f ∘ p" in exI)
unfolding winding_number_prop_def by auto
qed
show "path (f ∘ γ)"
using path_mult[OF path_const ‹path γ›] unfolding f_def comp_def
by simp
show "z * c ∉ path_image (f ∘ γ)"
using ‹z ∉ path_image γ› ‹c≠0›
unfolding path_image_def f_def by auto
qed
lemma winding_number_part_circlepath_full:
assumes "y ∈ ball x r" "α + 2 * pi = β"
shows "winding_number (part_circlepath x r α β) y = 1"
proof -
have "0 ≤ dist x y"
by auto
also have "… < r"
using assms by auto
finally have "r > 0" .
have "homotopic_loops (-{y}) (part_circlepath x r α (α + 2 * pi)) (circlepath x r)"
by (rule homotopic_loops_part_circlepath_circlepath) (use assms ‹r > 0› in auto)
hence "winding_number (part_circlepath x r α (α + 2 * pi)) y = winding_number (circlepath x r) y"
by (rule winding_number_homotopic_loops)
also have "… = 1"
by (intro winding_number_circlepath) (use assms in ‹auto simp: dist_norm norm_minus_commute›)
also have "α + 2 * pi = β"
using assms(2) by (simp add: algebra_simps)
finally show ?thesis .
qed
lemma winding_number_part_circlepath_full':
assumes "y ∈ ball x r" "α - 2 * pi = β"
shows "winding_number (part_circlepath x r α β) y = -1"
proof -
have "0 ≤ dist x y"
by simp
also from assms have "dist x y < r"
by auto
finally have r: "r > 0"
by simp
have "winding_number (part_circlepath x r (α - 2 * pi) α) y = 1"
by (rule winding_number_part_circlepath_full) (use assms in auto)
also have "part_circlepath x r (α - 2 * pi) α = reversepath (part_circlepath x r α (α - 2 * pi))"
by simp
also have "winding_number … y = -winding_number (part_circlepath x r α (α - 2 * pi)) y"
using path_image_part_circlepath_subset'[of r x α "α - 2 * pi"] r assms
by (intro winding_number_reversepath) auto
also have "α - 2 * pi = β"
using assms(2) by (simp add: algebra_simps)
finally show ?thesis
by Groebner_Basis.algebra
qed
lemma winding_number_inverse_valid_path:
assumes "valid_path γ" "0 ∉ path_image γ" "z ∉ path_image γ" "z ≠ 0"
shows "winding_number (inverse ∘ γ) (inverse z) = winding_number γ z - winding_number γ 0"
proof -
define C where "C = 1 / (complex_of_real (2 * pi) * 𝗂)"
have "winding_number (inverse ∘ γ) (inverse z)
= C * contour_integral γ (λw. deriv inverse w / (inverse w - inverse z))"
unfolding C_def
proof (rule winding_number_comp[of "UNIV - {0,z}"])
show "open (UNIV - {0, z})"
by (metis Diff_insert open_UNIV open_delete)
show "inverse holomorphic_on UNIV - {0, z}"
by (auto intro:holomorphic_intros)
show "path_image γ ⊆ UNIV - {0, z}" "inverse z ∉ path_image (inverse ∘ γ)"
using ‹0 ∉ path_image γ› ‹z ∉ path_image γ› unfolding path_image_def
by auto
qed fact
also have "… = C * (contour_integral γ (λw. 1 / (w - z) - 1 / w))"
proof -
have "contour_integral γ (λw. deriv inverse w / (inverse w - inverse z)) =
contour_integral γ (λw. 1 / (w - z) - 1 / w)"
proof (rule contour_integral_cong)
fix x assume "x ∈ path_image γ"
then have "x≠0" "x≠z"
using ‹0 ∉ path_image γ› ‹z ∉ path_image γ› unfolding path_image_def
by auto
then show "deriv inverse x / (inverse x - inverse z) = 1 / (x - z) - 1 / x"
using ‹z≠0›
by (auto simp:divide_simps power2_eq_square algebra_simps)
qed simp
then show ?thesis by simp
qed
also have "… = C * (contour_integral γ (λw. 1 / (w - z)) - contour_integral γ (λw. 1 / w))"
proof (subst contour_integral_diff)
show "(λw. 1 / (w - z)) contour_integrable_on γ"
by (rule contour_integrable_inversediff) fact+
show "(/) 1 contour_integrable_on γ"
using contour_integrable_inversediff[OF ‹valid_path γ› ‹0 ∉ path_image γ›]
by simp
qed simp
also have "… = winding_number γ z - winding_number γ 0"
unfolding C_def by (subst (1 2) winding_number_valid_path) (use assms in ‹auto simp: algebra_simps›)
finally show ?thesis .
qed
lemma winding_number_inverse:
assumes "path γ" "path_image γ ⊆ {z. Im z > 0}" "z ∉ path_image γ" "Im z > 0"
shows "winding_number (inverse ∘ γ) (inverse z) = winding_number γ z - winding_number γ 0"
proof -
have compact: "compact (Im ` ({z} ∪ (path_image γ)))"
by (intro compact_continuous_image compact_Un compact_path_image assms continuous_intros) auto
hence bdd: "bdd_below (Im ` ({z} ∪ path_image γ))"
by (meson bounded_imp_bdd_below compact_imp_bounded)
define c' where "c' = Inf (Im ` ({z} ∪ path_image γ))"
have c'_le: "Im u ≥ c'" if "u ∈ {z} ∪ path_image γ" for u
using that bdd unfolding c'_def by (meson cINF_lower)
have "c' ∈ Im ` ({z} ∪ path_image γ)"
unfolding c'_def using compact by (intro closed_contains_Inf compact_imp_closed bdd) auto
with assms have "c' > 0"
by auto
define c where "c = c' / 2"
have "c > 0" "c < c'"
using ‹c' > 0› by (simp_all add: c_def)
have c: "c > 0" "Im z > c" "⋀u. u ∈ path_image γ ⟹ Im u > c"
using ‹c > 0› ‹c < c'› c'_le by force+
show ?thesis
proof (rule winding_number_comp')
show "inverse holomorphic_on {z. Im z > c}"
using c by (intro holomorphic_intros) auto
have "(1/c^2)-lipschitz_on {z. Im z > c} inverse"
by (rule lipschitz_on_subset[OF lipschitz_on_complex_inverse[of c]]) (use c in auto)
thus "uniformly_continuous_on {z. c < Im z} inverse"
by (rule lipschitz_on_uniformly_continuous)
show "inj_on inverse {z. Im z > c}"
using assms by (auto simp: inj_on_def)
show "open {z. Im z > c}"
by (simp add: open_halfspace_Im_gt)
show "path γ" "path_image γ ⊆ {z. Im z > c}" "z ∈ {z. c < Im z}" "z ∉ path_image γ"
using c assms by auto
have "∀⇩F p in valid_path_nhds γ. valid_path p ∧ path_image p ∩ ({z. Im z ≤ c} ∪ {z}) = {}"
by (intro eventually_conj eventually_valid_path_valid_path_nhds
eventually_valid_path_nhds_avoid closed_Un closed_halfspace_Im_le)
(use assms c in force)+
moreover have "∀⇩F p in path_nhds γ. winding_number p 0 = winding_number γ 0 ∧
winding_number p z = winding_number γ z"
by (intro eventually_conj eventually_winding_number_eq_path_nhds) (use assms in auto)
hence "∀⇩F p in valid_path_nhds γ. winding_number p 0 = winding_number γ 0 ∧
winding_number p z = winding_number γ z"
by (meson filter_leD path_nhds_le_valid_path_nhds)
ultimately have "∀⇩F p in valid_path_nhds γ.
contour_integral p (λw. deriv inverse w / (inverse w - inverse z)) =
complex_of_real (2 * pi) * 𝗂 * (winding_number γ z - winding_number γ 0)"
proof eventually_elim
case (elim p)
have "contour_integral p (λw. deriv inverse w / (inverse w - inverse z)) =
contour_integral p (λw. 1 / (w - z) - 1 / w)"
proof (rule contour_integral_cong)
fix x assume "x ∈ path_image p"
then have "x ≠ 0" "x ≠ z"
using elim c by auto
then show "deriv inverse x / (inverse x - inverse z) = 1 / (x - z) - 1 / x"
using assms by (auto simp: divide_simps power2_eq_square)
qed simp
also have "… = contour_integral p (λw. 1 / (w - z)) - contour_integral p ((/) 1)"
proof (rule contour_integral_diff)
show "(λw. 1 / (w - z)) contour_integrable_on p"
by (rule contour_integrable_inversediff) (use elim in auto)
have "(λw. 1 / (w - 0)) contour_integrable_on p"
by (rule contour_integrable_inversediff) (use elim c in auto)
thus "(λw. 1 / w) contour_integrable_on p"
by simp
qed
also have "… = (2 * pi * 𝗂) * (winding_number p z - winding_number p 0)"
by (subst (1 2) winding_number_valid_path) (use elim c in ‹auto simp: algebra_simps›)
finally show ?case
using elim by (simp add: algebra_simps)
qed
thus "∃⇩F p in valid_path_nhds γ.
contour_integral p (λw. deriv inverse w / (inverse w - inverse z)) =
complex_of_real (2 * pi) * 𝗂 * (winding_number γ z - winding_number γ 0)"
by (rule eventually_frequently [rotated]) (use assms in auto)
qed
qed
lemma winding_number_inverse_valid_path_0:
assumes "valid_path γ" "pathstart γ = pathfinish γ" "0 ∉ path_image γ"
shows "winding_number (inverse ∘ γ) 0 = -winding_number γ 0"
proof -
have val: "valid_path (inverse ∘ γ)" using assms
by (intro valid_path_compose_holomorphic[of _ _ "-{0}"] assms)
(auto intro!: holomorphic_intros)
obtain B where B: "⋀w. norm w ≥ B ⟹ winding_number γ w = 0"
using winding_number_zero_at_infinity[of γ] val assms
by (auto simp: valid_path_imp_path)
have "compact (path_image γ ∪ path_image (inverse ∘ γ))"
using assms by (intro compact_Un compact_path_image valid_path_imp_path val) auto
hence "open (-(path_image γ ∪ path_image (inverse ∘ γ)))"
by (intro open_Compl compact_imp_closed)
moreover have "0 ∈ -(path_image γ ∪ path_image (inverse ∘ γ))"
using assms by (auto simp: path_image_compose)
ultimately obtain ε where ε: "ε > 0" "cball 0 ε ⊆ -(path_image γ ∪ path_image (inverse ∘ γ))"
unfolding open_contains_cball by blast
define w where "w = complex_of_real (min ε (1 / max 1 B))"
have pos: "min ε (1 / max 1 B) > 0"
using ε by (auto simp: min_less_iff_disj)
hence norm_w: "norm w = min ε (1 / max 1 B)"
unfolding w_def norm_of_real by simp
from pos have "norm w ≠ 0"
unfolding norm_w by linarith
hence "w ≠ 0"
by auto
have "w ∈ cball 0 ε"
by (auto simp: norm_w)
have "B ≤ max 1 B"
by simp
also have "max 1 B = 1 / (1 / max 1 B)"
by (auto simp: field_simps)
also have "… ≤ 1 / min ε (1 / max 1 B)"
using ε by (intro divide_left_mono) auto
also have "… = norm (inverse w)"
by (simp add: ‹norm w = _› norm_inverse field_simps norm_divide)
finally have "B ≤ norm (inverse w)" .
have "w ∉ inverse ` path_image γ"
using ‹w ∈ cball 0 ε› ε unfolding path_image_compose by blast
hence "inverse w ∉ path_image γ"
using ‹w ≠ 0› by (metis image_iff inverse_inverse_eq)
have "winding_number (inverse ∘ γ) 0 = winding_number (inverse ∘ γ) w"
proof (rule winding_number_eq)
show "w ∈ cball 0 ε" "0 ∈ cball 0 ε" "cball 0 ε ∩ path_image (inverse ∘ γ) = {}"
"connected (cball 0 ε :: complex set)"
using ε by (auto simp: w_def)
qed (use assms val in ‹auto intro: valid_path_imp_path simp: pathfinish_def pathstart_def›)
also have "winding_number (inverse ∘ γ) w = winding_number (inverse ∘ γ) (inverse (inverse w))"
using ‹w ≠ 0› by simp
also have "… = winding_number γ (inverse w) - winding_number γ 0"
using assms ‹w ∈ cball 0 ε› ‹w ≠ 0› ε ‹inverse w ∉ path_image γ›
by (subst winding_number_inverse_valid_path) (auto simp: path_image_compose)
also have "winding_number γ (inverse w) = 0"
using ε ‹B ≤ norm (inverse w)› by (intro B)
finally show ?thesis by (simp add: o_def)
qed
text ‹
The following allows us to compute the winding number of a non-closed circular arc with
respect to its centre.
›
lemma winding_number_part_circlepath_centre:
assumes "r > 0"
shows "winding_number (part_circlepath z r a b) z = (b - a) / (2 * pi)"
proof -
have "winding_number (part_circlepath 0 r a b) 0 = (b - a) / (2 * pi)"
proof (induction a b rule: linorder_wlog)
case (le a b)
show ?case
proof (cases "a = b")
case True
thus ?thesis
using assms by (simp add: part_circlepath_empty winding_number_zero_const)
next
case False
let ?p = "part_circlepath 0 r a b"
have "((λt. 𝗂) has_integral (b - a) *⇩R 𝗂) {a..b}"
using has_integral_const[of 𝗂 a b] assms False le by (simp add: scaleR_conv_of_real mult_ac)
hence "((λz. 1 / z) has_contour_integral (b - a) *⇩R 𝗂) ?p"
by (subst has_contour_integral_part_circlepath_iff) (use assms False le in simp_all)
moreover have "0 ∉ path_image ?p"
using assms by (auto simp: path_image_part_circlepath')
hence "((λz. 1 / z) has_contour_integral 2 * 𝗂 * pi * winding_number ?p 0) ?p"
using has_contour_integral_winding_number[of ?p 0] assms by (auto simp add: mult_ac)
ultimately have "(b - a) *⇩R 𝗂 = 2 * 𝗂 * pi * winding_number ?p 0"
using has_contour_integral_unique by blast
thus ?thesis
by (simp add: scaleR_conv_of_real)
qed
next
case (sym a b)
from assms have "0 ∉ path_image (part_circlepath 0 r a b)"
by (auto simp: path_image_part_circlepath')
thus ?case using assms sym
by (simp add: reversepath_part_circlepath [symmetric, of 0 r b a]
winding_number_reversepath field_simps del: reversepath_part_circlepath)
qed
hence "winding_number ((+) z ∘ part_circlepath 0 r a b) (0 + z) = (b - a) / (2 * pi)"
by (subst winding_number_comp_plus) (use assms in ‹auto simp: path_image_part_circlepath'›)
thus ?thesis
by (subst (asm) part_circlepath_translate) auto
qed
subsection ‹Continuous transformations that preserve the winding number in some way›
locale winding_preserving =
fixes A :: "complex set" and f :: "complex ⇒ complex" and g :: "complex ⇒ complex"
assumes inj: "inj_on f A"
assumes cont: "continuous_on A f"
assumes winding_number_eq:
"⋀p x. path p ⟹ path_image p ⊆ A ⟹ pathstart p = pathfinish p ⟹ x ∈ A - path_image p ⟹
winding_number (f ∘ p) (f x) = g (winding_number p x)"
lemma winding_preserving_comp:
assumes "winding_preserving B f2 g2"
assumes "winding_preserving A f1 g1"
assumes subset: "f1 ` A ⊆ B"
shows "winding_preserving A (f2 ∘ f1) (g2 ∘ g1)"
proof
interpret f1: winding_preserving A f1 g1
by fact
interpret f2: winding_preserving B f2 g2
by fact
show "inj_on (f2 ∘ f1) A"
by (intro comp_inj_on f1.inj inj_on_subset[OF f2.inj] assms)
show "continuous_on A (f2 ∘ f1)"
by (intro continuous_on_compose f1.cont continuous_on_subset[OF f2.cont] subset)
show "winding_number (f2 ∘ f1 ∘ p) ((f2 ∘ f1) x) = (g2 ∘ g1) (winding_number p x)"
if p: "path p" "path_image p ⊆ A" "x ∈ A - path_image p" "pathstart p = pathfinish p" for p x
proof -
have [simp]: "f1 x = f1 (p t) ⟷ x = p t" if "t ∈ {0..1}" for t
using f1.inj that p unfolding inj_on_def path_image_def by blast
have "winding_number (f2 ∘ f1 ∘ p) ((f2 ∘ f1) x) =
winding_number (f2 ∘ (f1 ∘ p)) (f2 (f1 x))"
by (simp add: o_def)
also have "… = g2 (winding_number (f1 ∘ p) (f1 x))"
proof (rule f2.winding_number_eq)
show "path (f1 ∘ p)"
using that by (intro path_continuous_image continuous_on_subset[OF f1.cont])
show "path_image (f1 ∘ p) ⊆ B"
using that subset by (auto simp: path_image_def)
show "f1 x ∈ B - path_image (f1 ∘ p)"
using that subset f1.inj by (auto simp: path_image_def)
qed (use p in ‹auto simp: pathstart_compose pathfinish_compose›)
also have "winding_number (f1 ∘ p) (f1 x) = g1 (winding_number p x)"
by (rule f1.winding_number_eq) (use p in auto)
finally show ?thesis
by (simp add: o_def)
qed
qed
lemmas winding_preserving_comp' = winding_preserving_comp [unfolded o_def]
lemma winding_preserving_subset:
assumes "winding_preserving A f g" "B ⊆ A"
shows "winding_preserving B f g"
proof -
interpret winding_preserving A f g
by fact
show ?thesis
proof
show "inj_on f B"
by (rule inj_on_subset[OF inj]) (use assms(2) in auto)
show "continuous_on B f"
by (rule continuous_on_subset[OF cont]) (use assms(2) in auto)
show "winding_number (f ∘ p) (f x) = g (winding_number p x)"
if "path p" "path_image p ⊆ B" "x ∈ B - path_image p" "pathstart p = pathfinish p" for p x
using that winding_number_eq[of p x] assms(2) by auto
qed
qed
lemma winding_preserving_translate: "winding_preserving A (λx. c + x) (λx. x)"
proof
show "winding_number ((+) c ∘ p) (c + x) = winding_number p x"
if "path p" "path_image p ⊆ A" "x ∈ A - path_image p" for p x
using that winding_number_comp_plus[of p x c] by (auto simp: algebra_simps)
qed (auto intro!: inj_onI continuous_intros)
lemma winding_preserving_mult: "c ≠ 0 ⟹ winding_preserving A (λx. c * x) (λx. x)"
proof
assume "c ≠ 0"
show "winding_number ((*) c ∘ p) (c * x) = winding_number p x"
if "path p" "path_image p ⊆ A" "x ∈ A - path_image p" for p x
using that winding_number_comp_times[of p x c] ‹c ≠ 0› by (auto simp: algebra_simps)
qed (auto intro!: inj_onI continuous_intros)
lemma winding_preserving_cnj: "winding_preserving A cnj (λx. -cnj x)"
proof
show "winding_number (cnj ∘ p) (cnj x) = -cnj (winding_number p x)"
if "path p" "path_image p ⊆ A" "x ∈ A - path_image p" for p x
using that winding_number_cnj[of p x] by (auto simp: algebra_simps)
qed (auto intro!: inj_onI continuous_intros)
lemma winding_preserving_uminus: "winding_preserving A (λx. -x) (λx. x)"
using winding_preserving_mult[of "-1" A] by simp
subsection ‹Paths›
lemma simple_path_cnj [simp]: "simple_path (cnj ∘ p) ⟷ simple_path p"
by (rule simple_path_linear_image_eq) (auto intro!: linear_cnj simp: inj_def)
lemma part_circlepath_cnj': "cnj ∘ part_circlepath c r a b = part_circlepath (cnj c) r (-a) (-b)"
unfolding o_def by (intro ext part_circlepath_cnj)
lemma linepath_minus: "linepath (-a) (-b) x = -linepath a b x"
by (simp add: linepath_def algebra_simps)
text ‹
The following lemma is very difficult to bypass some nasty geometric reasoning:
If a path only touches the frontier of a set at its beginning or end,
then it is either fully inside the set or fully outside the set.
›
lemma path_fully_inside_or_fully_outside:
fixes p :: "real ⇒ 'a :: euclidean_space"
assumes "path p" "⋀x. x ∈ {0<..<1} ⟹ p x ∉ frontier A"
shows "path_image p ⊆ closure A ∨ path_image p ∩ interior A = {}"
proof (rule ccontr)
assume *: "¬(path_image p ⊆ closure A ∨ path_image p ∩ interior A = {})"
from * obtain x y where xy: "x ∈ {0..1}" "y ∈ {0..1}" "p x ∉ closure A" "p y ∈ interior A"
unfolding path_image_def by blast
define x' y' where "x' = min x y" and "y' = max x y"
have xy': "x' ∈ {0..1}" "y' ∈ {0..1}" "x' ≤ y'"
using xy by (auto simp: x'_def y'_def)
define q where "q = subpath x' y' p"
have [simp]: "path q"
using xy' by (auto simp: q_def assms)
have "path_image q ∩ frontier A ≠ {}"
proof (rule connected_Int_frontier)
show "connected (path_image q)"
by auto
next
have "q (if x ≤ y then 0 else 1) ∈ path_image q"
by (auto simp: path_image_def)
moreover have "q (if x ≤ y then 0 else 1) ∉ A"
using xy closure_subset by (auto simp: q_def subpath_def x'_def y'_def)
ultimately show "path_image q - A ≠ {}"
by blast
next
have "q (if x ≤ y then 1 else 0) ∈ path_image q"
by (auto simp: path_image_def)
moreover have "q (if x ≤ y then 1 else 0) ∈ A"
using xy interior_subset by (auto simp: q_def subpath_def x'_def y'_def)
ultimately show "path_image q ∩ A ≠ {}"
by blast
qed
then obtain w where w: "w ∈ {x'..y'}" "p w ∈ frontier A"
unfolding q_def path_image_subpath using xy' by (force split: if_splits)
have "w ≠ x"
using xy w by (metis DiffE frontier_def)
moreover have "w ≠ y"
using xy w unfolding frontier_def by auto
ultimately have "w ∈ {x'<..<y'}"
using w(1) by (auto simp: x'_def y'_def)
also have "… ⊆ {0<..<1}"
using xy' by auto
finally have "w ∈ {0<..<1}" .
with assms(2)[of w] have "p w ∉ frontier A"
by blast
with ‹p w ∈ frontier A› show False
by contradiction
qed
lemma simple_path_joinE':
assumes "simple_path (g1 +++ g2)" and "pathfinish g1 = pathstart g2"
shows "path_image g1 ∩ path_image g2 ⊆
(insert (pathstart g2) (if pathstart g1 = pathfinish g2 then {pathstart g1} else {}))"
using assms
by (smt (verit, del_insts) arc_join_eq insert_commute pathfinish_join pathstart_join simple_path_cases simple_path_joinE)
lemma simple_path_joinE'':
assumes "simple_path (g1 +++ g2)" and "pathfinish g1 = pathstart g2"
"x ∈ path_image g1" "x ∈ path_image g2"
shows "x = pathstart g2 ∨ x = pathfinish g2 ∧ pathstart g1 = pathfinish g2"
using simple_path_joinE'[OF assms(1,2)] assms(3,4) by (auto split: if_splits)
lemma arc_continuous_image:
assumes "arc p" "inj_on f (path_image p)" "continuous_on (path_image p) f"
shows "arc (f ∘ p)"
using assms by (auto simp: arc_def inj_on_def path_image_def intro!: path_continuous_image)
lemma eventually_path_image_cball_subset:
fixes p :: "real ⇒ 'a :: real_normed_vector"
assumes "path p" "path_image p ⊆ interior A"
shows "eventually (λε. (⋃x∈path_image p. cball x ε) ⊆ A) (at_right 0)"
proof -
from assms have "compact ( path_image p)"
by (intro compact_path_image) auto
moreover have "path_image p ∩ frontier A = {}"
using assms by (simp add: disjoint_iff frontier_def subset_eq)
ultimately have "eventually (λε. setdist_gt ε (path_image p) (frontier A)) (at_right 0)"
by (intro compact_closed_imp_eventually_setdist_gt_at_right_0) auto
moreover have "eventually (λε. ε > 0) (at_right (0 :: real))"
by (simp add: eventually_at_right_less)
ultimately have "eventually (λε. (⋃x∈path_image p. cball x ε) ⊆ A) (at_right 0)"
proof eventually_elim
case (elim ε)
show "(⋃x∈path_image p. cball x ε) ⊆ A"
proof (intro subsetI, elim UN_E)
fix x y assume xy: "x ∈ path_image p" "y ∈ cball x ε"
show "y ∈ A"
proof (rule ccontr)
assume "y ∉ A"
have "cball x ε ∩ frontier A ≠ {}"
proof (rule connected_Int_frontier)
have "x ∈ cball x ε"
using ‹ε > 0› by simp
moreover have "x ∈ A"
using ‹x ∈ path_image p› assms interior_subset by blast
ultimately show "cball x ε ∩ A ≠ {}"
by blast
next
from xy show "cball x ε - A ≠ {}"
using ‹y ∉ A› by blast
qed auto
hence "¬setdist_gt ε {x} (frontier A)"
by (force simp: setdist_gt_def)
moreover have "setdist_gt ε {x} (frontier A)"
by (rule setdist_gt_mono[OF elim(1)]) (use xy in auto)
ultimately show False by contradiction
qed
qed
qed
thus ?thesis
by eventually_elim (use assms interior_subset in auto)
qed
lemma eventually_path_image_cball_subset':
fixes p :: "real ⇒ 'a :: real_normed_vector"
assumes "path p" "path_image p ⊆ interior A" "X ⊆ path_image p"
shows "eventually (λε. path_image p ∪ (⋃x∈X. cball x ε) ⊆ A) (at_right 0)"
using eventually_path_image_cball_subset[OF assms(1-2)]
eventually_at_right_less[of 0]
proof eventually_elim
case (elim ε)
have "path_image p ∪ (⋃x∈X. cball x ε) = (⋃x∈path_image p. {x}) ∪ (⋃x∈X. cball x ε)"
by blast
also have "… ⊆ (⋃x∈path_image p. cball x ε) ∪ (⋃x∈X. cball x ε)"
using elim(2) by (intro Un_mono UN_mono) auto
also have "… = (⋃x∈path_image p ∪ X. cball x ε)"
by blast
also have "path_image p ∪ X = path_image p"
using assms by blast
also have "(⋃x∈path_image p. cball x ε) ⊆ A"
by fact
finally show ?case .
qed
text ‹
We say that a path does not cross a set ‹A› if it enters ‹A› at most at its beginning and
end, and never inbetween.
›
definition does_not_cross :: "(real ⇒ 'a :: real_vector) ⇒ 'a set ⇒ bool" where
"does_not_cross p A ⟷ (∀x∈{0<..<1}. p x ∉ A)"
lemma does_not_cross_simple_path:
assumes "simple_path p"
shows "does_not_cross p A ⟷ path_image p ∩ A ⊆ {pathstart p, pathfinish p}"
proof
assume "does_not_cross p A"
thus "path_image p ∩ A ⊆ {pathstart p, pathfinish p}" using assms
by (force simp: does_not_cross_def simple_path_def path_image_def pathstart_def pathfinish_def)
next
assume *: "path_image p ∩ A ⊆ {pathstart p, pathfinish p}"
show "does_not_cross p A"
unfolding does_not_cross_def
proof safe
fix x :: real assume x: "x ∈ {0<..<1}" "p x ∈ A"
hence "p x ∉ {pathstart p, pathfinish p}"
using assms by (force simp: simple_path_def loop_free_def pathstart_def pathfinish_def)+
moreover from x have "p x ∈ path_image p"
by (auto simp: path_image_def)
ultimately show False
using * and x by blast
qed
qed
lemma path_fully_inside_or_fully_outside':
fixes p :: "real ⇒ 'a :: euclidean_space"
assumes "path p" "does_not_cross p (frontier A)"
shows "path_image p ⊆ closure A ∨ path_image p ∩ interior A = {}"
using path_fully_inside_or_fully_outside[OF assms(1), of A] assms unfolding does_not_cross_def
by auto
lemma in_path_image_part_circlepathI:
assumes "y = x + rcis r u" "u ∈ closed_segment a b"
shows "y ∈ path_image (part_circlepath x r a b)"
proof -
have "u ∈ path_image (linepath a b)"
using assms by simp
then obtain v where v: "v ∈ {0..1}" "u = linepath a b v"
unfolding path_image_def by blast
have "y = part_circlepath x r a b v"
by (simp add: part_circlepath_altdef v assms)
with v(1) show ?thesis
unfolding path_image_def by blast
qed
lemma in_path_image_part_circlepathI':
assumes "Arg (y - x) ∈ closed_segment a b" "dist y x = r"
shows "y ∈ path_image (part_circlepath x r a b)"
proof (rule in_path_image_part_circlepathI)
show "y = x + rcis r (Arg (y - x))"
using assms
by (cases "x = y")
(auto simp: rcis_def cis_Arg complex_sgn_def dist_commute scaleR_conv_of_real
field_simps dist_norm norm_minus_commute)
qed fact
lemma path_image_part_circlepath':
"path_image (part_circlepath x r a b) = (λt. x + rcis r t) ` closed_segment a b"
proof -
have "path_image (part_circlepath x r a b) = (λt. x + rcis r t) ` path_image (linepath a b)"
by (simp add: path_image_def part_circlepath_altdef image_image)
thus ?thesis
by simp
qed
lemma path_image_part_circlepath:
assumes "a ∈ {-pi<..pi}" "b ∈ {-pi<..pi}" "r > 0"
shows "path_image (part_circlepath x r a b) = {y∈sphere x r. Arg (y - x) ∈ closed_segment a b}"
proof safe
fix y assume y: "y ∈ path_image (part_circlepath x r a b)"
show "y ∈ sphere x r"
using y path_image_part_circlepath_subset'[of r x a b] assms by auto
from y obtain u where u: "u ∈ {0..1}" "y = part_circlepath x r a b u"
by (auto simp: path_image_def)
have "linepath a b u ∈ closed_segment a b"
using linepath_in_path u(1) by blast
also have "… ⊆ {-pi<..pi}"
using assms by (intro closed_segment_subset) auto
finally have *: "linepath a b u ∈ {-pi<..pi}" .
have "Arg (y - x) = Arg (rcis r (linepath a b u))"
by (simp add: u part_circlepath_altdef)
also have "… = linepath a b u"
using * assms by (subst Arg_rcis) auto
also have "… ∈ closed_segment a b"
by fact
finally show "Arg (y - x) ∈ closed_segment a b" .
next
fix y assume y: "y ∈ sphere x r" "Arg (y - x) ∈ closed_segment a b"
show "y ∈ path_image (part_circlepath x r a b)"
using y by (intro in_path_image_part_circlepathI') (auto simp: dist_commute)
qed
lemma path_image_part_circlepath_mono:
assumes "min a' b' ≤ min a b" "max a' b' ≥ max a b"
shows "path_image (part_circlepath x r a b) ⊆ path_image (part_circlepath x r a' b')"
proof -
have "path_image (part_circlepath x r a b) = (λt. x + rcis r t) ` path_image (linepath a b)"
by (simp add: path_image_def part_circlepath_altdef image_image)
also have "… ⊆ (λt. x + rcis r t) ` path_image (linepath a' b')"
unfolding path_image_linepath using assms
by (intro image_mono) (auto simp: closed_segment_eq_real_ivl split: if_splits)
also have "… = path_image (part_circlepath x r a' b')"
by (simp add: path_image_def part_circlepath_altdef image_image)
finally show ?thesis .
qed
subsection ‹Topology›
lemma eventually_at_within_in_open:
assumes "open X" "x ∈ X"
shows "eventually (λz. z ∈ X ∩ A - {x}) (at x within A)"
using eventually_nhds_in_open[OF assms] unfolding eventually_at_filter
by eventually_elim auto
lemma filterlim_at_withinD:
assumes "filterlim f (at L within A) F" "open X" "L ∈ X"
shows "eventually (λx. f x ∈ X ∩ A - {L}) F"
proof -
have "eventually (λz. z ∈ X ∩ A - {L}) (at L within A)"
by (rule eventually_at_within_in_open) (use assms in auto)
moreover from assms(1) have "filtermap f F ≤ at L within A"
unfolding filterlim_def .
ultimately have "eventually (λz. z ∈ X ∩ A - {L}) (filtermap f F)"
unfolding le_filter_def by blast
thus ?thesis
by (simp add: eventually_filtermap)
qed
lemma filterlim_at_withinD':
assumes "filterlim f (at L within A) F" "open X" "L ∈ X"
shows "eventually (λx. f x ∈ X ∩ A) F"
using filterlim_at_withinD[OF assms] by eventually_elim auto
lemma filterlim_at_rightD:
assumes "filterlim f (at_right L) F" "a > L"
shows "eventually (λx. f x ∈ {L<..<a}) F"
using filterlim_at_withinD'[OF assms(1), of "{..<a}"] assms(2)
by (auto elim!: eventually_mono)
lemma filterlim_at_leftD:
assumes "filterlim f (at_left L) F" "a < L"
shows "eventually (λx. f x ∈ {a<..<L}) F"
using filterlim_at_withinD'[OF assms(1), of "{a<..}"] assms(2)
by (auto elim!: eventually_mono)
lemma eventually_Ball_at_right_0_real:
assumes "eventually P (at_right (0 :: real))"
shows "eventually (λx. ∀y∈{0<..x}. P y) (at_right 0)"
using assms unfolding eventually_at_right_field by force
lemma open_segment_same_Re:
assumes "Re a = Re b"
shows "open_segment a b = {z. Re z = Re a ∧ Im z ∈ open_segment (Im a) (Im b)}"
using assms by (auto simp: open_segment_def closed_segment_same_Re complex_eq_iff)
lemma open_segment_same_Im:
assumes "Im a = Im b"
shows "open_segment a b = {z. Im z = Im a ∧ Re z ∈ open_segment (Re a) (Re b)}"
using assms by (auto simp: open_segment_def closed_segment_same_Im complex_eq_iff)
lemma interior_halfspace_Re_ge [simp]: "interior {z. Re z ≥ x} = {z. Re z > x}"
and interior_halfspace_Re_le [simp]: "interior {z. Re z ≤ x} = {z. Re z < x}"
and interior_halfspace_Im_ge [simp]: "interior {z. Im z ≥ x} = {z. Im z > x}"
and interior_halfspace_Im_le [simp]: "interior {z. Im z ≤ x} = {z. Im z < x}"
using interior_halfspace_ge[of "1::complex" x] interior_halfspace_le[of "1::complex" x]
interior_halfspace_ge[of 𝗂 x] interior_halfspace_le[of 𝗂 x]
by (simp_all add: inner_complex_def)
thm arc_def
thm simple_path_def
end