Holomorphy of Dixon's h₂ off the curve

Dixon's h₂ integral dixonH2 f γ a b w = ∫ t in a..b, f (γ t) / (γ t - w) * deriv γ t is holomorphic in the point w, at every w off the curve. This is the Cauchy-type half of the analyticity of Dixon's glued function.

Main results

• TauCeti.Contour.differentiableAt_dixonH2 — fun w ↦ dixonH2 f γ a b w is complex-differentiable at every point off the curve, given continuity of γ and interval-integrability of the Cauchy integrand f (γ ·) / (γ · - w) · deriv γ.

This feeds the homologyCauchyTheorem roadmap target (TauCetiRoadmap/ContourIntegration/Suggested.lean, Layer 3, Dixon's argument).

Provenance

Adapted from dixonH2_differentiableAt / dixonH2_differentiableAt_of_regular in DixonDiff.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on an oriented interval and phrased with the integrable Cauchy integrand (weaker than a continuous f and a separately integrable derivative). See J. D. Dixon, A brief proof of Cauchy's integral theorem (1971).

theorem TauCeti.Contour.differentiableAt_dixonH2 {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (h_cauchy_int : IntervalIntegrable (fun (t : ℝ) => f (γ t) / (γ t - w) * deriv γ t) MeasureTheory.volume a b) : DifferentiableAt ℂ (dixonH2 f γ a b) w

dixonH2 is holomorphic in the point, off the curve. If γ is continuous on uIcc a b and avoids w there, and the Cauchy integrand f (γ ·) / (γ · - w) · deriv γ is interval-integrable, then fun w ↦ dixonH2 f γ a b w is complex-differentiable at w.