Winding numbers under absolutely continuous reparametrizations

Monotone or antitone absolutely continuous changes of parameter preserve the winding integral with its oriented image interval. Increasing parameters onto a given interval preserve its index; decreasing parameters onto that interval negate its index. Constant pieces and unbounded speeds are allowed.

theorem AbsolutelyContinuousOnInterval.windingNumber_comp {γ : ℝ → ℂ} {θ : ℝ → ℝ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ (θ a) (θ b)) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (horder : MonotoneOn θ (Set.Icc a b) ∨ AntitoneOn θ (Set.Icc a b)) (hz : z ∉ γ '' Set.uIcc (θ a) (θ b)) : TauCeti.Contour.windingNumber (γ ∘ θ) a b z = TauCeti.Contour.windingNumber γ (θ a) (θ b) z

An absolutely continuous monotone or antitone change of parameter preserves the off-trace winding number when the image interval carries its induced orientation.

theorem AbsolutelyContinuousOnInterval.windingNumber_comp_of_monotoneOn {γ : ℝ → ℂ} {θ : ℝ → ℝ} {a b c d : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hmono : MonotoneOn θ (Set.Icc a b)) (ha : θ a = c) (hb : θ b = d) (hz : z ∉ γ '' Set.uIcc c d) : TauCeti.Contour.windingNumber (γ ∘ θ) a b z = TauCeti.Contour.windingNumber γ c d z

An increasing absolutely continuous parameter onto the original interval preserves the winding number of an absolutely continuous curve away from its trace.

theorem AbsolutelyContinuousOnInterval.windingNumber_comp_of_antitoneOn {γ : ℝ → ℂ} {θ : ℝ → ℝ} {a b c d : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hanti : AntitoneOn θ (Set.Icc a b)) (ha : θ a = d) (hb : θ b = c) (hz : z ∉ γ '' Set.uIcc c d) : TauCeti.Contour.windingNumber (γ ∘ θ) a b z = -TauCeti.Contour.windingNumber γ c d z

A decreasing absolutely continuous parameter onto the original interval negates the winding number of an absolutely continuous curve away from its trace.

theorem AbsolutelyContinuousOnInterval.windingNumber_comp_lineMap {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hz : z ∉ γ '' Set.uIcc a b) : TauCeti.Contour.windingNumber (γ ∘ ⇑(AffineMap.lineMap a b)) 0 1 z = TauCeti.Contour.windingNumber γ a b z

Affine normalization to the unit interval preserves the off-trace winding number, with the original interval orientation, including constant intervals.