Bridge single singularity — verified re-export #
bridge_single_singularity_base is a proved theorem in Lecture14.lean,
reduced from circleIntegral_eq_sum_of_singularities with Fin 1.
This file re-exports the result for discoverability.
theorem
bridge_single_singularity
{c : ℂ}
{R : ℝ}
(hR : 0 < R)
{a₀ : ℂ}
{r₀ : ℝ}
{f : ℂ → ℂ}
(ha : a₀ ∈ Metric.ball c R)
(hr : 0 < r₀)
(hrd : Metric.closedBall a₀ r₀ ⊆ Metric.ball c R)
(hcont : ContinuousOn f (Metric.closedBall c R \ {a₀}))
(hdiff : ∀ z ∈ Metric.ball c R \ {a₀}, DifferentiableAt ℂ f z)
:
Non-concentric single-singularity contour deformation (re-export).
The integral of f over C(c,R) equals the integral over C(a₀,r₀) when
f is holomorphic on closedBall c R \ {a₀} and closedBall a₀ r₀ ⊆ ball c R.