Cauchy Transform Continuity

Infrastructure for boundary behavior of the Cauchy transform. Proves:

• ContinuousOn versions of the Cauchy transform away from the integration circle
• The CIF with (w - z)⁻¹ kernel
• Vanishing of the Cauchy integral outside the contour (for holomorphic functions)
• Sign-flip corollaries connecting (z - w)⁻¹ and (w - z)⁻¹ kernels

theorem continuousOn_cauchy_transform_off_sphere {a : ℂ} {r : ℝ} {φ : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable φ a r) {S : Set ℂ} (hS : Disjoint S (Metric.sphere a r)) : ContinuousOn (fun (z : ℂ) => ∮ (w : ℂ) in C(a, r), (z - w)⁻¹ * φ w) S

ContinuousOn version: the Cauchy transform with kernel (z - w)⁻¹ is continuous on any set disjoint from the integration circle.

theorem circleIntegral_zw_eq_neg_wz {a : ℂ} {r : ℝ} {φ : ℂ → ℂ} (z : ℂ) : ∮ (w : ℂ) in C(a, r), (z - w)⁻¹ * φ w = -∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * φ w

Relationship between (z - w)⁻¹ and (w - z)⁻¹ kernels in the circle integral.

theorem continuousOn_cauchy_transform_wz_off_sphere {a : ℂ} {r : ℝ} {φ : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable φ a r) {S : Set ℂ} (hS : Disjoint S (Metric.sphere a r)) : ContinuousOn (fun (z : ℂ) => ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * φ w) S

ContinuousOn version: the Cauchy transform with kernel (w - z)⁻¹ is continuous on any set disjoint from the integration circle.

theorem cauchy_integral_formula_wz {a : ℂ} {r : ℝ} {f : ℂ → ℂ} (hf_diff : ∀ z ∈ Metric.closedBall a r, DifferentiableAt ℂ f z) {z : ℂ} (hz : z ∈ Metric.ball a r) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w = f z

Cauchy integral formula with (w - z)⁻¹ kernel. For f differentiable on closedBall a r and z ∈ ball a r: (2πi)⁻¹ * ∮ (w - z)⁻¹ f(w) dw = f(z)

theorem cauchy_integral_vanishes_outside {a : ℂ} {r : ℝ} (hr : 0 < r) {f : ℂ → ℂ} (hf_cont : ContinuousOn f (Metric.closedBall a r)) (hf_diff : ∀ z ∈ Metric.ball a r, DifferentiableAt ℂ f z) {z : ℂ} (hz : z ∉ Metric.closedBall a r) : ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w = 0

For f holomorphic on closedBall a r and z ∉ closedBall a r, the Cauchy integral ∮ (w - z)⁻¹ f(w) dw vanishes. This is because w ↦ (w - z)⁻¹ f(w) is holomorphic on the entire closed ball.

theorem continuousAt_cauchy_integral_wz {a : ℂ} {r : ℝ} {φ : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable φ a r) {z₀ : ℂ} (hz₀ : z₀ ∉ Metric.sphere a r) : ContinuousAt (fun (z : ℂ) => (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * φ w) z₀

The scaled Cauchy integral (2πi)⁻¹ * ∮ (w - z)⁻¹ f(w) dw is continuous at any point z₀ not on the circle sphere a r.

theorem differentiableAt_cauchy_integral_wz {a : ℂ} {r : ℝ} {φ : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable φ a r) {z₀ : ℂ} (hz₀ : z₀ ∉ Metric.sphere a r) : DifferentiableAt ℂ (fun (z : ℂ) => (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * φ w) z₀

The Cauchy integral (2πi)⁻¹ * ∮ (w - z)⁻¹ f(w) dw is differentiable at any point not on the circle.

theorem continuousOn_cauchy_integral_wz_off_sphere {a : ℂ} {r : ℝ} {φ : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable φ a r) {S : Set ℂ} (hS : Disjoint S (Metric.sphere a r)) : ContinuousOn (fun (z : ℂ) => (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * φ w) S

ContinuousOn version: the scaled Cauchy integral (2πi)⁻¹ * ∮ (w - z)⁻¹ f(w) dw is continuous on any set disjoint from the integration circle.

theorem differentiableAt_add_cauchy_integral {a : ℂ} {r : ℝ} {f : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable f a r) {z₀ : ℂ} (hz₀ : z₀ ∉ Metric.sphere a r) (hf : DifferentiableAt ℂ f z₀) : DifferentiableAt ℂ (fun (z : ℂ) => f z + (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w) z₀

The function f(z) + (2πi)⁻¹ ∮ (w-z)⁻¹ f(w) dw is differentiable at any point z₀ that lies outside sphere a r and where f is differentiable, provided f is circle-integrable on C(a, r).

theorem continuousAt_add_cauchy_integral {a : ℂ} {r : ℝ} {f : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable f a r) {z₀ : ℂ} (hz₀ : z₀ ∉ Metric.sphere a r) (hf : ContinuousAt f z₀) : ContinuousAt (fun (z : ℂ) => f z + (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w) z₀

The function f(z) + (2πi)⁻¹ ∮ (w-z)⁻¹ f(w) dw is continuous at any point z₀ that lies outside sphere a r and where f is continuous, provided f is circle-integrable on C(a, r).

theorem continuousOn_add_cauchy_integral {a : ℂ} {r : ℝ} {f : ℂ → ℂ} (hr : 0 < r) (hint : CircleIntegrable f a r) {S : Set ℂ} (hS : Disjoint S (Metric.sphere a r)) (hf : ContinuousOn f S) : ContinuousOn (fun (z : ℂ) => f z + (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w) S

ContinuousOn version: f + (2πi)⁻¹ ∮ (w-z)⁻¹ f(w) dw is continuous on any set where f is continuous and that is disjoint from the integration circle.

theorem cauchy_integral_formula_wz_off_countable {a : ℂ} {r : ℝ} {f : ℂ → ℂ} {s : Set ℂ} (hs : s.Countable) (hf_cont : ContinuousOn f (Metric.closedBall a r)) (hf_diff : ∀ z ∈ Metric.ball a r \ s, DifferentiableAt ℂ f z) {z : ℂ} (hz : z ∈ Metric.ball a r) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w = f z

Generalized CIF with (w - z)⁻¹ kernel allowing a countable exceptional set. For f continuous on closedBall a r, differentiable on ball a r \ s (where s is countable), and z ∈ ball a r: (2πi)⁻¹ * ∮ (w - z)⁻¹ f(w) dw = f(z)

theorem cauchy_integral_vanishes_outside_off_countable {a : ℂ} {r : ℝ} (hr : 0 < r) {f : ℂ → ℂ} {s : Set ℂ} (hs : s.Countable) (hf_cont : ContinuousOn f (Metric.closedBall a r)) (hf_diff : ∀ z ∈ Metric.ball a r \ s, DifferentiableAt ℂ f z) {z : ℂ} (hz : z ∉ Metric.closedBall a r) : ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w = 0

For f continuous on closedBall a r, differentiable on ball a r \ s, and z ∉ closedBall a r, the Cauchy integral ∮ (w - z)⁻¹ f(w) dw vanishes. This generalizes cauchy_integral_vanishes_outside to allow a countable exceptional set.

theorem add_cauchy_integral_eq_double {a : ℂ} {r : ℝ} {f : ℂ → ℂ} (hf_diff : ∀ z ∈ Metric.closedBall a r, DifferentiableAt ℂ f z) {z : ℂ} (hz : z ∈ Metric.ball a r) : f z + (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a, r), (w - z)⁻¹ * f w = 2 * f z

When f is holomorphic on closedBall a r and z ∈ ball a r, the sum f(z) + (2πi)⁻¹ ∮ (w-z)⁻¹ f(w) dw equals 2 * f(z) by the Cauchy integral formula.