Compat: Leibniz rule, ContDiffOn gluing, and the rectangle ↔ iterated-integral bridge

Unit: planar-stokes-atoms (docs/design/planar-stokes.md §5.1). Mathlib-only (plus Jacobian.Dbar.Wirtinger, D10-compliant, no manifold imports). Three groups of facts:

• The Leibniz rule for wirtingerDbar (wirtingerDbar_mul and its two specializations), not present in Jacobian/Dbar/Wirtinger.lean — proved here exactly as de-risked in the design's spike (scratch_stokes.lean); flagged for upstreaming in docs/requests/dbar-solvability.md.
• ContDiffOn.contDiff_of_hasCompactSupport: the two-piece gluing argument that upgrades a ContDiffOn U function of compact support ⊆ U to a globally ContDiff function.
• The ℂ-rectangle ↔ iterated-real-integral bridge, both as a general (no support hypothesis) internal building block setIntegral_reProdIm_eq_intervalIntegral (reused by AnnulusResidue.lean's Step 3) and as the exported compact-support corollary integral_eq_intervalIntegral_of_tsupport_subset_reProdIm.

The Leibniz rule

theorem RS.wirtingerDbar_mul {g f : ℂ → ℂ} {z : ℂ} (hg : DifferentiableAt ℝ g z) (hf : DifferentiableAt ℝ f z) : wirtingerDbar (fun (w : ℂ) => g w * f w) z = wirtingerDbar g z * f z + g z * wirtingerDbar f z

Leibniz rule for the Wirtinger dbar (requested for upstreaming to Jacobian/Dbar/Wirtinger.lean — see docs/requests/dbar-solvability.md; proved locally here meanwhile, exactly as compiled in the design's spike).

theorem RS.wirtingerDbar_mul_of_differentiableAt {g f : ℂ → ℂ} {z : ℂ} (hg : DifferentiableAt ℝ g z) (hf : DifferentiableAt ℂ f z) : wirtingerDbar (fun (w : ℂ) => g w * f w) z = wirtingerDbar g z * f z

The f-holomorphic specialization: the dbar of a product with a holomorphic factor sees only the other factor's dbar.

theorem RS.wirtingerDbar_mul_eq_zero_of_notMem_tsupport {g f : ℂ → ℂ} {z : ℂ} (hz : z ∉ tsupport g) : wirtingerDbar (fun (w : ℂ) => g w * f w) z = 0

g vanishes identically on a whole neighborhood of any point outside tsupport g, so a product with an arbitrary (possibly non-differentiable/junk) f is still dbar-trivial there.

The ContDiffOn → ContDiff gluing lemma

theorem RS.ContDiffOn.contDiff_of_hasCompactSupport {g : ℂ → ℂ} {U : Set ℂ} {n : ℕ∞} (hU : IsOpen U) (hg : ContDiffOn ℝ (↑n) g U) (_hcs : HasCompactSupport g) (hsub : tsupport g ⊆ U) : ContDiff ℝ (↑n) g

Upgrade a ContDiffOn function with compact support strictly inside an open set to a globally ContDiff function (two-piece gluing: locally g on U, locally 0 on (tsupport g)ᶜ, these two opens cover ℂ).

theorem RS.continuous_wirtingerDbar_of_contDiff_one {g : ℂ → ℂ} (hg : ContDiff ℝ 1 g) : Continuous (wirtingerDbar g)

Continuity of wirtingerDbar g from ContDiff ℝ 1 g alone (Dbar's own continuous_wirtingerDbar needs ContDiff ℝ ∞; this unit only ever has regularity 1 in hand, per D1 — R1 in the design's risk list, resolved by the same two-line argument one level down).

theorem RS.tsupport_wirtingerDbar_subset {g : ℂ → ℂ} : tsupport (wirtingerDbar g) ⊆ tsupport g

tsupport (wirtingerDbar g) ⊆ tsupport g (a sharper, closure-level companion to Dbar's own hasCompactSupport_wirtingerDbar, which only extracts compactness).

The rectangle ↔ iterated-real-integral bridge

theorem RS.setIntegral_reProdIm_eq_intervalIntegral {F : ℂ → ℂ} {z w : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im) (hF : MeasureTheory.IntegrableOn F (Set.Icc z.re w.re ×ℂ Set.Icc z.im w.im) MeasureTheory.volume) : ∫ (ζ : ℂ) in Set.Icc z.re w.re ×ℂ Set.Icc z.im w.im, F ζ = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, F (↑x + ↑y * Complex.I)

Internal building block (no support/vanishing hypothesis): the ℂ-set integral over a closed rectangle equals the iterated real interval integral, given integrability on the rectangle and z.re ≤ w.re, z.im ≤ w.im. Reused both for the exported compact-support corollary below and by AnnulusResidue.lean's Step 3.

theorem RS.integral_eq_intervalIntegral_of_tsupport_subset_reProdIm {F : ℂ → ℂ} {z w : ℂ} (hFc : Continuous F) (hsub : tsupport F ⊆ Set.Ioo z.re w.re ×ℂ Set.Ioo z.im w.im) : ∫ (ζ : ℂ), F ζ = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, F (↑x + ↑y * Complex.I)

The ℂ-rectangle ↔ iterated-real-integral bridge: a function vanishing off an open rectangle has the same global ℂ-integral as its iterated real double integral over (any closed rectangle containing) that open rectangle.