noncomputable def CauchyKernel.cauchyKernel (p : ℝ × ℝ) : ℂ

The Cauchy kernel K(x, y) = (2π)^{-1} · (x + i y)^{-1} on ℝ², identifying a real point (x, y) with the complex number x + i y. Acts as a fundamental solution for the Cauchy–Riemann operator.

noncomputable def CauchyKernel.cauchyKernelBare (p : ℝ × ℝ) : ℂ

The Cauchy kernel without the (2π)^{-1} prefactor: (x + i y)^{-1}. Useful for integrability arguments where the constant is irrelevant.

theorem CauchyKernel.norm_polar (r θ : ℝ) (hr : 0 < r) : ‖↑(r * Real.cos θ) + Complex.I * ↑(r * Real.sin θ)‖ = r

Polar magnitude: ‖r cos θ + i r sin θ‖ = r for r > 0.

theorem CauchyKernel.norm_cauchyKernelBare_polarCoord_symm {r θ : ℝ} (hr : 0 < r) : ‖cauchyKernelBare (↑polarCoord.symm (r, θ))‖ = r⁻¹

The norm of the bare Cauchy kernel at the polar point (r, θ) equals r⁻¹.

theorem CauchyKernel.polar_in_closedBall_bound {r θ R : ℝ} (hr : 0 < r) (hmem : ↑polarCoord.symm (r, θ) ∈ Metric.closedBall 0 R) : r ≤ R * √2

If the polar point (r, θ) (with r > 0) sits in the closed ball of radius R for the product metric on ℝ × ℝ, then r ≤ R · √2.

theorem CauchyKernel.integrableOn_cauchyKernelBare_closedBall (R : ℝ) (hR : 0 < R) : MeasureTheory.IntegrableOn cauchyKernelBare (Metric.closedBall 0 R) MeasureTheory.volume

The bare Cauchy kernel (x + i y)^{-1} is Lebesgue-integrable on the closed ball of radius R in ℝ². In polar coordinates the Jacobian r dr cancels the r⁻¹ singularity, giving a bounded integral.

theorem CauchyKernel.cauchyKernelBare_locallyIntegrable : MeasureTheory.LocallyIntegrable cauchyKernelBare MeasureTheory.volume

Lemma 11.5 (Melrose): the bare Cauchy kernel (x + i y)^{-1} is locally integrable on ℝ². This is the key fact making the Cauchy–Riemann fundamental solution a well-defined distribution.