Model sectors as contour cycles

Hungerbühler--Wasem Proposition 2.2 decomposes a closed immersed curve, as a contour cycle, into a cycle avoiding the distinguished point and one model-sector cycle for each crossing. The raw model sector, its piecewise-C¹ regularity, and its winding number are constructed in ModelSector.Closed; this file packages it as the closed-curve generator that the cycle decomposition uses.

Main definitions

• Contour.modelSectorCurve -- the model sector as a closed piecewise-C¹ curve.
• Contour.modelSectorCycle -- the corresponding one-generator contour cycle.

Main results

• Contour.Cycle.integral_modelSectorCycle -- its cycle integral is the raw contour integral.
• Contour.Cycle.windingNumber_modelSectorCycle_eq_raw -- its cycle winding number is the raw winding number.
• Contour.Cycle.windingNumber_modelSectorCycle -- at the sector center its winding number is α / 2π.

References

• N. Hungerbühler and M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), equation (2.4) and Proposition 2.2.

noncomputable def TauCeti.Contour.modelSectorCurve (z₀ : ℂ) (r φ α : ℝ) (hr : 0 ≤ r) (hα : 0 ≤ α) : PiecewiseC1ClosedCurve

The model sector bundled as a closed piecewise-C¹ curve.

Equations

• TauCeti.Contour.modelSectorCurve z₀ r φ α hr hα = TauCeti.Contour.PiecewiseC1ClosedCurve.of (TauCeti.Contour.modelSector z₀ r φ α) ⋯ ⋯

noncomputable def TauCeti.Contour.modelSectorCycle (z₀ : ℂ) (r φ α : ℝ) (hr : 0 ≤ r) (hα : 0 ≤ α) : Cycle

The model sector as a one-generator contour cycle.

Equations

• TauCeti.Contour.modelSectorCycle z₀ r φ α hr hα = FreeAbelianGroup.of (TauCeti.Contour.modelSectorCurve z₀ r φ α hr hα)

@[simp]

theorem TauCeti.Contour.modelSectorCurve_a (z₀ : ℂ) (r φ α : ℝ) (hr : 0 ≤ r) (hα : 0 ≤ α) : (modelSectorCurve z₀ r φ α hr hα).a = -r

The bundled model sector starts at -r.

@[simp]

theorem TauCeti.Contour.modelSectorCurve_b (z₀ : ℂ) (r φ α : ℝ) (hr : 0 ≤ r) (hα : 0 ≤ α) : (modelSectorCurve z₀ r φ α hr hα).b = r + α

The bundled model sector ends at r + α.

@[simp]

theorem TauCeti.Contour.modelSectorCurve_apply {z₀ : ℂ} {r φ α t : ℝ} (hr : 0 ≤ r) (hα : 0 ≤ α) (ht : t ∈ Set.uIcc (-r) (r + α)) : Function.extend Subtype.val (modelSectorCurve z₀ r φ α hr hα).toFun 0 t = modelSector z₀ r φ α t

On its parameter interval, the bundled model sector agrees with the raw model sector.

@[simp]

theorem TauCeti.Contour.Cycle.trace_modelSectorCycle (z₀ : ℂ) (r φ α : ℝ) (hr : 0 ≤ r) (hα : 0 ≤ α) : (modelSectorCycle z₀ r φ α hr hα).trace = modelSector z₀ r φ α '' Set.uIcc (-r) (r + α)

The trace of the model-sector cycle is the image of its raw parametrization.

@[simp]

theorem TauCeti.Contour.Cycle.integral_modelSectorCycle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z₀ : ℂ) (r φ α : ℝ) (hr : 0 ≤ r) (hα : 0 ≤ α) : (integral f) (modelSectorCycle z₀ r φ α hr hα) = ∫ (t : ℝ) in -r..r + α, deriv (modelSector z₀ r φ α) t • f (modelSector z₀ r φ α t)

Integrating over the model-sector cycle gives the raw contour integral over the model sector.

@[simp]

theorem TauCeti.Contour.Cycle.windingNumber_modelSectorCycle_eq_raw (z z₀ : ℂ) (r φ α : ℝ) (hr : 0 ≤ r) (hα : 0 ≤ α) : (windingNumber z) (modelSectorCycle z₀ r φ α hr hα) = Contour.windingNumber (modelSector z₀ r φ α) (-r) (r + α) z

The winding number of the model-sector cycle is the winding number of its raw parametrization.

theorem TauCeti.Contour.Cycle.windingNumber_modelSectorCycle {z₀ : ℂ} {r : ℝ} (hr : 0 < r) (φ : ℝ) {α : ℝ} (hα : 0 ≤ α) : (windingNumber z₀) (modelSectorCycle z₀ r φ α ⋯ hα) = ↑α / (2 * ↑Real.pi)

The model-sector cycle has winding number α / 2π about its corner. This is the cycle form of Contour.windingNumber_closedModelSector, ready to be summed in the finite crossing decomposition of Hungerbühler--Wasem Proposition 2.2.