Holomorphic primitives on the upper half-plane

Every holomorphic function on the upper half-plane has a global primitive. This file gives an explicit one: Complex.wedgeIntegral b z f, the integral along the horizontal-then-vertical polygonal path from a chosen base point b to z.

The central input is path independence for these wedge paths. Three such paths bound a rectangle, and that rectangle stays in the upper half-plane. Cauchy's theorem for rectangles therefore makes the wedge integrals additive. Locally, the explicit primitive agrees up to a constant with Mathlib's primitive on a ball, so it has derivative f throughout the half-plane.

Main results

• Complex.IsConservativeOn.wedgeIntegral_sub_wedgeIntegral_eq_of_mem_upperHalfPlane -- wedge integrals based at an upper-half-plane point are additive.
• DifferentiableOn.hasDerivAt_wedgeIntegral_upperHalfPlane -- the explicit wedge integral has derivative equal to its integrand.

theorem TauCeti.exists_hasDerivAt_eqOn_ball_inter_upperHalfPlane {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f g : ℂ → E} {c : ℂ} {r : ℝ} (hg : DifferentiableOn ℂ g (Metric.ball c r)) (hf : ∀ z ∈ Metric.ball c r ∩ UpperHalfPlane.upperHalfPlaneSet, HasDerivAt f (g z) z) : ∃ (G : ℂ → E), (∀ z ∈ Metric.ball c r, HasDerivAt G (g z) z) ∧ Set.EqOn G f (Metric.ball c r ∩ UpperHalfPlane.upperHalfPlaneSet)

A holomorphic integrand on a ball has a primitive agreeing with any given primitive on the intersection of that ball with the upper half-plane.

theorem Complex.IsConservativeOn.wedgeIntegral_sub_wedgeIntegral_eq_of_mem_upperHalfPlane {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hf : IsConservativeOn f UpperHalfPlane.upperHalfPlaneSet) (hcont : ContinuousOn f UpperHalfPlane.upperHalfPlaneSet) {b z w : ℂ} (hb : b ∈ UpperHalfPlane.upperHalfPlaneSet) (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) (hw : w ∈ UpperHalfPlane.upperHalfPlaneSet) : b.wedgeIntegral w f - b.wedgeIntegral z f = z.wedgeIntegral w f

Wedge integrals based at a point of the upper half-plane are additive along any intermediate point there. Equivalently, the integral around the rectangle left between the three wedge paths vanishes.

theorem DifferentiableOn.hasDerivAt_wedgeIntegral_upperHalfPlane {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (b : UpperHalfPlane) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : HasDerivAt (fun (w : ℂ) => (↑b).wedgeIntegral w f) (f z) z

The wedge integral of a holomorphic function from an upper-half-plane base point has derivative equal to the function at every point of the upper half-plane.