Dixon's Proof of the Homological Cauchy Theorem

The Dixon kernel g(z, w) = (f(z) - f(w))/(z - w) (extended to f'(w) at z = w) is exactly mathlib's dslope f z w. We use this identification throughout.

Main definitions

• dixonKernel -- the Dixon kernel (= dslope)
• dixonH1 -- the Dixon integral h₁(w)
• dixonH2 -- the Cauchy-type integral h₂(w)
• dixonFunction -- the piecewise Dixon function

Main results

• dixonH1_eq -- key identity: h₁(w) = h₂(w) - 2πi · n(γ,w) · f(w)
• dixonH1_differentiableOn -- h₁ is differentiable on U
• dixonH2_differentiableAt -- h₂ is differentiable off the curve
• dixonFunction_differentiable -- the Dixon function is entire
• dixonFunction_eq_zero -- h ≡ 0 by Liouville's theorem
• cauchyIntegralFormula_nullHomologous -- Cauchy integral formula
• contourIntegral_eq_zero_of_nullHomologous -- vanishing for holomorphic functions

@[reducible, inline]

noncomputable abbrev dixonKernel (f : ℂ → ℂ) (z w : ℂ) : ℂ

The Dixon kernel is exactly dslope: dixonKernel f z w = dslope f z w. We use dslope directly rather than a custom definition.

Equations

• dixonKernel f z w = dslope f z w

noncomputable def dixonH1 (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) (w : ℂ) : ℂ

h₁(w) = ∮_γ dslope(f, γ(t), w) · γ'(t) dt — the Dixon integral. Holomorphic on all of U including image(γ).

Equations

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

noncomputable def dixonH2 (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) (w : ℂ) : ℂ

h₂(w) = ∮_γ f(z)/(z-w) · γ'(t) dt — the Cauchy-type integral. Holomorphic on ℂ \ image(γ).

Equations

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

theorem dixonH1_eq {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (γ : PiecewiseC1Immersion) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) (w : ℂ) (hoff : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ w) : dixonH1 f γ w = dixonH2 f γ w - 2 * ↑Real.pi * Complex.I * generalizedWindingNumber' γ.toFun γ.a γ.b w * f w

Key identity: h₁(w) = h₂(w) - 2πi · n(γ,w) · f(w) for w off the curve. This follows from expanding dslope and splitting the integral.

theorem dixonH2_differentiableAt (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) (hf_cont : ContinuousOn f (γ.toFun '' Set.Icc γ.a γ.b)) (w : ℂ) (hoff : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ w) : DifferentiableAt ℂ (dixonH2 f γ) w

h₂ is differentiable at every point off the curve, when f is continuous on the image.

theorem dixonH1_differentiableOn {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (γ : PiecewiseC1Immersion) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) : DifferentiableOn ℂ (dixonH1 f γ) U

h₁ is differentiable on all of U, including across the curve. Uses the Leibniz rule (parametric differentiation of the dslope integral).

noncomputable def dixonFunction (f : ℂ → ℂ) (U : Set ℂ) (γ : PiecewiseC1Immersion) (w : ℂ) : ℂ

The Dixon function: h1 on U, h2 on C \ U.

Equations

• dixonFunction f U γ w = if _h : w ∈ U then dixonH1 f γ w else dixonH2 f γ w

theorem dixonFunction_differentiable {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) : Differentiable ℂ (dixonFunction f U γ)

The Dixon function is entire (differentiable on all of ℂ). On U: it's h₁, holomorphic by dixonH1_differentiableOn. On ℂ \ U: it's h₂, holomorphic by dixonH2_differentiableAt. Patching at ∂U: null-homologous gives n(γ,w) = 0 near ∂U, so h₁ = h₂ there.

theorem dixonFunction_tendsto_zero {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) : Filter.Tendsto (dixonFunction f U γ) (Filter.cocompact ℂ) (nhds 0)

theorem dixonFunction_eq_zero {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (w : ℂ) : dixonFunction f U γ w = 0

h ≡ 0 by Liouville's theorem.

theorem cauchyIntegralFormula_nullHomologous {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (w : ℂ) (hw : w ∈ U) (hoff : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ w) : dixonH2 f γ w = 2 * ↑Real.pi * Complex.I * generalizedWindingNumber' γ.toFun γ.a γ.b w * f w

Cauchy integral formula for null-homologous curves: ∮_γ f(z)/(z-w) dz = 2πi · n(γ,w) · f(w) for w ∈ U off the curve.

theorem piecewiseC1_image_interior_empty (γ : PiecewiseC1Immersion) : interior (γ.toFun '' Set.Icc γ.a γ.b) = ∅

The image of a piecewise C¹ immersion has empty interior in ℂ. This follows from the fact that a Lipschitz map from ℝ to ℂ has image with Hausdorff dimension at most 1, hence Lebesgue measure 0 in ℂ.

theorem contourIntegral_eq_zero_of_nullHomologous {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) : ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t = 0