Theory Path_Nhds
section ‹Neighbourhoods of a path›
theory Path_Nhds
imports "HOL-Complex_Analysis.Complex_Analysis"
begin
lemma le_filterD_frequently [trans]: "F ≤ G ⟹ frequently P F ⟹ frequently P G"
unfolding le_filter_def frequently_def by blast
lemma le_filterD_frequently' [trans]: "frequently P F ⟹ F ≤ G ⟹ frequently P G"
unfolding le_filter_def frequently_def by blast
lemma frequently_filtermap: "frequently P (filtermap f F) ⟷ frequently (λx. P (f x)) F"
by (simp add: frequently_def eventually_filtermap)
lemma eventually_uniformly_on_iff:
"eventually P (uniformly_on A f) ⟷ (∃e>0. ∀g. (∀y∈A. dist (g y) (f y) < e) ⟶ P g)"
(is "?lhs = ?rhs")
proof -
have "eventually P (uniformly_on A f) ⟷
(∃X⊆{0<..}. finite X ∧ eventually P (INF b∈X. principal {fa. ∀x∈A. dist (fa x) (f x) < b}))"
unfolding uniformly_on_def by (rule eventually_INF)
also have "… ⟷ (∃X⊆{(0::real)<..}. finite X ∧ (∃Q. (∀e∈X. ∀g. (∀y∈A. dist (g y) (f y) < e) ⟶ Q e g) ∧
(∀y. (∀x∈X. Q x y) ⟶ P y)))"
proof (intro ex_cong1 conj_cong refl, goal_cases)
case (1 X)
have "eventually P (INF b∈X. principal {fa. ∀x∈A. dist (fa x) (f x) < b}) ⟷
(∃Q. (∀e∈X. ∀g. (∀y∈A. dist (g y) (f y) < e) ⟶ Q e g) ∧
(∀y. (∀x∈X. Q x y) ⟶ P y))"
using 1 by (subst eventually_INF_finite) (simp_all add: eventually_principal)
thus ?case .
qed
finally have eq: "eventually P (uniformly_on A f) =
(∃X⊆{0<..}. finite X ∧
(∃Q. (∀e∈X. ∀g. (∀y∈A. dist (g y) (f y) < e) ⟶ Q e g) ∧
(∀y. (∀x∈X. Q x y) ⟶ P y)))" .
show ?thesis
proof
assume ?rhs
then obtain e where e: "e > 0" "⋀g. (∀y∈A. dist (g y) (f y) < e) ⟹ P g"
by blast
let ?Q = "λe g. ∀y∈A. dist (g y) (f y) < e"
show "eventually P (uniformly_on A f)"
by (subst eq, rule exI[of _ "{e}"], safe intro!: e exI[of _ ?Q]) (use e in auto)
next
assume ?lhs
then obtain X Q where XQ: "X ⊆ {0<..}" "finite X"
"⋀e g. e ∈ X ⟹ (∀y∈A. dist (g y) (f y) < e) ⟹ Q e g"
"⋀g. (⋀x. x ∈ X ⟹ Q x g) ⟹ P g"
by (subst (asm) eq) metis
show ?rhs
proof (cases "X = {}")
case True
thus ?thesis using XQ
by (auto intro!: exI[of _ 1])
next
case False
define e where "e = Min X"
have e: "e > 0" "e ∈ X"
using False XQ(1,2) by (auto simp: e_def)
show ?rhs
proof (rule exI[of _ e], safe)
show "e > 0"
by fact
next
fix g assume g: "∀y∈A. dist (g y) (f y) < e"
show "P g"
proof (intro XQ ballI)
fix e' y assume e': "e' ∈ X" and y: "y ∈ A"
have "dist (g y) (f y) < e"
using g y by blast
also have "e ≤ e'"
using e' False ‹finite X› by (simp add: e_def)
finally show "dist (g y) (f y) < e'" .
qed auto
qed
qed
qed
qed
lemma eventually_uniformly_onI [intro?]:
"e > 0 ⟹ (⋀g. (⋀y. y ∈ A ⟹ dist (g y) (f y) < e) ⟹ P g) ⟹
eventually P (uniformly_on A f)"
unfolding eventually_uniformly_on_iff by blast
abbreviation same_ends :: "(real ⇒ 'a :: topological_space) ⇒ (real ⇒ 'a) ⇒ bool"
where "same_ends p q ≡ pathstart p = pathstart q ∧ pathfinish p = pathfinish q"
subsection ‹Nearby paths›
definition path_nhds :: "(real ⇒ 'a :: real_normed_vector) ⇒ (real ⇒ 'a) filter" where
"path_nhds γ = inf (uniformly_on {0..1} γ) (principal {p. path p ∧ same_ends p γ})"
lemma eventually_path_nhds_iff:
"eventually P (path_nhds γ) ⟷
(∃e>0. ∀p. path p ⟶ same_ends p γ ⟶ (∀y∈{0..1}. dist (p y) (γ y) < e) ⟶ P p)"
unfolding path_nhds_def eventually_uniformly_on_iff eventually_inf_principal
by blast
lemma frequently_path_nhds_iff:
"frequently P (path_nhds γ) ⟷
(∀e>0. ∃p. path p ∧ same_ends p γ ∧ (∀y∈{0..1}. dist (p y) (γ y) < e) ∧ P p)"
unfolding frequently_def eventually_path_nhds_iff by blast
lemma eventually_path_nhdsI [intro?]:
"e > 0 ⟹ (⋀p. path p ⟹ same_ends p γ ⟹ (⋀y. y ∈ {0..1} ⟹ dist (p y) (γ y) < e) ⟹ P p)
⟹ eventually P (path_nhds γ)"
unfolding eventually_path_nhds_iff by blast
lemma eventually_path_path_nhds: "eventually (λp. path p) (path_nhds γ)"
by (rule eventually_path_nhdsI[OF zero_less_one])
lemma path_nhds_neq_bot [simp]: "path γ ⟹ path_nhds γ ≠ bot"
by (auto simp: trivial_limit_def eventually_path_nhds_iff intro!: exI[of _ γ])
lemma eventually_dist_less_path_nhds:
assumes "e > 0"
shows "eventually (λp. ∀t∈{0..1}. dist (p t) (γ t) < e) (path_nhds γ)"
using assms by (intro eventually_path_nhdsI[of e]) auto
lemma eventually_winding_number_eq_path_nhds:
assumes "path γ" "z ∉ path_image γ"
shows "eventually (λp. winding_number p z = winding_number γ z) (path_nhds γ)"
proof -
define e where "e = setdist {z} (path_image γ)"
show ?thesis
proof (rule eventually_path_nhdsI; safe?)
show "e > 0"
using assms unfolding e_def
by (subst setdist_gt_0_compact_closed) (auto intro!: closed_path_image)
next
fix p assume p: "path p" "pathstart p = pathstart γ" "pathfinish p = pathfinish γ"
"⋀y. y ∈ {0..1} ⟹ dist (p y) (γ y) < e"
show "winding_number p z = winding_number γ z"
proof (rule winding_number_nearby_paths_eq)
fix t :: real assume t: "t ∈ {0..1}"
have "norm (p t - γ t) < e"
using p(4)[OF t] by (simp add: dist_norm)
also have "… ≤ dist z (γ t)"
unfolding e_def by (rule setdist_le_dist) (use t in ‹auto simp: path_image_def›)
finally show "cmod (p t - γ t) < cmod (γ t - z)"
by (simp add: dist_norm norm_minus_commute)
qed (use p assms in auto)
qed
qed
lemma eventually_path_image_subset_path_nhds:
assumes "path γ" "open A" "path_image γ ⊆ A"
shows "eventually (λp. path_image p ⊆ A) (path_nhds γ)"
proof -
have "compact (path_image γ)"
by (intro compact_path_image assms)
then obtain e where e: "e > 0" "(⋃x∈path_image γ. cball x e) ⊆ A"
using compact_subset_open_imp_cball_epsilon_subset[of "path_image γ" A] assms ‹open A›
by blast
have "eventually (λp. ∀t∈{0..1}. dist (p t) (γ t) < e) (path_nhds γ)"
by (intro eventually_dist_less_path_nhds assms e)
thus ?thesis
proof eventually_elim
case (elim p)
show "path_image p ⊆ A"
unfolding path_image_def
proof safe
fix t :: real assume t: "t ∈ {0..1}"
have "dist (p t) (γ t) < e"
using elim t by blast
hence "p t ∈ (⋃x∈path_image γ. cball x e)"
unfolding path_image_def using t by (auto simp: dist_commute intro!: less_imp_le)
also have "… ⊆ A"
using e by blast
finally show "p t ∈ A" .
qed
qed
qed
lemma eventually_path_nhds_avoid:
assumes "path γ" "closed A" "A ∩ path_image γ = {}"
shows "eventually (λp. path_image p ∩ A = {}) (path_nhds γ)"
proof -
have "eventually (λp. path_image p ⊆ -A) (path_nhds γ)"
by (rule eventually_path_image_subset_path_nhds) (use assms in auto)
thus ?thesis
by eventually_elim blast
qed
text ‹
If we have a path ‹p› and transform it with a function that is continuous
in some open neighbourhood of ‹p›, then all the paths that are close to ‹p›
are also transformed to paths close to the image of ‹p›.
›
lemma continuous_path_image:
fixes p :: "real ⇒ 'a :: euclidean_space"
assumes "path p" "continuous_on A f" "open A" "path_image p ⊆ A"
shows "filterlim (λp. f ∘ p) (path_nhds (f ∘ p)) (path_nhds p)"
unfolding filterlim_def le_filter_def eventually_filtermap
proof safe
fix P assume P: "eventually P (path_nhds (f ∘ p))"
then obtain ε :: real where ε: "ε > 0"
"⋀p'. path p' ⟹ same_ends p' (f ∘ p) ⟹
(⋀t. t ∈ {0..1} ⟹ dist (p' t) ((f ∘ p) t) < ε) ⟹ P p'"
unfolding eventually_path_nhds_iff by blast
obtain r where r: "r > 0" "(⋃x∈path_image p. cball x r) ⊆ A"
using compact_subset_open_imp_cball_epsilon_subset[of "path_image p" A] assms
by auto
define B where "B = (⋃x∈path_image p. cball x r)"
have "B ⊆ A"
using r unfolding B_def by blast
have "compact B"
unfolding B_def by (intro compact_minkowski_sum_cball compact_path_image assms)
have "uniformly_continuous_on B f"
by (intro compact_uniformly_continuous continuous_on_subset[OF assms(2)]) fact+
then obtain δ' where δ': "δ' > 0" "⋀x y. x ∈ B ⟹ y ∈ B ⟹ dist x y < δ' ⟹ dist (f x) (f y) < ε"
using ‹ε > 0› unfolding uniformly_continuous_on_def by fast
define δ where "δ = min r δ'"
have δ: "δ > 0" "δ ≤ r" "δ ≤ δ'"
using ‹δ' > 0› ‹r > 0› unfolding δ_def by auto
show "∀⇩F x in path_nhds p. P (f ∘ x)"
proof
show "δ > 0"
by fact
next
fix p'
assume p': "path p'" "same_ends p' p"
"⋀t. t ∈ {0..1} ⟹ dist (p' t) (p t) < δ"
have "path_image p ⊆ B"
unfolding B_def using ‹r > 0› by fastforce
have "path_image p' ⊆ B"
using p'(3) δ unfolding B_def
by (force simp: path_image_def dist_commute)
show "P (f ∘ p')"
proof (rule ε(2))
show "path (f ∘ p')"
using assms ‹path_image p' ⊆ B› ‹B ⊆ A›
by (intro path_continuous_image p' continuous_on_subset[OF assms(2)]) auto
show "same_ends (f ∘ p') (f ∘ p)"
using p' by (simp add: pathstart_compose pathfinish_compose)
show "dist ((f ∘ p') t) ((f ∘ p) t) < ε" if "t ∈ {0..1}" for t
proof -
have "dist ((f ∘ p') t) ((f ∘ p) t) = dist (f (p' t)) (f (p t))"
by simp
moreover have "dist (p' t) (p t) < δ'"
using δ_def min_less_iff_conj p'(3) that by blast
ultimately show "dist ((f ∘ p') t) ((f ∘ p) t) < ε"
unfolding o_def using p' ‹path_image p ⊆ B› ‹path_image p' ⊆ B› δ that
by (intro δ') (auto simp: path_image_def)
qed
qed
qed
qed
subsection ‹Piecewise smooth paths in the neighbourhood›
definition valid_path_nhds :: "(real ⇒ 'a :: real_normed_vector) ⇒ (real ⇒ 'a) filter" where
"valid_path_nhds γ = inf (uniformly_on {0..1} γ) (principal {p. valid_path p ∧ same_ends p γ})"
lemma eventually_valid_path_nhds_iff:
"eventually P (valid_path_nhds γ) ⟷
(∃e>0. ∀p. valid_path p ⟶ same_ends p γ ⟶ (∀y∈{0..1}. dist (p y) (γ y) < e) ⟶ P p)"
unfolding valid_path_nhds_def eventually_uniformly_on_iff eventually_inf_principal
by blast
lemma frequently_valid_path_nhds_iff:
"frequently P (valid_path_nhds γ) ⟷
(∀e>0. ∃p. valid_path p ∧ same_ends p γ ∧ (∀y∈{0..1}. dist (p y) (γ y) < e) ∧ P p)"
unfolding frequently_def eventually_valid_path_nhds_iff by blast
lemma eventually_valid_path_nhdsI [intro?]:
"e > 0 ⟹ (⋀p. valid_path p ⟹ same_ends p γ ⟹ (⋀y. y ∈ {0..1} ⟹ dist (p y) (γ y) < e) ⟹ P p)
⟹ eventually P (valid_path_nhds γ)"
unfolding eventually_valid_path_nhds_iff by blast
lemma eventually_valid_path_valid_path_nhds: "eventually (λp. valid_path p) (valid_path_nhds γ)"
by (rule eventually_valid_path_nhdsI [OF zero_less_one])
lemma path_nhds_le_valid_path_nhds: "valid_path_nhds γ ≤ path_nhds γ"
by (rule filter_leI)
(auto simp: eventually_path_nhds_iff eventually_valid_path_nhds_iff valid_path_imp_path)
lemma valid_path_nhds_neq_bot [simp]: "valid_path γ ⟹ valid_path_nhds γ ≠ bot"
by (auto simp: trivial_limit_def eventually_valid_path_nhds_iff intro!: exI[of _ γ])
lemma valid_path_nhds_eq_bot' [simp]:
assumes "path (γ :: real ⇒ 'a :: euclidean_space)"
shows "valid_path_nhds γ ≠ bot"
proof -
{
fix e :: real assume e: "e > 0"
obtain p where p: "polynomial_function p" "pathstart p = pathstart γ"
"pathfinish p = pathfinish γ" "⋀t. t ∈ {0..1} ⟹ norm (p t - γ t) < e"
using path_approx_polynomial_function[OF assms(1) e] by blast
hence "∃p. valid_path p ∧ same_ends p γ ∧ (∀t∈{0..1}. dist (p t) (γ t) < e)"
using valid_path_polynomial_function by (intro exI[of _ p]) (auto simp: dist_norm)
}
thus ?thesis
unfolding trivial_limit_def eventually_valid_path_nhds_iff by blast
qed
lemma eventually_dist_less_valid_path_nhds:
assumes "e > 0"
shows "eventually (λp. ∀t∈{0..1}. dist (p t) (γ t) < e) (valid_path_nhds γ)"
using assms by (intro eventually_valid_path_nhdsI[of e]) auto
lemma eventually_same_ends_path_nhds:
"eventually (λp. same_ends p γ) (path_nhds γ)"
and eventually_same_ends_valid_path_nhds:
"eventually (λp. same_ends p γ) (valid_path_nhds γ)"
by (rule eventually_path_nhdsI[of 1] eventually_valid_path_nhdsI[of 1]; simp)+
lemma eventually_valid_path_nhds_avoid:
assumes "path γ" "closed A" "A ∩ path_image γ = {}"
shows "eventually (λp. path_image p ∩ A = {}) (valid_path_nhds γ)"
using eventually_path_nhds_avoid[OF assms]
le_filter_def path_nhds_le_valid_path_nhds by blast
lemma winding_number_unique':
assumes "frequently (λp. winding_number p z = n) (valid_path_nhds γ)"
assumes "path γ" "z ∉ path_image γ"
shows "winding_number γ z = n"
proof (rule winding_number_unique)
fix e :: real
assume e: "e > 0"
have "frequently (λp. path_image p ∩ {z} = {} ∧ winding_number p z = n) (valid_path_nhds γ)"
using assms by (intro frequently_eventually_conj eventually_valid_path_nhds_avoid) auto
then obtain p
where p: "valid_path p" "z ∉ path_image p" "same_ends p γ" "winding_number p z = n"
"(∀y∈{0..1}. dist (p y) (γ y) < e)"
using e unfolding frequently_valid_path_nhds_iff by fast
have "contour_integral p (λw. 1 / (w - z)) = 2 * complex_of_real pi * 𝗂 * winding_number p z"
using p by (subst winding_number_valid_path) auto
with p show "∃p. winding_number_prop γ z e p n"
by (intro exI[of _ p]) (auto simp: winding_number_prop_def dist_norm norm_minus_commute)
qed (use assms in auto)
lemma eventually_path_image_subset_valid_path_nhds:
assumes "path γ" "open A" "path_image γ ⊆ A"
shows "eventually (λp. path_image p ⊆ A) (valid_path_nhds γ)"
using eventually_path_image_subset_path_nhds[OF assms]
le_filter_def path_nhds_le_valid_path_nhds by blast
text ‹
A set is defined to be path-connected if any two points in it are connected by a continuous
path. The following shows that for open sets, one can also take the paths to be piecewise C1.
›
lemma path_connected_open_has_valid_path:
fixes A :: "'a :: euclidean_space set"
assumes "path_connected A" "open A" "x ∈ A" "y ∈ A"
obtains p where "valid_path p" "path_image p ⊆ A" "pathstart p = x" "pathfinish p = y"
proof -
from assms obtain p where p: "path p" "path_image p ⊆ A" "pathstart p = x" "pathfinish p = y"
by (force simp: path_connected_def)
have "eventually (λp'. valid_path p' ∧ path_image p' ⊆ A ∧ same_ends p p') (valid_path_nhds p)"
using eventually_valid_path_valid_path_nhds eventually_same_ends_valid_path_nhds
eventually_path_image_subset_valid_path_nhds[OF p(1) assms(2) p(2)]
by eventually_elim auto
moreover have "valid_path_nhds p ≠ bot"
using p by auto
ultimately show ?thesis using that
using eventually_happens' p(3) p(4) by force
qed
text ‹
A path ‹p› always has arbitrarily close smooth paths in its vicinity.
(i.e. it can be approximated by smooth paths to arbitrary precision)
›
lemma frequently_valid_path:
assumes "path (p :: real ⇒ 'a :: euclidean_space)"
shows "frequently (λp'. valid_path p') (path_nhds p)"
proof -
have "valid_path_nhds p ≠ bot"
using assms by simp
thus ?thesis
by (meson eventually_frequently eventually_valid_path_valid_path_nhds
frequently_def le_filter_def path_nhds_le_valid_path_nhds)
qed
subsection ‹Lipschitz-continuity and paths›
lemma path_nhds_compose:
assumes "uniformly_continuous_on A f" "path γ" "path_image γ ⊆ A" "open A"
shows "filterlim ((∘) f) (path_nhds (f ∘ γ)) (path_nhds γ)"
proof -
have 1: "uniform_limit {0..1} (λg. g) γ (path_nhds γ)"
unfolding path_nhds_def using filterlim_ident filterlim_inf by blast
have 2: "∀⇩F h in path_nhds γ. path_image h ⊆ A"
by (rule eventually_path_image_subset_path_nhds) (use assms in auto)
have 3: "uniform_limit {0..1} ((∘) f) (f ∘ γ) (path_nhds γ)"
using uniform_limit_compose[OF 1 assms(1)] 2 assms by (simp add: o_def[abs_def] path_image_def)
have 4: "∀⇩F x in path_nhds γ. path (f ∘ x) ∧ same_ends (f ∘ x) (f ∘ γ)"
using eventually_path_path_nhds[of γ] eventually_same_ends_path_nhds[of γ] 2
proof eventually_elim
case (elim h)
have "continuous_on (path_image h) f"
using uniformly_continuous_imp_continuous continuous_on_subset elim assms by blast
hence "path (f ∘ h)"
using elim by (auto intro!: path_continuous_image)
moreover have "same_ends (f ∘ h) (f ∘ γ)"
using elim by (auto simp: pathstart_compose pathfinish_compose)
ultimately show ?case
by blast
qed
from 3 and 4 show ?thesis
unfolding path_nhds_def filterlim_inf filterlim_principal by simp_all
qed
lemma valid_path_nhds_compose:
assumes "f analytic_on A" "uniformly_continuous_on A f" "path γ" "path_image γ ⊆ A" "open A"
shows "filterlim ((∘) f) (valid_path_nhds (f ∘ γ)) (valid_path_nhds γ)"
proof -
have 1: "uniform_limit {0..1} (λg. g) γ (valid_path_nhds γ)"
unfolding valid_path_nhds_def using filterlim_ident filterlim_inf by blast
have 2: "∀⇩F h in valid_path_nhds γ. path_image h ⊆ A"
by (rule eventually_path_image_subset_valid_path_nhds) (use assms in auto)
have 3: "uniform_limit {0..1} ((∘) f) (f ∘ γ) (valid_path_nhds γ)"
using uniform_limit_compose[OF 1 assms(2)] 2 assms by (simp add: o_def[abs_def] path_image_def)
have 4: "∀⇩F x in valid_path_nhds γ. valid_path (f ∘ x) ∧ same_ends (f ∘ x) (f ∘ γ)"
using eventually_valid_path_valid_path_nhds[of γ] eventually_same_ends_valid_path_nhds[of γ] 2
proof eventually_elim
case (elim h)
have "continuous_on (path_image h) f"
using uniformly_continuous_imp_continuous continuous_on_subset elim assms by blast
hence "valid_path (f ∘ h)"
using elim by (auto intro!: valid_path_compose_analytic analytic_on_subset[OF assms(1)])
moreover have "same_ends (f ∘ h) (f ∘ γ)"
using elim by (auto simp: pathstart_compose pathfinish_compose)
ultimately show ?case
by blast
qed
from 3 and 4 show ?thesis
unfolding valid_path_nhds_def filterlim_inf filterlim_principal by simp_all
qed
lemma winding_number_comp':
assumes f: "f holomorphic_on A" "uniformly_continuous_on A f" "inj_on f A" "open A"
assumes γ: "path γ" "path_image γ ⊆ A"
assumes z: "z ∈ A" "z ∉ path_image γ"
assumes int: "∃⇩F p in valid_path_nhds γ.
contour_integral p (λw. deriv f w / (f w - f z)) = 2 * pi * 𝗂 * c"
shows "winding_number (f ∘ γ) (f z) = c"
proof -
have cont: "continuous_on A f"
using f(1) by (intro holomorphic_on_imp_continuous_on)
have *: "f z ∉ f ` X" if "z ∉ X" "X ⊆ A" for X
proof
assume "f z ∈ f ` X"
then obtain z' where z': "z' ∈ X" "f z' = f z"
by force
have "z' = z"
using inj_onD[OF f(3) z'(2)] z'(1) z γ(2) interior_subset that by auto
with z'(1) and that show False
by simp
qed
show ?thesis
proof (rule winding_number_unique')
show "path (f ∘ γ)"
using assms
by (intro path_continuous_image γ continuous_on_subset[OF cont])
next
show "f z ∉ path_image (f ∘ γ)"
unfolding path_image_compose using assms interior_subset by (intro *) auto
next
have ev: "∀⇩F p in valid_path_nhds γ. path_image p ∩ {z} = {} ∧ path_image p ⊆ A ∧ valid_path p"
by (intro eventually_conj eventually_valid_path_nhds_avoid
eventually_path_image_subset_valid_path_nhds eventually_valid_path_valid_path_nhds)
(use assms in auto)
have freq: "∃⇩Fp in valid_path_nhds γ. winding_number (f ∘ p) (f z) = c"
using frequently_eventually_conj[OF int ev]
proof (rule frequently_elim1, goal_cases)
case (1 p)
have "f z ∉ path_image (f ∘ p)"
unfolding path_image_compose using * 1 by blast
hence "winding_number (f ∘ p) (f z) =
contour_integral (f ∘ p) (λw. 1 / (w - f z)) / (2 * pi * 𝗂)" using 1
by (subst winding_number_valid_path)
(auto simp: path_image_compose intro!: valid_path_compose_holomorphic
holomorphic_on_subset[OF f(1)] ‹open A›)
also have "… = c"
proof (subst contour_integral_comp_analyticW)
show "f analytic_on A"
using assms by (simp add: analytic_on_open)
show "valid_path p" "path_image p ⊆ A"
using 1 by auto
qed (use 1 ‹open A› in auto)
finally show ?case .
qed
show "∃⇩F p in valid_path_nhds (f ∘ γ). winding_number p (f z) = c"
using valid_path_nhds_compose unfolding filterlim_def
proof (rule le_filterD_frequently)
show "f analytic_on A"
using assms by (simp_all add: analytic_on_open)
qed (use assms freq in ‹auto simp: frequently_filtermap›)
qed
qed
end