Planar Cauchy kernel estimates

The complex reciprocal and its norm are locally integrable. Their integrals over a disk admit a uniform bound in terms of the radius when the pole lies in that disk. Compact truncation of the kernel also gives local L¹ continuity as the pole varies.

theorem Complex.locallyIntegrable_sub_inv (w : ℂ) : MeasureTheory.LocallyIntegrable (fun (z : ℂ) => (w - z)⁻¹) MeasureTheory.volume

The kernel z ↦ (w - z)⁻¹ of the Cauchy transform is locally integrable on ℂ.

theorem Complex.locallyIntegrable_inv : MeasureTheory.LocallyIntegrable (fun (z : ℂ) => z⁻¹) MeasureTheory.volume

The Cauchy kernel z ↦ z⁻¹ is locally integrable on ℂ.

noncomputable def TauCeti.truncatedCauchyKernel (R : ℝ) : ℂ → ℂ

The reciprocal kernel cut off outside the closed disk of radius R.

Equations

• TauCeti.truncatedCauchyKernel R = (Metric.closedBall 0 R).indicator fun (z : ℂ) => z⁻¹

theorem TauCeti.truncatedCauchyKernel_def (R : ℝ) : truncatedCauchyKernel R = (Metric.closedBall 0 R).indicator fun (z : ℂ) => z⁻¹

The cutoff kernel is the indicator of the reciprocal on its closed disk.

theorem TauCeti.measurable_truncatedCauchyKernel (R : ℝ) : Measurable (truncatedCauchyKernel R)

The truncated Cauchy kernel is measurable.

theorem TauCeti.integrable_truncatedCauchyKernel (R : ℝ) : MeasureTheory.Integrable (truncatedCauchyKernel R) MeasureTheory.volume

The truncated Cauchy kernel is integrable.

theorem TauCeti.integral_norm_sub_inv_closedBall_le {w c : ℂ} {R : ℝ} (hw : w ∈ Metric.closedBall c R) : ∫ (z : ℂ) in Metric.closedBall c R, ‖z - w‖⁻¹ ≤ 4 * Real.pi * R

A pole in a disk of radius R contributes at most 4πR to its inverse-distance integral.

theorem TauCeti.integral_norm_sub_inv_closedBall {R : ℝ} (hR : 0 ≤ R) (w : ℂ) : ∫ (z : ℂ) in Metric.closedBall w R, ‖z - w‖⁻¹ = 2 * Real.pi * R

The inverse-distance integral over a disk centered at its pole is 2πR.

theorem TauCeti.integral_norm_truncatedCauchyKernel {R : ℝ} (hR : 0 ≤ R) : ∫ (z : ℂ), ‖truncatedCauchyKernel R z‖ = 2 * Real.pi * R

The L¹ norm of the truncated reciprocal kernel is 2πR.

theorem TauCeti.tendsto_integral_norm_sub_inv_sub_sub_inv_closedBall {ι : Type u_1} {l : Filter ι} {wn : ι → ℂ} {w : ℂ} (hw : Filter.Tendsto wn l (nhds w)) (c : ℂ) (R : ℝ) : Filter.Tendsto (fun (n : ι) => ∫ (z : ℂ) in Metric.closedBall c R, ‖(z - wn n)⁻¹ - (z - w)⁻¹‖) l (nhds 0)

Moving the pole continuously gives local L¹ convergence of the complex reciprocal kernel.