Dixon's h₁ and h₂ functions and their defining identity

Dixon's proof of the homology form of Cauchy's theorem hinges on a single auxiliary function that is analytic on all of ℂ. This file records its two constituent integrals and the algebraic identity relating them; the analyticity, boundedness, and Liouville steps are developed downstream.

For a curve γ : ℝ → ℂ on the oriented interval with endpoints a, b and a function f:

• dixonH1 f γ a b w = ∫ t in a..b, dslope f w (γ t) * deriv γ t — built from the difference quotient dslope f w z, which equals (f z - f w) / (z - w) for z ≠ w and deriv f w at z = w, so the integrand is defined for every w, including points on γ.
• dixonH2 f γ a b w = ∫ t in a..b, f (γ t) / (γ t - w) * deriv γ t — the Cauchy-type integral, defined for w off the curve.
• dixonFunction f U γ a b w — selects dixonH1 on U and dixonH2 on its complement.

Each definition is irreducible_def, exposing a public *_def equation lemma while keeping the body opaque.

Main results

• TauCeti.Contour.dixonH1_eq_dixonH2_sub_windingNumber_mul_f — for γ continuous on uIcc a b and w off the curve, with the index and Cauchy-type integrands interval-integrable, dixonH1 f γ a b w = dixonH2 f γ a b w - 2πi · n(γ, w) · f w, where n(γ, w) is the generalized windingNumber. This is what makes dixonFunction well-glued across ∂U.

These are the building blocks of the homologyCauchyTheorem roadmap target (TauCetiRoadmap/ContourIntegration/Suggested.lean, Layer 3, proved by Dixon's argument).

Provenance

Adapted from dixonH1, dixonH2, dixonFunction, and dixonH1_eq_dixonH2_sub_winding_f in DixonDef.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on an oriented interval with endpoints a and b. See J. D. Dixon, A brief proof of Cauchy's integral theorem, Proc. Amer. Math. Soc. 29 (1971), and N. Hungerbühler, M. Wasem, A generalized notion of winding numbers.

theorem TauCeti.Contour.dixonH1_def (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (w : ℂ) : dixonH1 f γ a b w = ∫ (t : ℝ) in a..b, dslope f w (γ t) * deriv γ t

@[irreducible]

noncomputable def TauCeti.Contour.dixonH1 (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (w : ℂ) : ℂ

Dixon's h₁ integral ∫ t in a..b, dslope f w (γ t) * deriv γ t. The difference quotient dslope f w z equals (f z - f w) / (z - w) for z ≠ w and deriv f w at z = w, so the integrand is defined for every w, including points on the curve γ.

Equations

• TauCeti.Contour.dixonH1 f γ a b w = ∫ (t : ℝ) in a..b, dslope f w (γ t) * deriv γ t

theorem TauCeti.Contour.dixonH2_def (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (w : ℂ) : dixonH2 f γ a b w = ∫ (t : ℝ) in a..b, f (γ t) / (γ t - w) * deriv γ t

@[irreducible]

noncomputable def TauCeti.Contour.dixonH2 (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (w : ℂ) : ℂ

Dixon's h₂ integral ∫ t in a..b, f (γ t) / (γ t - w) * deriv γ t, the ordinary Cauchy-type integral, defined for w off the curve.

Equations

• TauCeti.Contour.dixonH2 f γ a b w = ∫ (t : ℝ) in a..b, f (γ t) / (γ t - w) * deriv γ t

@[irreducible]

noncomputable def TauCeti.Contour.dixonFunction (f : ℂ → ℂ) (U : Set ℂ) (γ : ℝ → ℂ) (a b : ℝ) (w : ℂ) : ℂ

Dixon's glued function: dixonH1 on U, dixonH2 on its complement. That these two pieces glue, under null-homology, into a function analytic on all of ℂ is the downstream content of Dixon's argument, established in later results; here the function is only defined.

Equations

• TauCeti.Contour.dixonFunction f U γ a b w = if w ∈ U then TauCeti.Contour.dixonH1 f γ a b w else TauCeti.Contour.dixonH2 f γ a b w

theorem TauCeti.Contour.dixonFunction_def (f : ℂ → ℂ) (U : Set ℂ) (γ : ℝ → ℂ) (a b : ℝ) (w : ℂ) : dixonFunction f U γ a b w = if w ∈ U then dixonH1 f γ a b w else dixonH2 f γ a b w

theorem TauCeti.Contour.dixonH1_eq_dixonH2_sub_windingNumber_mul_f {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) (h_base_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) : dixonH1 f γ a b w = dixonH2 f γ a b w - 2 * ↑Real.pi * Complex.I * windingNumber γ a b w * f w

The h₁/h₂ identity. For γ continuous on uIcc a b and w off the curve, with the index and Cauchy-type integrands interval-integrable, dixonH1 f γ a b w differs from dixonH2 f γ a b w by exactly 2πi · n(γ, w) · f w, the generalized winding number of γ about w scaled by f w.

@[simp]

theorem TauCeti.Contour.dixonFunction_eq_dixonH1 {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (hw : w ∈ U) : dixonFunction f U γ a b w = dixonH1 f γ a b w

On U, the glued Dixon function is dixonH1.

@[simp]

theorem TauCeti.Contour.dixonFunction_eq_dixonH2 {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (hw : w ∉ U) : dixonFunction f U γ a b w = dixonH2 f γ a b w

Off U, the glued Dixon function is dixonH2.