The Dixon function vanishes (Liouville step)

Dixon's glued function dixonFunction f U γ a b is entire (differentiable_dixonFunction) and, for a closed null-homologous curve, tends to 0 at infinity, so Liouville's theorem forces it to vanish identically. The decay comes from the eventual agreement dixonFunction = dixonH2 far from the origin — off U by definition, and on U because the winding number is eventually 0, which collapses the h₁/h₂ identity — combined with the L¹ decay of dixonH2.

Main results

• TauCeti.Contour.dixonFunction_eq_zero — dixonFunction f U γ a b w = 0 for every w, for a closed null-homologous curve in U with f differentiable on the open set U.

This pointwise vanishing is the hinge of Dixon's proof of the homology form of Cauchy's theorem (homologyCauchyTheorem, TauCetiRoadmap/ContourIntegration/Suggested.lean): applying it to (· - w₀) * f yields the Cauchy integral formula and thence ∮_γ f = 0.

Provenance

Adapted from dixonFunction_eventually_eq_dixonH2, dixonFunction_tendsto_zero and dixonFunction_eq_zero in DixonTheorem.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on an oriented interval. See J. D. Dixon, A brief proof of Cauchy's integral theorem (1971).

theorem TauCeti.Contour.dixonFunction_eq_zero {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ} {P : Set ℝ} (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) (hclosed : γ a = γ b) (hP : P.Countable) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (h_null : IsNullHomologous γ a b U) (w : ℂ) : dixonFunction f U γ a b w = 0

The Dixon function is identically zero (Liouville). For a closed curve γ, null-homologous in an open set U (continuous on uIcc a b, differentiable off a countable set, with interval-integrable derivative and image in U) and f differentiable on U, the entire function dixonFunction f U γ a b tends to 0 at infinity, so Liouville's theorem forces it to vanish at every point.