Holomorphy of Dixon's h₁ on the region

Dixon's h₁ integral dixonH1 f γ a b w = ∫ t in a..b, dslope f w (γ t) * deriv γ t is holomorphic in the point w, throughout the open region U where f is holomorphic and the curve γ lives. This is the removable-singularity half of the analyticity of Dixon's glued function: because dslope f · (γ t) extends f's divided difference across the diagonal, the integrand stays holomorphic even for w on the curve.

Main results

• TauCeti.Contour.differentiableOn_dixonH1 — fun w ↦ dixonH1 f γ a b w is complex-differentiable on U, for f differentiable on the open set U and γ continuous on uIcc a b with interval-integrable derivative and image in U.

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

Provenance

Adapted from dixonH1_differentiableOn / dixonH1_differentiableOn_of_regular_open_full in DixonDiff.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on an oriented interval with the curve's derivative required only to be interval-integrable. See J. D. Dixon, A brief proof of Cauchy's integral theorem (1971).

theorem TauCeti.Contour.differentiableOn_dixonH1 {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) : DifferentiableOn ℂ (dixonH1 f γ a b) U

dixonH1 is holomorphic on the region. For f differentiable on the open set U, and γ continuous on uIcc a b with deriv γ interval-integrable and image in U, the map fun w ↦ dixonH1 f γ a b w is complex-differentiable on U.