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

When f is differentiable on closedBall a r and z ∈ ball a r, the Cauchy transform (2πi)⁻¹ ∮ (z-w)⁻¹ f(w) dw = -f(z).

Note the sign: (z-w)⁻¹ = -(w-z)⁻¹, so this picks up a minus sign compared to the standard CIF with (w-z)⁻¹.

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

The Cauchy transform z ↦ ∮_{C(a,r)} (z - w)⁻¹ * φ(w) dw is continuous at any point z₀ not on the circle sphere a r.

theorem differentiableOn_cauchy_transform_inside {a : ℂ} {r : ℝ} (hr : 0 < r) {φ : ℂ → ℂ} (hint : CircleIntegrable φ a r) : DifferentiableOn ℂ (fun (z : ℂ) => ∮ (w : ℂ) in C(a, r), (z - w)⁻¹ * φ w) (Metric.ball a r)

A Cauchy-type integral z ↦ ∮_{C(a,r)} (z - w)⁻¹ * φ(w) dw is holomorphic (differentiable at every point) inside the circle ball a r, for any circle-integrable function φ.

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

The Cauchy transform z ↦ ∮_{C(a,r)} (z - w)⁻¹ * φ(w) dw is differentiable at any point z₀ whose distance from the center a is not equal to r (i.e., z₀ is not on the circle), provided φ is circle-integrable.