The excised integrand is integrable

An ε-excision replaces the integrand by 0 wherever the curve comes within ε of one of finitely many centres. That is what makes the integrand integrable when the unexcised one is not: the singularities all sit at the centres, and the excision deletes a neighbourhood of each. This file records the resulting integrability, at a fixed ε.

What survives the excision is φ ∘ γ times deriv γ on parameters at distance ≥ ε from every centre. Over a bounded interval the curve's image there is compact, so a φ continuous on it is bounded; with deriv γ bounded the excised integrand is bounded, and it is measurable because deriv always is. Bounded and measurable on a bounded interval is integrable.

Main results

• TauCeti.Contour.intervalIntegrable_excised_of_continuousOn: the excised integrand is interval-integrable.

theorem TauCeti.Contour.intervalIntegrable_excised_of_continuousOn {γ : ℝ → ℂ} {φ : ℂ → ℂ} {S : Finset ℂ} {a b ε : ℝ} (hγc : ContinuousOn γ (Set.uIcc a b)) (hd : IntervalIntegrable (deriv γ) MeasureTheory.volume a b) (hφ : ContinuousOn φ (γ '' Set.uIcc a b ∩ {z : ℂ | ∀ s ∈ S, ε ≤ ‖z - s‖})) : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else φ (γ t) * deriv γ t) MeasureTheory.volume a b

The excised integrand is integrable. Off the excision the curve stays at distance > ε from every centre, so over [a, b] its values lie in a compact set on which φ is continuous, hence bounded. The excised integrand is that bounded factor times deriv γ, so it is integrable whenever deriv γ is.

hφ asks for continuity only on the closed condition ε ≤ ‖z - s‖, which is what makes the relevant set compact; the excision itself keeps the strict ε < ‖γ t - s‖.