Primitives from vanishing contour integrals, and logarithms on sets without holes

A continuous function f on an open set U ⊆ ℂ whose contour integral ∫ t in a..b, deriv γ t • f (γ t) vanishes along every closed piecewise-C¹ curve γ in U has a primitive on U (Complex.IsExactOn f U): fix a base point in each path component of U, and integrate f from it along any piecewise-C¹ curve in U. The vanishing of closed integrals makes the value independent of the curve, and near each point the primitive differs from the integral along a segment by a constant, whose derivative Mathlib computes (HasFDerivAt.curveIntegral_segment_source').

By the homology form of Cauchy's theorem, the hypothesis holds for every holomorphic f as soon as every closed curve in U is null-homologous in U, and that is the case when U has no holes: when every connected component of ℂ \ U is unbounded (filledHull U ⊆ U), the condition that the complement of U in the Riemann sphere is connected. On such a set every holomorphic function has a primitive, so every nowhere-zero holomorphic function g has a holomorphic logarithm — a primitive of g' / g, corrected by a locally constant function — and holomorphic n-th roots. These are the implications (d) ⇒ (c) ⇒ (f) ⇒ (g) ⇒ (h) ⇒ (i) of Rudin's characterisation of simply connected plane domains, the step (c) ⇒ (f) being the homology form of Cauchy's theorem: a set without holes has holomorphic square roots.

Main results

• TauCeti.Contour.intervalIntegral_deriv_smul_eq_of_forall_closed_integral_eq_zero — if the contour integrals of f along closed curves in U vanish, its contour integral along a curve in U depends only on the endpoints.
• TauCeti.Contour.intervalIntegral_deriv_smul_segment_eq_curveIntegral — the contour integral along an affinely parametrized segment is Mathlib's curve integral along Path.segment.
• TauCeti.Contour.isExactOn_of_forall_closed_integral_eq_zero — the converse of Cauchy's theorem: such an f has a primitive on U.
• TauCeti.Contour.isExactOn_of_forall_isNullHomologous — a holomorphic function has a primitive on an open set in which every closed curve is null-homologous.
• TauCeti.Contour.isExactOn_of_filledHull_subset — a holomorphic function has a primitive on an open set without holes.
• TauCeti.Contour.exists_differentiableOn_eqOn_exp_comp_of_isExactOn — a nowhere-zero holomorphic function whose logarithmic derivative has a primitive has a holomorphic logarithm.
• TauCeti.Contour.exists_differentiableOn_eqOn_exp_comp_of_filledHull_subset, TauCeti.Contour.exists_differentiableOn_pow_eq_of_filledHull_subset — holomorphic logarithms and n-th roots on an open set without holes.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., Theorem 13.11 ((d) ⇒ (c) ⇒ (f) ⇒ (g) ⇒ (h) ⇒ (i)).
• L. Ahlfors, Complex Analysis, 3rd ed., Ch. 4, Section 1.3, Theorem 1.

theorem TauCeti.Contour.intervalIntegral_deriv_smul_eq_of_forall_closed_integral_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {f : ℂ → E} (hf : ContinuousOn f U) (h : ∀ (γ : ℝ → ℂ) (a b : ℝ), IsPiecewiseC1On γ a b → Set.MapsTo γ (Set.uIcc a b) U → γ a = γ b → ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0) {γ δ : ℝ → ℂ} {a b c d : ℝ} (hγ : IsPiecewiseC1On γ a b) (hδ : IsPiecewiseC1On δ c d) (hab : a ≤ b) (hcd : c ≤ d) (hγU : Set.MapsTo γ (Set.uIcc a b) U) (hδU : Set.MapsTo δ (Set.uIcc c d) U) (hstart : γ a = δ c) (hend : γ b = δ d) : ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = ∫ (t : ℝ) in c..d, deriv δ t • f (δ t)

Path independence. If the contour integral of a continuous f vanishes along every closed piecewise-C¹ curve in U, then its contour integrals along two piecewise-C¹ curves in U with the same endpoints agree.

theorem TauCeti.Contour.intervalIntegral_deriv_smul_segment_eq_curveIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) (s : ℝ) : ∫ (t : ℝ) in s..s + 1, deriv (fun (t : ℝ) => (t - s) • (w - z) + z) t • f ((t - s) • (w - z) + z) = ∫ᶜ (x : ℂ) in Path.segment z w, ContinuousLinearMap.toSpanSingleton ℂ (f x)

Segments as contour integrals. The contour integral along the segment from z to w, parametrized affinely on [s, s + 1], is Mathlib's curve integral of the 1-form v ↦ v • f x along Path.segment z w.

theorem TauCeti.Contour.isExactOn_of_forall_closed_integral_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {f : ℂ → E} [CompleteSpace E] (hU : IsOpen U) (hf : ContinuousOn f U) (h : ∀ (γ : ℝ → ℂ) (a b : ℝ), IsPiecewiseC1On γ a b → Set.MapsTo γ (Set.uIcc a b) U → γ a = γ b → ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0) : Complex.IsExactOn f U

The converse of Cauchy's theorem. A continuous function on an open set U whose contour integral vanishes along every closed piecewise-C¹ curve in U has a primitive on U.

theorem TauCeti.Contour.isExactOn_of_forall_isNullHomologous {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (h : ∀ (γ : ℝ → ℂ) (a b : ℝ), IsPiecewiseC1On γ a b → Set.MapsTo γ (Set.uIcc a b) U → γ a = γ b → IsNullHomologous γ a b U) : Complex.IsExactOn f U

Holomorphic functions have primitives where closed curves are null-homologous. If every closed piecewise-C¹ curve in the open set U is null-homologous in U, then every function holomorphic on U has a primitive on U.

theorem TauCeti.Contour.isExactOn_of_filledHull_subset {U : Set ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hUf : filledHull U ⊆ U) (hf : DifferentiableOn ℂ f U) : Complex.IsExactOn f U

Holomorphic functions have primitives on a set without holes. If U is open and every connected component of ℂ \ U is unbounded (filledHull U ⊆ U), then every function holomorphic on U has a primitive on U.

theorem TauCeti.Contour.exists_differentiableOn_eqOn_exp_comp_of_isExactOn {U : Set ℂ} {g : ℂ → ℂ} (hU : IsOpen U) (hg : DifferentiableOn ℂ g U) (hg₀ : 0 ∉ g '' U) (hex : Complex.IsExactOn (logDeriv g) U) : ∃ (L : ℂ → ℂ), DifferentiableOn ℂ L U ∧ Set.EqOn (Complex.exp ∘ L) g U

A holomorphic logarithm from a primitive of the logarithmic derivative. If g is holomorphic and nowhere zero on an open set U and g' / g has a primitive h on U, then g has a holomorphic logarithm on U.

theorem TauCeti.Contour.exists_differentiableOn_eqOn_exp_comp_of_filledHull_subset {U : Set ℂ} {g : ℂ → ℂ} (hU : IsOpen U) (hUf : filledHull U ⊆ U) (hg : DifferentiableOn ℂ g U) (hg₀ : 0 ∉ g '' U) : ∃ (L : ℂ → ℂ), DifferentiableOn ℂ L U ∧ Set.EqOn (Complex.exp ∘ L) g U

Holomorphic logarithms on a set without holes. If U is open and every connected component of ℂ \ U is unbounded (filledHull U ⊆ U), then every function holomorphic and nowhere zero on U has a holomorphic logarithm on U.

theorem TauCeti.Contour.exists_differentiableOn_pow_eq_of_filledHull_subset {U : Set ℂ} {g : ℂ → ℂ} (hU : IsOpen U) (hUf : filledHull U ⊆ U) (hg : DifferentiableOn ℂ g U) (hg₀ : 0 ∉ g '' U) {n : ℕ} (hn : n ≠ 0) : ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f U ∧ Set.EqOn (fun (z : ℂ) => f z ^ n) g U

Holomorphic n-th roots on a set without holes. If U is open and every connected component of ℂ \ U is unbounded (filledHull U ⊆ U), then every function holomorphic and nowhere zero on U has a holomorphic n-th root on U, namely exp (L / n) for a holomorphic logarithm L.