The Cauchy kernel, the Cauchy transform, and Cauchy–Pompeiu (Forster 13.1)

Unit: dbar-solvability (docs/design/dbar-solvability.md §4.2, §5). Mathlib-only planar file.

cauchyKernel w := (π w)⁻¹; cauchyTransform g := cauchyKernel ⋆[mul ℝ ℂ] g. The pointwise identity dbar(cauchyKernel ⋆ g) = g for compactly supported C¹ g (cauchyPompeiu) is proved by polar coordinates + 1-D FTC in the radial and angular directions (design §5): the convolution derivative package handles "differentiate under the integral", and the polar substitution makes the kernel singularity cancel exactly.

noncomputable def RS.cauchyKernel : ℂ → ℂ

The Cauchy kernel 1/(π w).

Equations

• RS.cauchyKernel w = (↑Real.pi * w)⁻¹

theorem RS.measurable_cauchyKernel : Measurable cauchyKernel

theorem RS.aestronglyMeasurable_cauchyKernel : MeasureTheory.AEStronglyMeasurable cauchyKernel MeasureTheory.volume

theorem RS.norm_cauchyKernel (w : ℂ) : ‖cauchyKernel w‖ = (Real.pi * ‖w‖)⁻¹

theorem RS.integrableOn_cauchyKernel_ball (ρ : ℝ) : MeasureTheory.IntegrableOn cauchyKernel (Metric.ball 0 ρ) MeasureTheory.volume

Step 1 of the design: cauchyKernel is integrable on every ball centred at 0.

theorem RS.locallyIntegrable_cauchyKernel : MeasureTheory.LocallyIntegrable cauchyKernel MeasureTheory.volume

The Cauchy transform and its derivative (design §5, step 2)

noncomputable def RS.cauchyTransform (g : ℂ → ℂ) : ℂ → ℂ

The Cauchy transform cauchyKernel ⋆ g.

Equations

• RS.cauchyTransform g = MeasureTheory.convolution RS.cauchyKernel g (ContinuousLinearMap.mul ℝ ℂ) MeasureTheory.volume

theorem RS.contDiff_cauchyTransform (g : ℂ → ℂ) (hg : ContDiff ℝ (↑⊤) g) (hcs : HasCompactSupport g) : ContDiff ℝ (↑⊤) (cauchyTransform g)

theorem RS.wirtingerDbar_cauchyTransform (g : ℂ → ℂ) (hg : ContDiff ℝ (↑⊤) g) (hcs : HasCompactSupport g) (z : ℂ) : wirtingerDbar (cauchyTransform g) z = ∫ (w : ℂ), cauchyKernel w * wirtingerDbar g (z - w)

Step 2: differentiation under the integral, via the convolution-derivative package.

Cauchy–Pompeiu (design §5, steps 0, 1, 3–8)

theorem RS.cauchyPompeiu (g : ℂ → ℂ) (hg : ContDiff ℝ 1 g) (hcs : HasCompactSupport g) (z : ℂ) : ∫ (w : ℂ), cauchyKernel w * wirtingerDbar g (z - w) = g z

Forster 13.1 / Cauchy–Pompeiu, proved by the polar-FTC computation of design §5.

theorem RS.wirtingerDbar_cauchyTransform_eq (g : ℂ → ℂ) (hg : ContDiff ℝ (↑⊤) g) (hcs : HasCompactSupport g) (z : ℂ) : wirtingerDbar (cauchyTransform g) z = g z

Forster 13.1: dbar of the Cauchy transform recovers g.

theorem RS.exists_dbar_solution_of_hasCompactSupport (g : ℂ → ℂ) (hg : ContDiff ℝ (↑⊤) g) (hcs : HasCompactSupport g) : ∃ (u : ℂ → ℂ), ContDiff ℝ (↑⊤) u ∧ ∀ (z : ℂ), wirtingerDbar u z = g z

Forster 13.1, existential form: dbaru = g is solvable for compactly supported smooth g.