Pairwise-disjoint windows around a finite set of crossings

For a finite set of crossing parameters in an open interval (a, b), off a finite exceptional set, there is a common radius r > 0 whose closed windows [t_i - r, t_i + r] stay within [a, b], are pairwise disjoint, and avoid the exceptional set (exists_common_window_radius). Inside such a window, completeness of the crossing set makes the crossing unique (eq_of_mem_window_of_eq), and the distance from the curve to the crossed point is bounded below off the crossing (exists_window_dist_lower_bound) — the geometric scaffolding that localizes the principal-value analysis to one crossing per window.

Main results

• Contour.exists_common_window_radius — the common window radius.
• Contour.exists_common_window_radius_le — a common window radius additionally held below a positive per-crossing bound, with strict endpoint margins.
• Contour.eq_of_mem_window_of_eq_of_le_of_lt — in-window uniqueness of the crossing, from margins at that crossing alone.
• Contour.eq_of_mem_window_of_eq — the same for a whole crossing family.
• Contour.eq_of_mem_window_of_eq_of_lt_of_two_mul_lt — the same, from the strict margins returned by exists_common_window_radius_le.
• Contour.exists_window_dist_lower_bound — a positive lower bound for ‖γ t - s‖ on the two closed half-windows excluding the crossing.
• Contour.exists_complement_windows_dist_lower_bound — a positive lower bound for ‖γ t - s‖ on the complement of the open crossing windows in [a, b].
• Contour.sorted_crossing_gluing_induction — a generic invariant closed under piece concatenation and holding on every plain piece and crossing window holds on [a, b], by induction on the sorted crossing list; every consumer of Crossing.PVAggregation's per-window aggregation instantiates this one induction.

Provenance

Migrated from multi_pole_common_radius, multi_pole_local_uniqueness, multi_pole_local_far_bound (CPVExistenceMulti.lean), and multi_pole_smooth_complement_far_bound (LocalCutoffs.lean) in the AINTLIB LeanModularForms development, restated for a raw curve over an arbitrary interval (there the domain is the bundled [0, 1] of a ClosedPwC1Immersion), with the half-window bounds from Contour.exists_curve_dist_lower_bound rather than a bespoke compactness argument. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.exists_common_window_radius {a b : ℝ} {crossings P : Finset ℝ} (h_nonempty : crossings.Nonempty) (h_Ioo : ∀ t ∈ crossings, t ∈ Set.Ioo a b) (h_off : ∀ t ∈ crossings, t ∉ P) : ∃ r > 0, (∀ t ∈ crossings, a + r ≤ t ∧ t ≤ b - r) ∧ (∀ t ∈ crossings, ∀ t' ∈ crossings, t' ≠ t → 2 * r < |t - t'|) ∧ ∀ t ∈ crossings, ∀ p ∈ P, r < |t - p|

The common window radius: for a finite set of crossings in (a, b) avoiding a finite exceptional set P, there is r > 0 such that every window [t_i - r, t_i + r] stays within [a, b], distinct crossings are more than 2r apart (so the windows are pairwise disjoint), and no exceptional point comes within r of a crossing.

theorem TauCeti.Contour.exists_common_window_radius_le {a b : ℝ} {crossings : Finset ℝ} (h_Ioo : ∀ t ∈ crossings, t ∈ Set.Ioo a b) (R : ℝ → ℝ) (hR_pos : ∀ t ∈ crossings, 0 < R t) : ∃ r > 0, (∀ t ∈ crossings, a + r < t ∧ t < b - r) ∧ (∀ t ∈ crossings, ∀ t' ∈ crossings, t' ≠ t → 2 * r < |t - t'|) ∧ ∀ t ∈ crossings, r ≤ R t

A common window radius below a prescribed per-crossing bound. The P = ∅ case of exists_common_window_radius with the radius additionally placed under a given positive R t at every crossing — which is what lets a family of per-crossing window results, each valid only below its own radius, be applied at one shared radius. There is no exceptional-set clause; use exists_common_window_radius directly when one is needed.

Unlike that lemma this one does not ask for a nonempty family: for no crossings all three conditions are vacuous and any positive radius serves.

The endpoint margins come out strict here: the radius is chosen strictly below the one that lemma supplies, so it clears both endpoints with room to spare.

theorem TauCeti.Contour.eq_of_mem_window_of_eq_of_le_of_lt {α : Type u_1} {γ : ℝ → α} {s : α} {a b : ℝ} {crossings : Finset ℝ} {r t_i : ℝ} (h_endpts : a + r ≤ t_i ∧ t_i ≤ b - r) (h_pairwise : ∀ t' ∈ crossings, t' ≠ t_i → r < |t_i - t'|) (h_complete : ∀ t ∈ Set.Icc a b, γ t = s → t ∈ crossings) {t : ℝ} (ht : t ∈ Set.Icc (t_i - r) (t_i + r)) (h_eq : γ t = s) : t = t_i

In-window uniqueness of the crossing, from margins at that crossing alone. If the window [t_i - r, t_i + r] lies inside [a, b], every listed crossing other than t_i is more than r from t_i, and the listing is complete — every parameter of [a, b] where γ takes the value s is listed — then the only parameter of that window where γ takes the value s is t_i itself.

This is the pointwise core: nothing is assumed about the other crossings' own windows, and t_i need not itself be listed. eq_of_mem_window_of_eq is the family-wide form, for callers holding margins for every crossing at once. Stated for a bare function; no regularity is used.

theorem TauCeti.Contour.eq_of_mem_window_of_eq {α : Type u_1} {γ : ℝ → α} {s : α} {a b : ℝ} {crossings : Finset ℝ} {r : ℝ} (h_endpts : ∀ t ∈ crossings, a + r ≤ t ∧ t ≤ b - r) (h_pairwise : ∀ t ∈ crossings, ∀ t' ∈ crossings, t' ≠ t → r < |t - t'|) (h_complete : ∀ t ∈ Set.Icc a b, γ t = s → t ∈ crossings) {t_i : ℝ} (ht_i : t_i ∈ crossings) {t : ℝ} (ht : t ∈ Set.Icc (t_i - r) (t_i + r)) (h_eq : γ t = s) : t = t_i

In-window uniqueness of the crossing: with windows inside [a, b], distinct crossings more than r apart, and completeness — every parameter of [a, b] where γ takes the value s is a listed crossing — the only parameter of the window [t_i - r, t_i + r] where γ takes the value s is t_i itself. Stated for a bare function; no regularity is used.

The family-wide form, for callers holding margins for every crossing at once; it reads them off at t_i and defers to eq_of_mem_window_of_eq_of_le_of_lt.

theorem TauCeti.Contour.eq_of_mem_window_of_eq_of_lt_of_two_mul_lt {α : Type u_1} {γ : ℝ → α} {s : α} {a b : ℝ} {crossings : Finset ℝ} {r t_i : ℝ} (h_endpts : a + r < t_i ∧ t_i < b - r) (h_pairwise : ∀ t' ∈ crossings, t' ≠ t_i → 2 * r < |t_i - t'|) (h_complete : ∀ t ∈ Set.Icc a b, γ t = s → t ∈ crossings) {t : ℝ} (ht : t ∈ Set.Icc (t_i - r) (t_i + r)) (h_eq : γ t = s) : t = t_i

In-window uniqueness of the crossing, from a common window radius. The variant of eq_of_mem_window_of_eq_of_le_of_lt whose margins are the strict ones exists_common_window_radius_le returns, read off at t_i: t_i more than r inside the endpoints, and every other crossing more than 2 * r from it. No sign condition on r is required — halving the pairwise margin needs 0 ≤ r, but a negative radius leaves the window [t_i - r, t_i + r] empty, so ht supplies it.

theorem TauCeti.Contour.exists_window_dist_lower_bound {γ : ℝ → ℂ} {s : ℂ} {t_i r : ℝ} (hγ_cont : ContinuousOn γ (Set.Icc (t_i - r) (t_i + r))) (h_unique : ∀ t ∈ Set.Icc (t_i - r) (t_i + r), γ t = s → t = t_i) {r' : ℝ} (hr'_pos : 0 < r') (hr'_le : r' ≤ r) : ∃ m > 0, (∀ t ∈ Set.Icc (t_i - r) (t_i - r'), m ≤ ‖γ t - s‖) ∧ ∀ t ∈ Set.Icc (t_i + r') (t_i + r), m ≤ ‖γ t - s‖

Positive distance bound on the half-windows: when the crossing is unique in its window, ‖γ t - s‖ is bounded below by a common m > 0 on the two closed half-windows [t_i - r, t_i - r'] and [t_i + r', t_i + r] excluding the crossing.

theorem TauCeti.Contour.exists_complement_windows_dist_lower_bound {γ : ℝ → ℂ} {s : ℂ} {a b : ℝ} {crossings : Finset ℝ} (hγ_cont : ContinuousOn γ (Set.Icc a b)) (h_complete : ∀ t ∈ Set.Icc a b, γ t = s → t ∈ crossings) (r_at : ℝ → ℝ) (hr_pos : ∀ t ∈ crossings, 0 < r_at t) : ∃ m > 0, ∀ t ∈ Set.Icc a b, (∀ t_i ∈ crossings, t ∉ Set.Ioo (t_i - r_at t_i) (t_i + r_at t_i)) → m ≤ ‖γ t - s‖

Positive distance bound off the crossing windows: with every value-s parameter of [a, b] a listed crossing, ‖γ t - s‖ is bounded below by a positive m on the complement of the open crossing windows in [a, b] — the far bound on the smooth part of a multi-crossing excision.

theorem TauCeti.Contour.sorted_crossing_gluing_induction {E : Type u_1} [NormedAddCommGroup E] {γ : ℝ → E} {s : E} {Q : ℝ → ℝ → Prop} {A b r m : ℝ} (h_piece : ∀ (l u : ℝ), A ≤ l → l ≤ u → u ≤ b → (∀ t ∈ Set.Icc l u, m ≤ ‖γ t - s‖) → Q l u) (hglue : ∀ (l u₀ u : ℝ), l ≤ u₀ → u₀ ≤ u → Q l u₀ → Q u₀ u → Q l u) (sorted : List ℝ) : sorted.SortedLT → (sorted ≠ [] → 0 ≤ r) → ∀ (a : ℝ), A ≤ a → a ≤ b → (∀ t ∈ sorted, a ≤ t - r) → (∀ t ∈ sorted, t + r ≤ b) → (∀ t ∈ sorted, ∀ t' ∈ sorted, t' ≠ t → 2 * r ≤ |t - t'|) → (∀ t ∈ sorted, Q (t - r) (t + r)) → (∀ u ∈ Set.Icc a b, (∀ t ∈ sorted, u ∉ Set.Ioo (t - r) (t + r)) → m ≤ ‖γ u - s‖) → Q a b

Generic sorted-crossing-window gluing induction. An invariant Q : ℝ → ℝ → Prop that holds on every plain piece where the curve keeps distance ≥ m from s (h_piece) and on every crossing window (h_win), and is closed under concatenation at a shared endpoint (hglue), holds on [a, b], by induction on the sorted crossing list. Every consumer instantiates this one induction — whether its own invariant is a bare Prop (interval-integrability) or carries an aggregated value (∃ v, HasCauchyPVAt ... v, or HasCauchyPVAt ... (Φ (γ u) - Φ (γ l)) for a known closed form) — so none needs its own copy of the list recursion. Crossing-window-independent of the principal-value machinery it primarily feeds, so it lives here alongside the geometric window scaffolding above rather than in Crossing.PVAggregation.