Local constancy of winding numbers for absolutely continuous curves #
The winding number of a closed absolutely continuous curve is locally constant off its trace, and is consequently constant on each connected component of the trace complement.
theorem
AbsolutelyContinuousOnInterval.isLocallyConstant_windingNumber
{γ : ℝ → ℂ}
{a b : ℝ}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hclosed : γ a = γ b)
:
IsLocallyConstant fun (z : { z : ℂ // z ∉ γ '' Set.uIcc a b }) => TauCeti.Contour.windingNumber γ a b ↑z
The winding number of a closed absolutely continuous curve is locally constant off its trace.
theorem
AbsolutelyContinuousOnInterval.windingNumber_eq_of_mem_connectedComponentIn
{γ : ℝ → ℂ}
{a b : ℝ}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hclosed : γ a = γ b)
{z w : ℂ}
(hw : w ∈ connectedComponentIn (γ '' Set.uIcc a b)ᶜ z)
:
The winding number of a closed absolutely continuous curve is constant on each connected component of the complement of its trace.