The annulus Stokes identity and the smeared residue theorem

Unit: planar-stokes-atoms (docs/design/planar-stokes.md §7–§8). Two theorems:

• circleIntegral_sub_circleIntegral_eq_two_mul_I_mul_integral_wirtingerDbar (Atom 1′): the area-to-boundary identity for the dbar of an arbitrary C¹ function on a closed annulus, proved by the exponential substitution w = c + exp ζ mapping a rectangle onto the annulus. No meromorphy, no residues.
• integral_wirtingerDbar_mul_eq_neg_pi_mul_resAt (Atom 2, the smeared residue theorem) and its model-case regression check integral_wirtingerDbar_mul_inv_sub_eq (f = 1/(z-p), proved a second, independent way via RS.cauchyPompeiu).

Deviation from the design's §7 proof sketch: instead of routing the area term through Complex.polarCoord (whose target Ioi 0 ×ˢ Ioo(-π,π) forces a periodicity-shift reconciliation against the [0,2π] circle parametrization), we apply MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul directly to the substitution τ ζ = c + exp ζ on the half-open-in-angle rectangle Icc a b ×ℂ Ico 0 (2π) (a = log r, b = log R), which τ maps bijectively onto the annulus (no missing ray, unlike the open rectangle) — a shorter route to the same identity, using the same mathlib machinery flagged as the design's own R2 fallback.

Helper facts

The annulus identity (Atom 1′)

theorem RS.circleIntegral_sub_circleIntegral_eq_two_mul_I_mul_integral_wirtingerDbar {u : ℂ → ℂ} {c : ℂ} {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) (hu : ContDiffOn ℝ 1 u (Metric.closedBall c R \ Metric.ball c r)) : (∮ (w : ℂ) in C(c, R), u w) - ∮ (w : ℂ) in C(c, r), u w = 2 * Complex.I * ∫ (w : ℂ) in Metric.closedBall c R \ Metric.ball c r, wirtingerDbar u w

Atom 1′ (annulus Stokes, general — no meromorphy, no residue): area-to-boundary identity for the dbar of an arbitrary C¹ function on a closed annulus.

The smeared residue theorem (Atom 2)

theorem RS.integral_wirtingerDbar_mul_eq_neg_pi_mul_resAt {g f : ℂ → ℂ} {U : Set ℂ} {p : ℂ} (hU : IsOpen U) (_hpU : p ∈ U) (hg : ContDiffOn ℝ 1 g U) (hcs : HasCompactSupport g) (hsub : tsupport g ⊆ U) (hconst : g =ᶠ[nhds p] Function.const ℂ (g p)) (hf : DifferentiableOn ℂ f (U \ {p})) (hfp : MeromorphicAt f p) : ∫ (w : ℂ), wirtingerDbar g w * f w = -↑Real.pi * g p * resAt f p

Atom 2 (the smeared residue theorem — the "one honest integration atom" routing decision #2 budgets for): g compactly supported in U, locally CONSTANT near the puncture p (§D4), f holomorphic on U \ {p} and meromorphic at p.

Model-case regression check (f = (·-p)⁻¹, §8.4), and the abel-weak-solutions refinement

theorem RS.integral_wirtingerDbar_mul_inv_sub_eq {g : ℂ → ℂ} {U : Set ℂ} {p : ℂ} (hU : IsOpen U) (hg : ContDiffOn ℝ 1 g U) (hcs : HasCompactSupport g) (hsub : tsupport g ⊆ U) : ∫ (w : ℂ), wirtingerDbar g w * (w - p)⁻¹ = -↑Real.pi * g p

Model-case corollary (the verification the task asked for, f = 1/(z-p), kept as a named sanity lemma / regression test on Atom 2's -π normalization constant) — proved a second, independent way, translating RS.cauchyPompeiu (dbar-solvability) through the measure-preserving involution w ↦ p - w, NOT as a corollary of Atom 2 itself.

Deviation from the design's §5.3 signature: the frozen design states this lemma with the same hpU/hconst hypotheses as Atom 2, "for signature parity" only. Both are provably UNUSED in this proof (neither name appears in the tactic block below) — exactly as the design's own §8.4 already observes ("a simple pole is exactly the borderline order where the general-g and locally- constant-g formulas coincide... with no local-constancy hypothesis on g needed at all in this special case"). Dropped here because abel-weak-solutions (this unit's downstream consumer, docs/design/abel-weak-solutions.md §7.3/§10/§11 risk R1) needs exactly this hypothesis-free form: its g is a genuine holomorphic primitive, not locally constant near its punctures, so it cannot supply hconst. See integral_wirtingerDbar_mul_inv_sub_sub_inv_sub_eq below for the exact two-puncture shape that unit's Lemma 20.3 step assembles.

theorem RS.integrable_wirtingerDbar_mul_inv_sub {g : ℂ → ℂ} {U : Set ℂ} {p : ℂ} (hU : IsOpen U) (hg : ContDiffOn ℝ 1 g U) (hcs : HasCompactSupport g) (hsub : tsupport g ⊆ U) : MeasureTheory.Integrable (fun (w : ℂ) => wirtingerDbar g w * (w - p)⁻¹) MeasureTheory.volume

The wirtingerDbar g · (·-p)⁻¹ integrand of the model-case identity above is integrable (needed to combine several single-puncture instances of integral_wirtingerDbar_mul_inv_sub_eq into one multi-puncture identity — integral_wirtingerDbar_mul_inv_sub_sub_inv_sub_eq below). Proved the same way: transport the convolution-integrability fact already available for cauchyKernel * wirtingerDbar g (p - ·) (HasCompactSupport.convolutionExists_right, the same mathlib fact RS.cauchyPompeiu's own proof relies on) through the measure-preserving substitution w ↦ p - w.

theorem RS.integral_wirtingerDbar_mul_inv_sub_sub_inv_sub_eq {g : ℂ → ℂ} {U : Set ℂ} {a b : ℂ} (hU : IsOpen U) (hg : ContDiffOn ℝ 1 g U) (hcs : HasCompactSupport g) (hsub : tsupport g ⊆ U) : ∫ (w : ℂ), wirtingerDbar g w * ((w - b)⁻¹ - (w - a)⁻¹) = -↑Real.pi * (g b - g a)

The exact two-puncture shape abel-weak-solutions assembles in its Lemma-20.3-specialized step (docs/design/abel-weak-solutions.md §7.3 step 3): the smeared residue identity for f := (·-b)⁻¹ - (·-a)⁻¹ (simple poles of residue +1 at b, -1 at a), matching g b - g a directly, for any C¹ compactly-supported g — no local constancy needed at either puncture, since both poles are simple (the same reasoning as integral_wirtingerDbar_mul_inv_sub_eq). Assembled from two instances of that lemma plus linearity of the Bochner integral (integrable_wirtingerDbar_mul_inv_sub supplies the integrability MeasureTheory.integral_sub needs).