Aggregating per-window principal values across finitely many crossings

If the ε-truncated integral of g (γ t) * deriv γ t converges on each crossing window [t_i - r, t_i + r], the windows have disjoint interiors and lie in [a, b], and the curve keeps a positive distance from s off the windows, then the truncated integral over all of [a, b] converges — the single-point principal value exists (cauchyPVExistsAt_of_perWindow_tendsto_of_interiorDisjoint). Off the windows the truncation is eventually inactive and each between-piece integral is constant; the windows contribute their given limits; the pieces concatenate (HasCauchyPVAt.concat) along the sorted crossing list.

The per-window limits are hypotheses, so one aggregation serves every integrand: the simple-pole and higher-order per-window theorems both discharge them.

Main results

• Contour.cauchyPVExistsAt_of_perWindow_tendsto_of_interiorDisjoint — the single-point principal value on [a, b] from per-window convergence at finitely many crossings. The windows need only have disjoint interiors and lie in [a, b], so they may touch each other, or touch a or b; and the radius bound is required only when there is a window.
• Contour.hasCauchyPVAt_of_perWindow_boundary_tendsto_of_interiorDisjoint — the telescoping form: when the integrand has a curve-antiderivative Φ off the pole and each window limit is the boundary difference of Φ ∘ γ, the principal value is Φ (γ b) - Φ (γ a) — zero around a closed curve.
• Contour.exists_hasCauchyPVAt_re_eq_of_perWindow_tendsto_of_interiorDisjoint — like the first form above, but returns the aggregated value explicitly and pins its real part to the difference of a real boundary function Ψ, given only the real part of each piece and window value. Weaker than the telescoping form's shared complex antiderivative Φ, so it applies even when different windows need different branch choices for their imaginary part. All three instantiate Contour.sorted_crossing_gluing_induction (Crossing.Windows), the sorted-crossing-list geometry generalized to an arbitrary invariant Q : ℝ → ℝ → Prop closed under concatenation, including the value-carrying instantiations here (existential HasCauchyPVAt witnesses, or a known closed form) — so none needs its own copy of the recursion.

Provenance

Migrated from cpv_tendsto_along_sorted_corner, cpv_higherOrder_tendsto_along_sorted_corner and the aggregation steps of hasCauchyPV_inv_sub_multiCrossing_corner and hasCauchyPVOn_multiCrossing_higherOrder_corner of MultiCrossingCPV.lean in the AINTLIB LeanModularForms development, restated for a raw curve on [a, b] with a generic integrand and, in the telescoping form, a generic antiderivative (there the inductions are instantiated separately for the simple-pole and higher-order integrands). See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.exists_hasCauchyPVAt_re_eq_of_perWindow_tendsto_of_interiorDisjoint {γ : ℝ → ℂ} {s : ℂ} {g : ℂ → ℂ} {Ψ : ℝ → ℝ} {a b r m : ℝ} (hab : a ≤ b) (crossings : Finset ℝ) (hr_nonneg : crossings.Nonempty → 0 ≤ r) (h_lo : ∀ t ∈ crossings, a ≤ t - r) (h_hi : ∀ t ∈ crossings, t + r ≤ b) (h_pair : ∀ t ∈ crossings, ∀ t' ∈ crossings, t' ≠ t → 2 * r ≤ |t - t'|) (h_int_tr : ∀ (ε : ℝ), 0 < ε → IntervalIntegrable (fun (t : ℝ) => if ‖γ t - s‖ > ε then g (γ t) * deriv γ t else 0) MeasureTheory.volume a b) (h_piece_re : ∀ (l u : ℝ), a ≤ l → l ≤ u → u ≤ b → (∀ t ∈ Set.Icc l u, m ≤ ‖γ t - s‖) → (∫ (t : ℝ) in l..u, g (γ t) * deriv γ t).re = Ψ u - Ψ l) (h_win : ∀ t ∈ crossings, ∃ (v : ℂ), v.re = Ψ (t + r) - Ψ (t - r) ∧ Filter.Tendsto (fun (ε : ℝ) => ∫ (u : ℝ) in t - r..t + r, if ‖γ u - s‖ > ε then g (γ u) * deriv γ u else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds v)) (h_far : 0 < m ∧ ∀ u ∈ Set.Icc a b, (∀ t ∈ crossings, u ∉ Set.Ioo (t - r) (t + r)) → m ≤ ‖γ u - s‖) : ∃ (L : ℂ), HasCauchyPVAt γ a b g s L ∧ L.re = Ψ b - Ψ a

Real-part boundary aggregation: like cauchyPVExistsAt_of_perWindow_tendsto_of_interiorDisjoint, but each plain piece and each window additionally has its real part pinned to the difference of a real boundary function Ψ — weaker than sharing one complex antiderivative Φ across every window, as hasCauchyPVAt_of_perWindow_boundary_tendsto_of_interiorDisjoint requires (different windows may need different branch choices for their imaginary part, so no single Φ need exist). Returns the aggregated principal value explicitly, together with the fact that its real part telescopes to Ψ b - Ψ a.

theorem TauCeti.Contour.cauchyPVExistsAt_of_perWindow_tendsto_of_interiorDisjoint {γ : ℝ → ℂ} {s : ℂ} {g : ℂ → ℂ} {a b r : ℝ} (hab : a ≤ b) (crossings : Finset ℝ) (hr_nonneg : crossings.Nonempty → 0 ≤ r) (h_lo : ∀ t ∈ crossings, a ≤ t - r) (h_hi : ∀ t ∈ crossings, t + r ≤ b) (h_pair : ∀ t ∈ crossings, ∀ t' ∈ crossings, t' ≠ t → 2 * r ≤ |t - t'|) (h_int_tr : ∀ (ε : ℝ), 0 < ε → IntervalIntegrable (fun (t : ℝ) => if ‖γ t - s‖ > ε then g (γ t) * deriv γ t else 0) MeasureTheory.volume a b) (h_win : ∀ t ∈ crossings, ∃ (v : ℂ), Filter.Tendsto (fun (ε : ℝ) => ∫ (u : ℝ) in t - r..t + r, if ‖γ u - s‖ > ε then g (γ u) * deriv γ u else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds v)) (h_far : ∃ (m : ℝ), 0 < m ∧ ∀ u ∈ Set.Icc a b, (∀ t ∈ crossings, u ∉ Set.Ioo (t - r) (t + r)) → m ≤ ‖γ u - s‖) : CauchyPVExistsAt γ a b g s

The single-point principal value from per-window convergence: if the ε-truncated integral of g (γ t) * deriv γ t converges on each crossing window (disjoint interiors, lying in [a, b] — they may touch each other, or touch a or b), the truncations are integrable on [a, b], and the curve keeps a positive distance from s off the windows, then the principal value at s exists on [a, b]. The per-window limits are hypotheses, so both the simple-pole and higher-order per-window theorems discharge them.

theorem TauCeti.Contour.hasCauchyPVAt_of_perWindow_boundary_tendsto_of_interiorDisjoint {γ : ℝ → ℂ} {s : ℂ} {g Φ : ℂ → ℂ} {a b r : ℝ} (hab : a ≤ b) (crossings : Finset ℝ) (hr_nonneg : crossings.Nonempty → 0 ≤ r) (h_lo : ∀ t ∈ crossings, a ≤ t - r) (h_hi : ∀ t ∈ crossings, t + r ≤ b) (h_pair : ∀ t ∈ crossings, ∀ t' ∈ crossings, t' ≠ t → 2 * r ≤ |t - t'|) (h_int_tr : ∀ (ε : ℝ), 0 < ε → IntervalIntegrable (fun (t : ℝ) => if ‖γ t - s‖ > ε then g (γ t) * deriv γ t else 0) MeasureTheory.volume a b) (h_plain_eq : ∀ (l u : ℝ), a ≤ l → l ≤ u → u ≤ b → (∀ t ∈ Set.Icc l u, γ t ≠ s) → ∫ (t : ℝ) in l..u, g (γ t) * deriv γ t = Φ (γ u) - Φ (γ l)) (h_win : ∀ t ∈ crossings, Filter.Tendsto (fun (ε : ℝ) => ∫ (u : ℝ) in t - r..t + r, if ‖γ u - s‖ > ε then g (γ u) * deriv γ u else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Φ (γ (t + r)) - Φ (γ (t - r))))) (h_far : ∃ (m : ℝ), 0 < m ∧ ∀ u ∈ Set.Icc a b, (∀ t ∈ crossings, u ∉ Set.Ioo (t - r) (t + r)) → m ≤ ‖γ u - s‖) : HasCauchyPVAt γ a b g s (Φ (γ b) - Φ (γ a))

Telescoping per-window aggregation: when the plain integrand has a curve-antiderivative Φ on pole-free pieces and each window limit is the boundary difference of Φ ∘ γ, the principal value on [a, b] is Φ (γ b) - Φ (γ a) — in particular zero around a closed curve. The higher-order per-window limits have exactly this boundary-difference shape.