Integrating g z / z through a primitive of dslope g 0

Let g be holomorphic near 0. Off 0, the integrand g z / z splits as dslope g 0 z + g 0 / z: the removable-singularity quotient dslope g 0 is holomorphic wherever g is (Mathlib's Complex.differentiableOn_dslope), and the polar part g 0 / z carries the whole singularity. So along a path γ avoiding 0, a primitive H of dslope g 0 evaluates the first part as an endpoint difference, and the integral of g z / z reduces to g 0 times the integral of dz / z.

Along an arc of circleMap 0 R the integral of dz / z is elementary, the integrand being constantly i, so the integral of g z / z over the arc on [a, b] is H (circleMap 0 R b) - H (circleMap 0 R a) + (b - a) i g 0.

Main results

• TauCeti.Contour.integral_mul_div_eq_of_hasDerivAt_dslope — along a path γ avoiding 0, the integral of g z / z is H (γ b) - H (γ a) + g 0 ∫ dz / z.
• TauCeti.Contour.integral_circleMap_mul_div_eq_of_hasDerivAt_dslope — its specialization to an arc of circleMap 0 R.

theorem TauCeti.Contour.integral_mul_div_eq_of_hasDerivAt_dslope {U : Set ℂ} {g H : ℂ → ℂ} {a b : ℝ} {γ γ' : ℝ → ℂ} (hU : U ∈ nhds 0) (hg : DifferentiableOn ℂ g U) (hH : ∀ z ∈ U, HasDerivAt H (dslope g 0 z) z) (hγ : ∀ s ∈ Set.uIcc a b, HasDerivAt γ (γ' s) s) (hγ' : ContinuousOn γ' (Set.uIcc a b)) (hγU : ∀ s ∈ Set.uIcc a b, γ s ∈ U) (hγ0 : ∀ s ∈ Set.uIcc a b, γ s ≠ 0) : ∫ (s : ℝ) in a..b, γ' s * (g (γ s) / γ s) = H (γ b) - H (γ a) + g 0 * ∫ (s : ℝ) in a..b, γ' s / γ s

The integral of g z / z through a primitive of dslope g 0. Let g be holomorphic on a neighbourhood U of 0 and H a primitive of dslope g 0 on U. Along a path γ in U avoiding 0, with continuous velocity γ', the integral of g z / z is the endpoint difference of H plus g 0 times the integral of dz / z.

theorem TauCeti.Contour.integral_circleMap_mul_div_eq_of_hasDerivAt_dslope {U : Set ℂ} {g H : ℂ → ℂ} {a b R : ℝ} (hR : R ≠ 0) (hU : U ∈ nhds 0) (hg : DifferentiableOn ℂ g U) (hH : ∀ z ∈ U, HasDerivAt H (dslope g 0 z) z) (hcirc : ∀ θ ∈ Set.uIcc a b, circleMap 0 R θ ∈ U) : ∫ (θ : ℝ) in a..b, circleMap 0 R θ * Complex.I * (g (circleMap 0 R θ) / circleMap 0 R θ) = H (circleMap 0 R b) - H (circleMap 0 R a) + g 0 * ((↑b - ↑a) * Complex.I)

The integral of g z / z over an arc of a circle about 0. Let g be holomorphic on a neighbourhood U of 0 and H a primitive of dslope g 0 on U. If R ≠ 0 and the arc of circleMap 0 R on [a, b] lies in U, then the integral of g z / z over the arc, with the velocity circleMap 0 R θ * I of the parametrization, is H (circleMap 0 R b) - H (circleMap 0 R a) + (b - a) i g 0.