Simultaneous excision of finitely many crossing windows

Hungerbühler–Wasem Proposition 2.2 replaces every crossing of a closed piecewise-C¹ immersion by a circular cap. Crossing.Excision constructs this replacement for one window; this file iterates that construction over a finite list of pairwise disjoint windows.

CircularCapWindow records the five parameters of one replacement. Applying exciseCrossings to a pairwise disjoint list has the expected simultaneous description: it is the prescribed cap on each window and the original curve off their union. It remains piecewise C¹ when the windows lie strictly inside the parameter interval and their cap endpoints match the original curve, and remains closed when the interval endpoints lie outside every window. Without a disjointness assumption, it avoids the crossing centre on Icc a b when every window meeting that interval has nonzero radius and the windows cover every parameter there at which the original curve meets that centre.

This is the finite geometric surgery producing the modified curve in Proposition 2.2. The winding number accounting is deliberately separate: Winding.Number.Partition supplies finite additivity, while the local crossing contribution is computed by the crossing-angle theory.

Main definitions

• TauCeti.Contour.CircularCapWindow — the parameters of one circular-cap replacement.
• TauCeti.Contour.CircularCapWindow.localContribution — the window winding number minus the cap's angular contribution.
• TauCeti.Contour.exciseCrossings — iteration of exciseCrossing over a finite list.

Main results

• TauCeti.Contour.exciseCrossings_eqOn_window and TauCeti.Contour.exciseCrossings_eqOn_compl — the simultaneous pointwise description.
• TauCeti.Contour.IsPiecewiseC1On.exciseCrossings — finite excision preserves piecewise C¹ regularity.
• TauCeti.Contour.exciseCrossings_closed — finite excision preserves closedness.
• TauCeti.Contour.exciseCrossings_ne_center — the resulting curve avoids the centre on Icc a b when the windows cover every crossing there.

References

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

structure TauCeti.Contour.CircularCapWindow : Type

The parameters of a circular cap replacing one crossing window. Every field contributes to the replacement: lower and upper delimit the window, radius is the signed radial scale, and startAngle and endAngle specify the cap's angular sweep.

• radius : ℝ

  Signed radial scale of the cap.

• lower : ℝ

  Lower endpoint of the parameter window.

• upper : ℝ

  Upper endpoint of the parameter window.

• startAngle : ℝ

  Angle of the cap at the lower endpoint.

• endAngle : ℝ

  Angle of the cap at the upper endpoint.

def TauCeti.Contour.CircularCapWindow.interval (W : CircularCapWindow) : Set ℝ

The closed parameter interval replaced by a circular cap.

Equations

• W.interval = Set.Icc W.lower W.upper

@[simp]

theorem TauCeti.Contour.CircularCapWindow.mem_interval_iff {W : CircularCapWindow} {t : ℝ} : t ∈ W.interval ↔ W.lower ≤ t ∧ t ≤ W.upper

Membership in a window is membership in its closed endpoint interval.

theorem TauCeti.Contour.CircularCapWindow.disjoint_interval_of_upper_lt_lower {W V : CircularCapWindow} (h : W.upper < V.lower) : Disjoint W.interval V.interval

Two windows listed strictly from left to right have disjoint closed intervals.

noncomputable def TauCeti.Contour.CircularCapWindow.cap (W : CircularCapWindow) (s : ℂ) : ℝ → ℂ

The circular cap prescribed by a crossing window.

Equations

• W.cap s = TauCeti.Contour.circleCap s W.radius W.lower W.upper W.startAngle W.endAngle

theorem TauCeti.Contour.CircularCapWindow.cap_apply (W : CircularCapWindow) (s : ℂ) (t : ℝ) : W.cap s t = circleMap s W.radius (W.startAngle + (W.endAngle - W.startAngle) / (W.upper - W.lower) * (t - W.lower))

At t, the bundled cap is the point at the corresponding affine interpolation of its endpoint angles.

@[simp]

theorem TauCeti.Contour.CircularCapWindow.cap_left (W : CircularCapWindow) (s : ℂ) : W.cap s W.lower = circleMap s W.radius W.startAngle

The bundled cap starts at its prescribed angle at the lower endpoint.

@[simp]

theorem TauCeti.Contour.CircularCapWindow.cap_right (W : CircularCapWindow) (s : ℂ) (hlu : W.lower ≠ W.upper) : W.cap s W.upper = circleMap s W.radius W.endAngle

The bundled cap ends at its prescribed angle at a distinct upper endpoint.

theorem TauCeti.Contour.CircularCapWindow.contDiff_cap (W : CircularCapWindow) (s : ℂ) : ContDiff ℝ 1 (W.cap s)

A bundled cap is C¹.

theorem TauCeti.Contour.CircularCapWindow.cap_ne_center (W : CircularCapWindow) {s : ℂ} (hr : W.radius ≠ 0) {t : ℝ} : W.cap s t ≠ s

A bundled cap with nonzero signed radius misses its centre.

theorem TauCeti.Contour.CircularCapWindow.cauchyPVExistsAt_cap (W : CircularCapWindow) (s : ℂ) (a b : ℝ) : CauchyPVExistsAt (W.cap s) a b (fun (z : ℂ) => (z - s)⁻¹) s

The index principal value exists along a bundled circular cap.

theorem TauCeti.Contour.CircularCapWindow.windingNumber_cap (W : CircularCapWindow) (s : ℂ) (hr : W.radius ≠ 0) (hlu : W.lower ≠ W.upper) : windingNumber (W.cap s) W.lower W.upper s = ↑(W.endAngle - W.startAngle) / (2 * ↑Real.pi)

The winding number of a nondegenerate bundled cap is its angular extent over 2π.

noncomputable def TauCeti.Contour.CircularCapWindow.localContribution (W : CircularCapWindow) (γ : ℝ → ℂ) (s : ℂ) : ℂ

The contribution of one circular-cap window: the winding number of the original curve across the window minus the cap's angular term. Under the nondegeneracy hypotheses of localContribution_eq_sub_windingNumber_cap, this is the window winding number minus the cap winding number.

Equations

• W.localContribution γ s = TauCeti.Contour.windingNumber γ W.lower W.upper s - ↑(W.endAngle - W.startAngle) / (2 * ↑Real.pi)

theorem TauCeti.Contour.CircularCapWindow.localContribution_def (W : CircularCapWindow) (γ : ℝ → ℂ) (s : ℂ) : W.localContribution γ s = windingNumber γ W.lower W.upper s - ↑(W.endAngle - W.startAngle) / (2 * ↑Real.pi)

The defining window-minus-angular-term formula for a local contribution.

theorem TauCeti.Contour.CircularCapWindow.localContribution_eq_sub_windingNumber_cap (W : CircularCapWindow) (γ : ℝ → ℂ) (s : ℂ) (hr : W.radius ≠ 0) (hlu : W.lower ≠ W.upper) : W.localContribution γ s = windingNumber γ W.lower W.upper s - windingNumber (W.cap s) W.lower W.upper s

The local contribution is the difference between the window winding number and the winding number of the prescribed cap.

noncomputable def TauCeti.Contour.CircularCapWindow.excise (W : CircularCapWindow) (γ : ℝ → ℂ) (s : ℂ) : ℝ → ℂ

Replace one crossing window of γ by its prescribed circular cap about s.

Equations

• W.excise γ s = TauCeti.Contour.exciseCrossing γ s W.radius W.lower W.upper W.startAngle W.endAngle

theorem TauCeti.Contour.CircularCapWindow.excise_def (W : CircularCapWindow) (γ : ℝ → ℂ) (s : ℂ) : W.excise γ s = exciseCrossing γ s W.radius W.lower W.upper W.startAngle W.endAngle

A bundled one-window excision is the corresponding unbundled circular-cap excision.

@[simp]

theorem TauCeti.Contour.CircularCapWindow.excise_of_mem (W : CircularCapWindow) {γ : ℝ → ℂ} {s : ℂ} {t : ℝ} (ht : t ∈ W.interval) : W.excise γ s t = W.cap s t

On its window, a one-window excision is the prescribed cap.

@[simp]

theorem TauCeti.Contour.CircularCapWindow.excise_of_notMem (W : CircularCapWindow) {γ : ℝ → ℂ} {s : ℂ} {t : ℝ} (ht : t ∉ W.interval) : W.excise γ s t = γ t

Off its window, a one-window excision is the original curve.

theorem TauCeti.Contour.pairwise_disjoint_interval_of_pairwise_upper_lt_lower {windows : List CircularCapWindow} (hordered : List.Pairwise (fun (W V : CircularCapWindow) => W.upper < V.lower) windows) : List.Pairwise (fun (W V : CircularCapWindow) => Disjoint W.interval V.interval) windows

Windows listed strictly from left to right have pairwise disjoint closed intervals.

noncomputable def TauCeti.Contour.exciseCrossings (γ : ℝ → ℂ) (s : ℂ) : List CircularCapWindow → ℝ → ℂ

Replace each window in windows by its circular cap about s. Later replacements act on the curve produced by earlier ones. For pairwise disjoint windows the order is immaterial pointwise, and exciseCrossings_eqOn_window gives the simultaneous description.

Equations

• TauCeti.Contour.exciseCrossings γ s windows = List.foldl (fun (δ : ℝ → ℂ) (W : TauCeti.Contour.CircularCapWindow) => W.excise δ s) γ windows

@[simp]

theorem TauCeti.Contour.exciseCrossings_nil (γ : ℝ → ℂ) (s : ℂ) : exciseCrossings γ s [] = γ

Excising an empty list of windows leaves the curve unchanged.

@[simp]

theorem TauCeti.Contour.exciseCrossings_cons (γ : ℝ → ℂ) (s : ℂ) (W : CircularCapWindow) (windows : List CircularCapWindow) : exciseCrossings γ s (W :: windows) = exciseCrossings (W.excise γ s) s windows

Excising a nonempty list first replaces its head window.

theorem TauCeti.Contour.exciseCrossings_eqOn_compl {γ : ℝ → ℂ} {s : ℂ} {windows : List CircularCapWindow} {S : Set ℝ} (hdisj : ∀ W ∈ windows, Disjoint S W.interval) : Set.EqOn (exciseCrossings γ s windows) γ S

Away from every window, finite excision agrees with the original curve.

theorem TauCeti.Contour.exciseCrossings_apply_of_forall_notMem {γ : ℝ → ℂ} {s : ℂ} {windows : List CircularCapWindow} {t : ℝ} (ht : ∀ W ∈ windows, t ∉ W.interval) : exciseCrossings γ s windows t = γ t

Pointwise form of exciseCrossings_eqOn_compl.

theorem TauCeti.Contour.exciseCrossings_eqOn_window {γ : ℝ → ℂ} {s : ℂ} {windows : List CircularCapWindow} (hpw : List.Pairwise (fun (W V : CircularCapWindow) => Disjoint W.interval V.interval) windows) {W : CircularCapWindow} (hW : W ∈ windows) : Set.EqOn (exciseCrossings γ s windows) (W.cap s) W.interval

For pairwise disjoint windows, finite excision is the prescribed cap on each window.

theorem TauCeti.Contour.exciseCrossings_perm {γ : ℝ → ℂ} {s : ℂ} {windows windows' : List CircularCapWindow} (hpw : List.Pairwise (fun (W V : CircularCapWindow) => Disjoint W.interval V.interval) windows) (hperm : windows.Perm windows') : exciseCrossings γ s windows = exciseCrossings γ s windows'

Pairwise-disjoint finite excision is independent of the ordering of the windows.

theorem TauCeti.Contour.IsPiecewiseC1On.exciseCrossings {γ : ℝ → ℂ} {s : ℂ} {a b : ℝ} {windows : List CircularCapWindow} (hγ : IsPiecewiseC1On γ a b) (hpw : List.Pairwise (fun (W V : CircularCapWindow) => Disjoint W.interval V.interval) windows) (hinside : ∀ W ∈ windows, a < W.lower ∧ W.lower < W.upper ∧ W.upper < b) (hstart : ∀ W ∈ windows, γ W.lower = circleMap s W.radius W.startAngle) (hend : ∀ W ∈ windows, γ W.upper = circleMap s W.radius W.endAngle) : IsPiecewiseC1On (Contour.exciseCrossings γ s windows) a b

Finite excision preserves piecewise-C¹ regularity when the windows are pairwise disjoint, strictly inside the parameter interval, and their cap endpoints agree with the original curve.

theorem TauCeti.Contour.exciseCrossings_closed {γ : ℝ → ℂ} {s : ℂ} {a b : ℝ} {windows : List CircularCapWindow} (hclosed : γ a = γ b) (hendpoints : ∀ W ∈ windows, a ∉ W.interval ∧ b ∉ W.interval) : exciseCrossings γ s windows a = exciseCrossings γ s windows b

Finite excision preserves closedness when both parameter endpoints lie outside every replacement window.

theorem TauCeti.Contour.exciseCrossings_ne_center {γ : ℝ → ℂ} {s : ℂ} {a b : ℝ} {windows : List CircularCapWindow} (hr : ∀ W ∈ windows, (W.interval ∩ Set.Icc a b).Nonempty → W.radius ≠ 0) (hcover : ∀ t ∈ Set.Icc a b, γ t = s → ∃ W ∈ windows, t ∈ W.interval) (t : ℝ) : t ∈ Set.Icc a b → exciseCrossings γ s windows t ≠ s

If closed windows cover every parameter in Icc a b where γ meets s, and every window meeting Icc a b has nonzero radius, finite excision produces a curve avoiding s there, even when the windows overlap.