Winding numbers of absolutely continuous curves in star-shaped sets #
A closed absolutely continuous curve contained in a set Ω that is star-shaped about x has
winding number 0 about every point outside Ω, by straight-line contraction to the constant
curve at x. Consequently, two absolutely continuous paths in Ω sharing both endpoints have
the same winding number about every point outside Ω.
References #
- S. Lang, Complex Analysis, Ch. IV.
theorem
AbsolutelyContinuousOnInterval.windingNumber_eq_zero_of_starConvex
{γ : ℝ → ℂ}
{a b : ℝ}
{w : ℂ}
{Ω : Set ℂ}
{x : ℂ}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hstar : StarConvex ℝ x Ω)
(hclosed : γ a = γ b)
(hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω)
(hw : w ∉ Ω)
:
The winding number of a closed absolutely continuous curve vanishes outside any star-shaped set containing its trace.
theorem
AbsolutelyContinuousOnInterval.isNullHomologous_of_starConvex
{γ : ℝ → ℂ}
{a b : ℝ}
{Ω : Set ℂ}
{x : ℂ}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hstar : StarConvex ℝ x Ω)
(hclosed : γ a = γ b)
(hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω)
:
TauCeti.Contour.IsNullHomologous γ a b Ω
A closed absolutely continuous curve in a star-shaped set is null-homologous there.
theorem
AbsolutelyContinuousOnInterval.windingNumber_eq_of_starConvex_of_eq_endpoints
{γ₀ γ₁ : ℝ → ℂ}
{a b : ℝ}
{w : ℂ}
{Ω : Set ℂ}
{x : ℂ}
(h₀ : AbsolutelyContinuousOnInterval γ₀ a b)
(h₁ : AbsolutelyContinuousOnInterval γ₁ a b)
(hstar : StarConvex ℝ x Ω)
(ha : γ₀ a = γ₁ a)
(hb : γ₀ b = γ₁ b)
(h₀Ω : ∀ t ∈ Set.uIcc a b, γ₀ t ∈ Ω)
(h₁Ω : ∀ t ∈ Set.uIcc a b, γ₁ t ∈ Ω)
(hw : w ∉ Ω)
:
Two absolutely continuous paths in a star-shaped set with common endpoints have equal winding numbers outside that set.