The excised boundary integrand is integrable

intervalIntegral_excised_logDeriv_fdBoundary assembles the excised boundary integral from integrability assumed on [0, 1], [1, 2] and [4, 5]. This file discharges that assumption, for any subinterval of [0, 5] at once.

Both inputs the general criterion needs are available for the boundary contour: it is piecewise C¹ (isPiecewiseC1On_fdBoundary), which makes its derivative interval-integrable, and off the excision the form is analytic and nonvanishing at the contour points themselves, so its logarithmic derivative is analytic there (analyticAt_logDeriv_of_analyticAt) and in particular continuous.

The analyticity hypothesis is stated along the contour rather than on an open set containing the fundamental domain, because that is all the proof uses. Keeping it contour-local is what lets the excision set here stay separate from the divisor set of the argument principle.

Main results

• TauCeti.ModularForm.intervalIntegrable_excised_deriv_smul_logDeriv_comp_ofComplex_fdBoundary: the excised boundary integrand is interval-integrable on any subinterval of [0, 5].

theorem TauCeti.ModularForm.intervalIntegrable_excised_deriv_smul_logDeriv_comp_ofComplex_fdBoundary {g : ℂ → ℂ} {H ε : ℝ} (hε : 0 < ε) {S : Finset ℂ} {a b : ℝ} (hab : Set.uIcc a b ⊆ Set.Icc 0 5) (hoff : ∀ t ∈ Set.uIcc a b, fdBoundary H t ∉ S → AnalyticAt ℂ g (fdBoundary H t) ∧ g (fdBoundary H t) ≠ 0) : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv g (fdBoundary H t)) MeasureTheory.volume a b

The excised boundary integrand is integrable. Off the excision the form is analytic and nonvanishing at the contour points, so its logarithmic derivative is continuous there; the contour is piecewise C¹, so its derivative is interval-integrable, and TauCeti.Contour's criterion applies.

hε is needed to know that a point at distance ≥ ε from every centre is not itself a centre.