Conjugation symmetry of normalized holomorphic primitives #
A holomorphic function on a connected conjugation-symmetric open set whose derivative commutes with conjugation has conjugation-symmetric increments; in particular it commutes with conjugation after subtracting its value at a real base point. This transfers symmetry of a regularized integrand to its primitive.
References #
- L. Ahlfors, Complex Analysis, Chapter 4, Section 3.
theorem
TauCeti.sub_conj_eq_conj_sub_of_deriv_conj
{f : ℂ → ℂ}
{Ω : Set ℂ}
(hΩopen : IsOpen Ω)
(hΩconn : IsPreconnected Ω)
(hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω)
(hf : DifferentiableOn ℂ f Ω)
(hderiv : ∀ z ∈ Ω, deriv f ((starRingEnd ℂ) z) = (starRingEnd ℂ) (deriv f z))
{w z : ℂ}
(hw : w ∈ Ω)
(hz : z ∈ Ω)
:
A holomorphic primitive of a conjugation-symmetric derivative on a connected domain has
conjugation-symmetric increments: f (conj z) - f (conj w) = conj (f z - f w). At a real base
point w = p, this says that f - f p commutes with conjugation.