Affine coordinate changes for contour winding numbers

This file packages the translation and nonzero-scaling invariance of the generalized winding number into the affine-coordinate form used by local contour geometry. A sector or crossing is typically normalized by sending its distinguished point to the origin and rescaling the tangent direction; the results here let downstream finite-decomposition arguments use the single map z ↦ c * z + d rather than manually alternating the separate translation and scaling lemmas.

Main results

• Contour.windingNumber_affine — simultaneous affine change of the curve and base point preserves the generalized winding number when the linear coefficient is nonzero.
• Contour.windingNumber_affine_preimage — the same statement with an arbitrary target point, pulled back through the inverse affine map.
• Contour.IsNullHomologous.affine — null-homology is preserved by affine image of the curve and ambient set.
• Contour.isNullHomologous_affine_iff — the corresponding equivalence for nondegenerate affine coordinate changes.

Provenance

This is routine API around the Hungerbühler--Wasem generalized winding number from the contour integration roadmap; no formal source is vendored. It combines the existing Tau Ceti translation and scaling invariance lemmas.

theorem TauCeti.Contour.hasCauchyPVAt_inv_sub_affine {γ : ℝ → ℂ} {a b : ℝ} {z₀ c d L : ℂ} (h : HasCauchyPVAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀ L) (hc : c ≠ 0) : HasCauchyPVAt (fun (t : ℝ) => c * γ t + d) a b (fun (w : ℂ) => (w - (c * z₀ + d))⁻¹) (c * z₀ + d) L

Index principal value under an affine coordinate change. If c ≠ 0, applying z ↦ c * z + d to both the curve and the distinguished point transports the single-point Cauchy principal value of the winding kernel without changing its value. This is the composed translation/scaling form of hasCauchyPVAt_inv_sub_const_mul.

theorem TauCeti.Contour.cauchyPVExistsAt_inv_sub_affine {γ : ℝ → ℂ} {a b : ℝ} {z₀ c d : ℂ} (h : CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀) (hc : c ≠ 0) : CauchyPVExistsAt (fun (t : ℝ) => c * γ t + d) a b (fun (w : ℂ) => (w - (c * z₀ + d))⁻¹) (c * z₀ + d)

Existence form of hasCauchyPVAt_inv_sub_affine: affine coordinate changes with nonzero linear coefficient preserve existence of the index principal value.

theorem TauCeti.Contour.windingNumber_affine {γ : ℝ → ℂ} {a b : ℝ} {z₀ c d : ℂ} (hc : c ≠ 0) : windingNumber (fun (t : ℝ) => c * γ t + d) a b (c * z₀ + d) = windingNumber γ a b z₀

The generalized winding number is invariant under simultaneous affine coordinate change of the curve and base point, provided the linear coefficient is nonzero.

theorem TauCeti.Contour.windingNumber_affine_preimage {γ : ℝ → ℂ} {a b : ℝ} {z c d : ℂ} (hc : c ≠ 0) : windingNumber (fun (t : ℝ) => c * γ t + d) a b z = windingNumber γ a b (c⁻¹ * (z - d))

Pulling the base point back through a nondegenerate affine map gives the value of the winding number of the affine image about an arbitrary point.

theorem TauCeti.Contour.IsNullHomologous.affine {γ : ℝ → ℂ} {a b : ℝ} {c d : ℂ} {Ω : Set ℂ} (h : IsNullHomologous γ a b Ω) (hc : c ≠ 0) : IsNullHomologous (fun (t : ℝ) => c * γ t + d) a b ((fun (z : ℂ) => c * z + d) '' Ω)

Null-homology is preserved by affine coordinate change of the curve and ambient set, provided the linear coefficient is nonzero.

theorem TauCeti.Contour.IsNullHomologous.of_affine {γ : ℝ → ℂ} {a b : ℝ} {c d : ℂ} {Ω : Set ℂ} (h : IsNullHomologous (fun (t : ℝ) => c * γ t + d) a b ((fun (z : ℂ) => c * z + d) '' Ω)) (hc : c ≠ 0) : IsNullHomologous γ a b Ω

If the affine image of a curve is null-homologous in the affine image of a set, then the original curve is null-homologous in the original set.

theorem TauCeti.Contour.isNullHomologous_affine_iff {γ : ℝ → ℂ} {a b : ℝ} {c d : ℂ} {Ω : Set ℂ} (hc : c ≠ 0) : IsNullHomologous (fun (t : ℝ) => c * γ t + d) a b ((fun (z : ℂ) => c * z + d) '' Ω) ↔ IsNullHomologous γ a b Ω

A nondegenerate affine coordinate change preserves and reflects null-homology.