Cauchy's integral formula on smooth convex Jordan domains

The smooth-Jordan Cauchy theorem extends to the Cauchy integral formula by removing the apparent singularity with dslope. The resulting identity is first stated using the raw scalar contour mass, then normalized under winding one. Oriented and canonical-orientation corollaries expose the forms needed by polynomial approximation on smooth convex domains.

theorem DiffContOnCl.dslope_of_mem_isOpen {U : Set ℂ} {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f U) (hU : IsOpen U) {z : ℂ} (hz : z ∈ U) : DiffContOnCl ℂ (dslope f z) U

The divided difference of a DiffContOnCl scalar function, filled in by the derivative at an interior point, is again DiffContOnCl.

theorem contourIntegral_inv_sub_mul_eq_contourIntegral_inv_sub_mul_value (Omega : SmoothJordanDomain) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f Omega.carrier) {z : ℂ} (hz : z ∈ Omega.carrier) : contourIntegral (fun (sigma : ℂ) => (sigma - z)⁻¹ * f sigma) Omega.boundaryParam = contourIntegral (fun (sigma : ℂ) => (sigma - z)⁻¹) Omega.boundaryParam * f z

Cauchy's formula before winding normalization: the contour integral of (sigma - z)⁻¹ f(sigma) is the raw scalar contour mass times f z.

theorem contourIntegral_inv_sub_mul_eq_two_pi_I_mul_of_kernel_eq_one (Omega : SmoothJordanDomain) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f Omega.carrier) {z : ℂ} (hz : z ∈ Omega.carrier) (hkernel : crouzeixScalarCauchyKernel Omega z = 1) : contourIntegral (fun (sigma : ℂ) => (sigma - z)⁻¹ * f sigma) Omega.boundaryParam = 2 * ↑Real.pi * Complex.I * f z

Cauchy's formula on a smooth Jordan carrier at a point where the normalized scalar winding kernel is one.

theorem contourIntegral_mul_inv_sub_eq_two_pi_I_mul_of_kernel_eq_one (Omega : SmoothJordanDomain) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f Omega.carrier) {z : ℂ} (hz : z ∈ Omega.carrier) (hkernel : crouzeixScalarCauchyKernel Omega z = 1) : contourIntegral (fun (sigma : ℂ) => f sigma * (sigma - z)⁻¹) Omega.boundaryParam = 2 * ↑Real.pi * Complex.I * f z

Cauchy's formula with the boundary datum placed before the scalar kernel, matching the exterior-kernel approximation interface.

theorem contourIntegral_mul_inv_sub_eq_two_pi_I_mul_of_oriented_carrier (Omega : SmoothJordanDomain) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f Omega.carrier) (c : ℂ) (hc : c ∈ Omega.carrier) (hcside : ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) {z : ℂ} (hz : z ∈ Omega.carrier) : contourIntegral (fun (sigma : ℂ) => f sigma * (sigma - z)⁻¹) Omega.boundaryParam = 2 * ↑Real.pi * Complex.I * f z

Consistent supporting-normal orientation supplies the winding-one hypothesis in Cauchy's formula.

theorem contourIntegral_mul_inv_sub_eq_two_pi_I_mul_canonicalOrientation (Omega : SmoothJordanDomain) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f Omega.carrier) {z : ℂ} (hz : z ∈ Omega.carrier) : contourIntegral (fun (sigma : ℂ) => f sigma * (sigma - z)⁻¹) Omega.canonicalOrientation.boundaryParam = 2 * ↑Real.pi * Complex.I * f z

The canonical orientation of every smooth convex Jordan domain satisfies the winding-one Cauchy integral formula.

theorem cauchyFormula_canonicalOrientation (Omega : SmoothJordanDomain) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f Omega.carrier) {z : ℂ} (hz : z ∈ Omega.carrier) : f z = (2 * ↑Real.pi * Complex.I)⁻¹ * contourIntegral (fun (sigma : ℂ) => f sigma * (sigma - z)⁻¹) Omega.canonicalOrientation.boundaryParam

The normalized Cauchy integral formula on the canonical orientation, with f z isolated for direct use by polynomial approximation.