Primitives of Holomorphic Functions

In this file, we give conditions under which holomorphic functions have primitives. The main goal is to prove that holomorphic functions on simply connected domains have primitives. As a first step, we prove that holomorphic functions on disks have primitives. The approach is based on Morera's theorem, that a continuous function (on a disk) whose integral round a rectangle vanishes on all rectangles contained in the disk has a primitive. (Coupled with the fact that holomorphic functions satisfy this property.) To prove Morera's theorem, we first define the Complex.wedgeIntegral, which is the integral of a function over a "wedge" (a horizontal segment followed by a vertical segment in the disk), and compute its derivative.

Main results

• Complex.IsConservativeOn.isExactOn_ball: Morera's Theorem: On a disk, a continuous function whose integrals on rectangles vanish, has primitives.
• DifferentiableOn.isExactOn_ball: On a disk, a holomorphic function has primitives.

TODO: Extend to holomorphic functions on simply connected domains.

noncomputable def Complex.wedgeIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (z w : ℂ) (f : ℂ → E) : E

The (z, w)-wedge-integral of f, is the integral of f over two sides of the rectangle determined by z and w.

theorem Complex.wedgeIntegral_add_wedgeIntegral_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (z w : ℂ) (f : ℂ → E) : z.wedgeIntegral w f + w.wedgeIntegral z f = (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)

def Complex.IsConservativeOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (U : Set ℂ) : Prop

A function f IsConservativeOn in U if, for any rectangle contained in U the integral of f over the rectangle is zero.

def Complex.IsExactOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (U : Set ℂ) : Prop

A function f IsExactOn in U if it is the complex derivative of a function on U.

In complex variable theory, this is also referred to as "having a primitive".

theorem Complex.IsExactOn.with_val_at {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {s : Set ℂ} (h : IsExactOn f s) (x₀ : ℂ) (y : E) : ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x

theorem Complex.IsConservativeOn.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {U V : Set ℂ} (h : U ⊆ V) (hf : IsConservativeOn f V) : IsConservativeOn f U

theorem DifferentiableOn.isConservativeOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) : Complex.IsConservativeOn f U

theorem Complex.IsExactOn.differentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {U : Set ℂ} (hU : IsOpen U) (hf : IsExactOn f U) : DifferentiableOn ℂ f U

theorem Complex.IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} (f_cont : ContinuousOn f (Metric.ball c r)) {z : ℂ} (hz : z ∈ Metric.ball c r) (hf : IsConservativeOn f (Metric.ball c r)) : ∀ᶠ (w : ℂ) in nhds z, c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

If a function f IsConservativeOn on a disk of center c, then for points z in this disk, the wedge integral from c to z is additive under a detour through a nearby point w.

theorem Complex.IsConservativeOn.hasDerivAt_wedgeIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E] (f_cont : ContinuousOn f (Metric.ball c r)) {z : ℂ} (hz : z ∈ Metric.ball c r) (h : IsConservativeOn f (Metric.ball c r)) : HasDerivAt (fun (w : ℂ) => c.wedgeIntegral w f) (f z) z

The wedgeIntegral has derivative at z equal to f z.

theorem Complex.IsConservativeOn.isExactOn_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E] (hf' : ContinuousOn f (Metric.ball c r)) (hf : IsConservativeOn f (Metric.ball c r)) : IsExactOn f (Metric.ball c r)

Morera's theorem for a disk On a disk, a continuous function whose integrals on rectangles vanish, has primitives.

theorem Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {U : Set ℂ} (hU : IsOpen U) : IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U

theorem DifferentiableOn.isExactOn_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E] (hf : DifferentiableOn ℂ f (Metric.ball c r)) : Complex.IsExactOn f (Metric.ball c r)

Morera's theorem for a disk On a disk, a holomorphic function has primitives.

theorem Complex.IsConservativeOn.isExactOn_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] (h₁ : Continuous f) (h₂ : IsConservativeOn f Set.univ) : IsExactOn f Set.univ

Morera's theorem for the complex plane A continuous function on ℂ whose integrals on rectangles vanish, has primitives.

theorem Differentiable.isExactOn_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] (hf : Differentiable ℂ f) : Complex.IsExactOn f Set.univ

Morera's theorem for the complex plane A holomorphic function on ℂ has primitives.