Holomorphic extension of f + P to ball(c,R)

Given f holomorphic on ball c R with closedBall a₀ r₀ ⊆ ball c R and r₀ > 0, let P(z) = (2πi)⁻¹ ∮_{C(a₀,r₀)} (z - w)⁻¹ f(w) dw be the Cauchy transform.

The main results:

1. f_plus_cauchy_transform_eq_zero_inside: On ball a₀ r₀, f + P = 0 by CIF.
2. cauchy_transform_eq_zero_outside: Outside closedBall a₀ r₀, P = 0.
3. f_plus_cauchy_transform_differentiableOn: f + P is holomorphic on ball c R \ sphere a₀ r₀ (the maximal open domain where f + P is defined).
4. f_plus_cauchy_transform_holomorphic_extension: There exists g holomorphic on all of ball c R that agrees with f + P on ball c R \ closedBall a₀ r₀.

Note: The literal Lean function z ↦ f z + (2πi)⁻¹ * ∮ (z-w)⁻¹ * f(w) dw is discontinuous at sphere points (the Bochner integral of the non-integrable integrand defaults to 0 in Lean, giving f(z₀) + 0 ≠ 0 while f + P → 0 from inside). The existential formulation provides the holomorphic extension via f.

theorem f_plus_cauchy_transform_eq_zero_inside {a₀ : ℂ} {r₀ : ℝ} (hr₀ : 0 < 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₀), (z - w)⁻¹ * f w = 0

On ball a₀ r₀, the Cauchy integral formula gives f + P = 0.

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

Outside closedBall a₀ r₀, the Cauchy transform vanishes. The integrand w ↦ (w - z)⁻¹ * f(w) is holomorphic on closedBall a₀ r₀ (since z is outside), so ∮ = 0 by Cauchy's theorem.

theorem f_plus_cauchy_transform_differentiableOn {c a₀ : ℂ} {R r₀ : ℝ} (_hR : 0 < R) (hr₀ : 0 < r₀) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball c R)) (hsub : Metric.closedBall a₀ r₀ ⊆ Metric.ball c R) : DifferentiableOn ℂ (fun (z : ℂ) => f z + (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a₀, r₀), (z - w)⁻¹ * f w) (Metric.ball c R \ Metric.sphere a₀ r₀)

f + P is differentiable on ball c R \ sphere a₀ r₀, where P(z) = (2πi)⁻¹ ∮_{C(a₀,r₀)} (z - w)⁻¹ f(w) dw is the Cauchy transform.

On ball a₀ r₀, f + P = 0 (holomorphic). On ball c R \ closedBall a₀ r₀, both f and P are holomorphic. Their union covers ball c R \ sphere a₀ r₀.

theorem f_plus_cauchy_transform_holomorphic_extension {c a₀ : ℂ} {R r₀ : ℝ} (_hR : 0 < R) (hr₀ : 0 < r₀) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball c R)) (hsub : Metric.closedBall a₀ r₀ ⊆ Metric.ball c R) : ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g (Metric.ball c R) ∧ ∀ z ∈ Metric.ball c R \ Metric.closedBall a₀ r₀, g z = f z + (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (w : ℂ) in C(a₀, r₀), (z - w)⁻¹ * f w

Holomorphic extension of f + P to all of ball(c,R).

There exists g holomorphic on the full ball c R that agrees with f + P on ball c R \ closedBall a₀ r₀ (where P = 0, so f + P = f). The witness is f.

On the interior component ball a₀ r₀, f + P = 0 by f_plus_cauchy_transform_eq_zero_inside.

theorem f_plus_cauchy_transform_diffContOnCl {c : ℂ} {R : ℝ} {f : ℂ → ℂ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : Metric.closedBall c R ⊆ U) : DiffContOnCl ℂ f (Metric.ball c R)

DiffContOnCl for the holomorphic extension.

When f is differentiable on a set U containing closedBall c R, the holomorphic extension of f + P (which is f itself) satisfies DiffContOnCl ℂ f (ball c R).

theorem f_circleIntegral_eq_zero_of_diffOn_closedBall {c : ℂ} {R : ℝ} (hR : 0 < R) {f : ℂ → ℂ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : Metric.closedBall c R ⊆ U) : ∮ (z : ℂ) in C(c, R), f z = 0

Vanishing circle integral via DiffContOnCl.

When f is differentiable on U ⊇ closedBall c R, the circle integral ∮_{C(c,R)} f = 0 by Cauchy-Goursat.

theorem f_circleIntegral_eq_of_diffOn_closedBall {c a₀ : ℂ} {R r₀ : ℝ} (hR : 0 < R) (hr₀ : 0 < r₀) {f : ℂ → ℂ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : Metric.closedBall c R ⊆ U) (hsub : Metric.closedBall a₀ r₀ ⊆ Metric.ball c R) : ∮ (z : ℂ) in C(c, R), f z = ∮ (z : ℂ) in C(a₀, r₀), f z

Non-concentric circle integral equality for holomorphic functions.

If f is differentiable on U ⊇ closedBall c R and closedBall a₀ r₀ ⊆ ball c R, then ∮_{C(c,R)} f = ∮_{C(a₀,r₀)} f. Since f is holomorphic on the entire closed ball (no singularities), both integrals equal zero.