The Cauchy–Pompeiu formula

The Cauchy kernel 1 / (π z) is a fundamental solution of the Cauchy–Riemann operator \bar∂ = (∂ₓ + i ∂ᵧ) / 2 on ℂ. Writing the operator as D u = ∂ₓ u + i ∂ᵧ u = 2 \bar∂ u, that is fun z ↦ fderiv ℝ u z 1 + I • fderiv ℝ u z I, this file proves both halves of that statement for compactly supported C¹ maps u : ℂ → F into a complex Banach space.

• The Cauchy–Pompeiu formula: every such u is the Cauchy transform of D u, u w = (2π)⁻¹ ∫ (w - z)⁻¹ • D u z, the integral being over the whole plane. This is the Cauchy–Pompeiu formula on a disc containing the support of u, whose boundary term (the Cauchy integral of u over the boundary circle) vanishes.
• The Cauchy transform w ↦ (2π)⁻¹ ∫ (w - z)⁻¹ • f z of a compactly supported C¹ map f is differentiable, its derivative is the Cauchy transform of the derivative of f, and D of it is f. With the conjugate Wirtinger derivative, \bar∂_w ∫ (w - z)⁻¹ • f z = π f w, so the transform is complex differentiable at every point where f vanishes, and holomorphic off the support of f.

So the Cauchy transform inverts D = 2 \bar∂ on both sides on compactly supported C¹ maps. This representation is the starting point of the elliptic estimates for the Cauchy–Riemann operator: differentiating it expresses ∂ u through \bar∂ u by the Beurling transform, a singular integral operator, and the Calderón–Zygmund inequality ‖∇u‖_{Lᵖ} ≤ C ‖\bar∂ u‖_{Lᵖ} for compactly supported u is the Lᵖ boundedness of that operator.

The proof of the formula passes to polar coordinates z = w + r e^{iθ} about w. There the integrand (z - w)⁻¹ • D u z dz becomes ∂ᵣ v + i r⁻¹ ∂_θ v for v (r, θ) = u (w + r e^{iθ}). The angular term integrates to zero over each circle, and the radial term integrates to -u w along each ray.

The normalized TauCeti.cauchyTransform f w = π⁻¹ ∫ z, (w - z)⁻¹ • f z inverts bar∂ itself. Its basic integral and convolution formulas, almost-everywhere congruence, and compact-support left and right inverse identities are available in this module.

Main results

• TauCeti.cauchyTransform and TauCeti.cauchyTransform_apply: the normalized integral.
• HasCompactSupport.conjWirtingerDeriv_cauchyTransform and HasCompactSupport.cauchyTransform_conjWirtingerDeriv: normalized right and left inverses.
• HasCompactSupport.two_pi_inv_smul_integral_sub_inv_smul_fderiv_apply_one_add_I_smul_apply_I: the Cauchy–Pompeiu formula.
• HasCompactSupport.hasFDerivAt_integral_sub_inv_smul: the Cauchy transform of a compactly supported C¹ map is differentiable, with derivative the transform of the derivative.
• HasCompactSupport.fderiv_cauchyTransform and HasCompactSupport.fderiv_cauchyTransform_apply: the same commutation D (T f) = T (D f) for the normalized transform, also in directional form.
• TauCeti.cauchyTransform_add and TauCeti.cauchyTransform_smul: the normalized transform is additive on continuous compactly supported data and commutes with scalar multiplication.
• HasCompactSupport.fderiv_apply_one_add_I_smul_apply_I_two_pi_inv_smul_integral_sub_inv_smul: D = 2 \bar∂ of the Cauchy transform of a compactly supported C¹ map f is f.
• HasCompactSupport.conjWirtingerDeriv_integral_sub_inv_smul_apply_one: \bar∂ (∫ (w - z)⁻¹ • f z) = π f.
• HasCompactSupport.differentiableAt_integral_sub_inv_smul_of_eq_zero and TauCeti.differentiableOn_integral_sub_inv_smul_compl: holomorphy where f vanishes, in particular off tsupport f.
• HasCompactSupport.contDiff_cauchyTransform, HasCompactSupport.differentiableAt_cauchyTransform_of_notMem_tsupport and HasCompactSupport.tendsto_cauchyTransform_cobounded: the normalized transform of compactly supported smooth data is smooth and holomorphic off tsupport f, and that of compactly supported integrable data tends to 0 at infinity.

References

• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990, Theorem 1.2.1 and Theorem 1.2.2.
• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix B.2 (the Calderón–Zygmund inequality).

noncomputable def TauCeti.cauchyTransform {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (w : ℂ) : F

The planar Cauchy transform with the normalization inverting bar∂, using the kernel (w - z)⁻¹. For rough compactly supported Lᵖ data the integral exists almost everywhere.

theorem TauCeti.cauchyTransform_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (w : ℂ) : cauchyTransform f w = (↑Real.pi)⁻¹ • ∫ (z : ℂ), (w - z)⁻¹ • f z

The defining normalized integral of the Cauchy transform.

theorem TauCeti.cauchyTransform_eq_convolution {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) : cauchyTransform f = fun (w : ℂ) => (↑Real.pi)⁻¹ • MeasureTheory.convolution (fun (z : ℂ) => z⁻¹) f (ContinuousLinearMap.lsmul ℝ ℂ) MeasureTheory.volume w

In convolution coordinates the Cauchy transform uses the reciprocal kernel with the same positive sign. The variable substitution gives ξ⁻¹ • f (w - ξ).

theorem TauCeti.cauchyTransform_eq_integral_closedBall {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {c : ℂ} {r : NNReal} (hf : Function.support f ⊆ Metric.closedBall c ↑r) (w : ℂ) : cauchyTransform f w = (↑Real.pi)⁻¹ • ∫ (z : ℂ) in Metric.closedBall c ↑r, (w - z)⁻¹ • f z

A supported input may be integrated over its input disc in the Cauchy formula.

theorem TauCeti.norm_mul_norm_cauchyTransform_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {r : ℝ} (hf : Function.support f ⊆ Metric.closedBall 0 r) (hfi : MeasureTheory.Integrable f MeasureTheory.volume) {w : ℂ} (hw : 2 * r ≤ ‖w‖) : ‖w‖ * ‖cauchyTransform f w‖ ≤ 2 * Real.pi⁻¹ * ∫ (z : ℂ), ‖f z‖

Decay of the Cauchy transform. If f is integrable and supported in the disc of radius r about the origin, then ‖w‖ ‖T f w‖ ≤ 2 π⁻¹ ‖f‖_{L¹} for ‖w‖ ≥ 2 r.

theorem TauCeti.cauchyTransform_congr_ae {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f g : ℂ → F} (hfg : f =ᵐ[MeasureTheory.volume] g) : cauchyTransform f = cauchyTransform g

Almost-everywhere changes in the source leave the actual Cauchy integral unchanged.

@[simp]

theorem TauCeti.cauchyTransform_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] : cauchyTransform 0 = 0

theorem TauCeti.cauchyTransform_add {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f g : ℂ → F} (hf : Continuous f) (hfc : HasCompactSupport f) (hg : Continuous g) (hgc : HasCompactSupport g) : cauchyTransform (f + g) = cauchyTransform f + cauchyTransform g

The Cauchy transform is additive on continuous compactly supported data.

theorem TauCeti.cauchyTransform_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [SMulCommClass ℝ 𝕜 F] (a : 𝕜) (f : ℂ → F) : cauchyTransform (a • f) = a • cauchyTransform f

The Cauchy transform commutes with scalar multiplications that commute with the complex and real actions, in particular with real and complex scalars.

theorem HasCompactSupport.two_pi_inv_smul_integral_sub_inv_smul_fderiv_apply_one_add_I_smul_apply_I {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {u : ℂ → F} (hc : HasCompactSupport u) (hu : ContDiff ℝ 1 u) (w : ℂ) : (2 * ↑Real.pi)⁻¹ • ∫ (z : ℂ), (w - z)⁻¹ • ((fderiv ℝ u z) 1 + Complex.I • (fderiv ℝ u z) Complex.I) = u w

The Cauchy–Pompeiu formula for a compactly supported C¹ map u : ℂ → F: u is the Cauchy transform of ∂ₓ u + i ∂ᵧ u = 2 \bar∂ u, u w = (2π)⁻¹ ∫ (w - z)⁻¹ • (∂ₓ u z + i ∂ᵧ u z), the integral being over the whole plane.

theorem HasCompactSupport.hasFDerivAt_integral_sub_inv_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) (w : ℂ) : HasFDerivAt (fun (w : ℂ) => ∫ (z : ℂ), (w - z)⁻¹ • f z) (∫ (z : ℂ), (w - z)⁻¹ • fderiv ℝ f z) w

The Cauchy transform w ↦ ∫ (w - z)⁻¹ • f z of a compactly supported C¹ map f is differentiable, and its derivative is the Cauchy transform of the derivative of f.

theorem HasCompactSupport.fderiv_apply_one_add_I_smul_apply_I_two_pi_inv_smul_integral_sub_inv_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) (w : ℂ) : (fderiv ℝ (fun (w : ℂ) => (2 * ↑Real.pi)⁻¹ • ∫ (z : ℂ), (w - z)⁻¹ • f z) w) 1 + Complex.I • (fderiv ℝ (fun (w : ℂ) => (2 * ↑Real.pi)⁻¹ • ∫ (z : ℂ), (w - z)⁻¹ • f z) w) Complex.I = f w

The Cauchy transform inverts D = 2 \bar∂ from the other side: for a compactly supported C¹ map f : ℂ → F, the transform T f w = (2π)⁻¹ ∫ (w - z)⁻¹ • f z satisfies ∂ₓ (T f) + i ∂ᵧ (T f) = f, that is 2 \bar∂ (T f) = f.

theorem HasCompactSupport.conjWirtingerDeriv_integral_sub_inv_smul_apply_one {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) (w : ℂ) : (TauCeti.conjWirtingerDeriv (fun (w : ℂ) => ∫ (z : ℂ), (w - z)⁻¹ • f z) w) 1 = ↑Real.pi • f w

The Cauchy transform solves \bar∂ u = f. For a compactly supported C¹ map f, the conjugate Wirtinger derivative of w ↦ ∫ (w - z)⁻¹ • f z is π • f, so the Cauchy transform π⁻¹ ∫ (w - z)⁻¹ • f z satisfies \bar∂ u = f.

theorem HasCompactSupport.differentiableAt_integral_sub_inv_smul_of_eq_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) {w : ℂ} (hw : f w = 0) : DifferentiableAt ℂ (fun (w : ℂ) => ∫ (z : ℂ), (w - z)⁻¹ • f z) w

The Cauchy transform of a compactly supported C¹ map f is complex differentiable at every point where f vanishes.

theorem TauCeti.differentiableOn_integral_sub_inv_smul_compl {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {k : Set ℂ} (hk : IsCompact k) (hfk : ∀ x ∉ k, f x = 0) (hf : ContDiff ℝ 1 f) : DifferentiableOn ℂ (fun (w : ℂ) => ∫ (z : ℂ), (w - z)⁻¹ • f z) kᶜ

The Cauchy transform of a C¹ map f vanishing outside a compact set k is holomorphic on the complement of k. For compactly supported f, taking k = tsupport f shows that the transform is holomorphic off the support of f. Applied to a family g p vanishing outside a common compact set k, this gives a region of holomorphy independent of the parameter p.

theorem HasCompactSupport.hasFDerivAt_cauchyTransform {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) (w : ℂ) : HasFDerivAt (TauCeti.cauchyTransform f) ((↑Real.pi)⁻¹ • ∫ (z : ℂ), (w - z)⁻¹ • fderiv ℝ f z) w

The real derivative of the Cauchy transform on compactly supported C¹ data is obtained by applying the same kernel to the derivative of the source.

theorem HasCompactSupport.contDiff_cauchyTransform {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {n : ℕ∞} {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ (↑n) f) : ContDiff ℝ (↑n) (TauCeti.cauchyTransform f)

The Cauchy transform of compactly supported data is as smooth as the data.

theorem HasCompactSupport.continuous_wirtingerDeriv_cauchyTransform {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) : Continuous fun (w : ℂ) => (TauCeti.wirtingerDeriv (TauCeti.cauchyTransform f) w) 1

The Wirtinger derivative ∂ (T f) of the Cauchy transform of compactly supported C¹ data is continuous.

theorem HasCompactSupport.conjWirtingerDeriv_cauchyTransform {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) (w : ℂ) : (TauCeti.conjWirtingerDeriv (TauCeti.cauchyTransform f) w) 1 = f w

On compactly supported C¹ data the normalized Cauchy transform is a right inverse of bar∂ = (∂ₛ + i ∂ₜ) / 2.

theorem HasCompactSupport.cauchyTransform_conjWirtingerDeriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {u : ℂ → F} (hc : HasCompactSupport u) (hu : ContDiff ℝ 1 u) (w : ℂ) : TauCeti.cauchyTransform (fun (z : ℂ) => (TauCeti.conjWirtingerDeriv u z) 1) w = u w

The normalized Cauchy transform is also a left inverse on compactly supported C¹ maps: applying it to bar∂ u recovers u, with no boundary term.

theorem HasCompactSupport.fderiv_cauchyTransform {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) : fderiv ℝ (TauCeti.cauchyTransform f) = TauCeti.cauchyTransform (fderiv ℝ f)

On compactly supported C¹ data the real derivative of the Cauchy transform is the Cauchy transform of the real derivative.

theorem HasCompactSupport.fderiv_cauchyTransform_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (hc : HasCompactSupport f) (hf : ContDiff ℝ 1 f) (w v : ℂ) : (fderiv ℝ (TauCeti.cauchyTransform f) w) v = TauCeti.cauchyTransform (fun (z : ℂ) => (fderiv ℝ f z) v) w

The directional derivative of the Cauchy transform of compactly supported C¹ data in the direction v is the Cauchy transform of the directional derivative of the data.

theorem HasCompactSupport.differentiableAt_cauchyTransform_of_notMem_tsupport {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {c : ℂ → F} (hc : HasCompactSupport c) (hs : ContDiff ℝ 1 c) {w : ℂ} (hw : w ∉ tsupport c) : DifferentiableAt ℂ (TauCeti.cauchyTransform c) w

The Cauchy transform of a compactly supported C¹ map is holomorphic off the support of the map.

theorem HasCompactSupport.tendsto_cauchyTransform_cobounded {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {c : ℂ → F} (hc : HasCompactSupport c) (hi : MeasureTheory.Integrable c MeasureTheory.volume) : Filter.Tendsto (TauCeti.cauchyTransform c) (Bornology.cobounded ℂ) (nhds 0)

The Cauchy transform of a compactly supported integrable map tends to 0 at infinity.