18.5. PlanarStokes.AnnulusResidueMeromorphic🔗

Jacobians.PlanarStokes.AnnulusResidueMeromorphic — source

contDiff_normSq_sub

The shifted squared modulus w ↦ normSq (w − c) is C^∞ (a real polynomial in re/im).

theorem contDiff_normSq_sub (c : ℂ) :
    ContDiff ℝ (⊤ : ℕ∞) (fun w : ℂ => Complex.normSq (w - c))

contDiff_radialCutoff

The complexified radial cutoff χ = η(normSq(·−c)) is globally C¹.

theorem contDiff_radialCutoff {η : ℝ → ℝ} (hη : ContDiff ℝ 1 η) (c : ℂ) :
    ContDiff ℝ 1 (fun w : ℂ => (η (Complex.normSq (w - c)) : ℂ))

mem_ball_of_normSq_le

normSq (z − c) ≤ s₁ < r² puts z in the metric ball ball c r.

theorem mem_ball_of_normSq_le {c z : ℂ} {s₁ r : ℝ} (hr : 0 < r) (hs₁r : s₁ < r ^ 2)
    (hz : Complex.normSq (z - c) ≤ s₁) : z ∈ ball c r

normSq_gt_of_notMem_closedBall

z outside the closed √s₁-ball means normSq (z − c) > s₁.

theorem normSq_gt_of_notMem_closedBall {c z : ℂ} {s₁ : ℝ} (hs₁ : 0 ≤ s₁)
    (hz : z ∉ closedBall c (Real.sqrt s₁)) : s₁ < Complex.normSq (z - c)

eventually_normSq_gt

The region normSq (· − c) > s₁ is open: a strict bound at z holds near z.

theorem eventually_normSq_gt {c z : ℂ} {s₁ : ℝ} (hz : s₁ < Complex.normSq (z - c)) :
    ∀ᶠ w in 𝓝 z, s₁ < Complex.normSq (w - c)

eventually_normSq_lt

The region normSq (· − c) < s₀ is open: a strict bound at z holds near z.

theorem eventually_normSq_lt {c z : ℂ} {s₀ : ℝ} (hz : Complex.normSq (z - c) < s₀) :
    ∀ᶠ w in 𝓝 z, Complex.normSq (w - c) < s₀

radialDeriv_eq_zero_of_lt

Pointwise vanishing of the profile derivative below s₀.

theorem radialDeriv_eq_zero_of_lt {η : ℝ → ℝ} {s₀ : ℝ} (h1 : ∀ s ≤ s₀, η s = 1)
    {c z : ℂ} (hz : Complex.normSq (z - c) < s₀) :
    deriv η (Complex.normSq (z - c)) = 0

radialDeriv_eq_zero_of_gt

Pointwise vanishing of the profile derivative above s₁.

theorem radialDeriv_eq_zero_of_gt {η : ℝ → ℝ} {s₁ : ℝ} (h0 : ∀ s, s₁ ≤ s → η s = 0)
    {c z : ℂ} (hz : s₁ < Complex.normSq (z - c)) :
    deriv η (Complex.normSq (z - c)) = 0

continuous_radialDerivForm

Continuity of η′(normSq(·−c))·F-shaped closed forms. F only needs continuity at the points of the OPEN punctured region 0 < normSq(·−c) < s₂ (s₁ < s₂): below s₀ and above s₁ the profile-derivative factor vanishes identically (0 < s₀, profile 1 → 0), so junk values of F at the centre or far away are killed.

theorem continuous_radialDerivForm {η : ℝ → ℝ} {s₀ s₁ s₂ : ℝ} (hη : ContDiff ℝ 1 η)
    (hs₀ : 0 < s₀) (hs₂ : s₁ < s₂)
    (h1 : ∀ s ≤ s₀, η s = 1) (h0 : ∀ s, s₁ ≤ s → η s = 0) (c : ℂ) {F : ℂ → ℂ}
    (hF : ∀ z : ℂ, z ≠ c → Complex.normSq (z - c) < s₂ → ContinuousAt F z) :
    Continuous fun z : ℂ => Complex.ofReal (deriv η (Complex.normSq (z - c))) * F z

hasCompactSupport_radialDerivForm

Compact support of η′(normSq(·−c))·F-shaped closed forms (support inside the closed √s₁-ball).

theorem hasCompactSupport_radialDerivForm {η : ℝ → ℝ} {s₁ : ℝ}
    (h0 : ∀ s, s₁ ≤ s → η s = 0) (hs₁ : 0 ≤ s₁) (c : ℂ) (F : ℂ → ℂ) :
    HasCompactSupport fun z : ℂ => Complex.ofReal (deriv η (Complex.normSq (z - c))) * F z

analyticAt_negTail_self_punctured

The negTail is analytic at every point OTHER than its centre (each term is a constant times a zpow of (· − c), nonvanishing base).

theorem analyticAt_negTail_self_punctured (c : ℂ) (b : ℕ → ℂ) (N : ℕ) {z : ℂ} (hz : z ≠ c) :
    AnalyticAt ℂ (negTail c b N) z

analyticAt_update_complement

The junk-repaired analytic complement. Given the principal-part split data (exists_principalPart_meromorphicAt), the function G := update (m − P) c (R c) agrees with m − P at every z ≠ c *by definition*, and is analytic on the whole ball ball c r whenever m is analytic on the punctured ball. This upgrades the germ-level split to a pointwise global identity m = P + G off c.

theorem analyticAt_update_complement {N : ℕ} {b : ℕ → ℂ} {R : ℂ → ℂ}
    (hR_an : AnalyticAt ℂ R c)
    (hsplit : m =ᶠ[𝓝[≠] c] fun z => negTail c b N z + R z)
    (hman : ∀ z ∈ ball c r \ {c}, AnalyticAt ℂ m z) :
    ∀ z ∈ ball c r, AnalyticAt ℂ
      (Function.update (fun w => m w - negTail c b N w) c (R c)) z

integral_dbar_radialCutoff_meromorphic

The Forster (10.21) single-pole atom, meromorphic integrand. For a radial C¹ cutoff χ = η(normSq(·−c)) (profile 1 → 0 between s₀ and s₁, 0 < s₀ < s₁) and m meromorphic at c, honestly analytic on a punctured ball of radius r dominating the cutoff (s₁ < r²),

∫_ℂ ∂̄(χ·m) = −π · Res_c m.

Principal-part split + planar Stokes for the complement + the single-power computation.

theorem integral_dbar_radialCutoff_meromorphic (hη : ContDiff ℝ 1 η)
    (hs₀ : 0 < s₀) (hs : s₀ < s₁)
    (h1 : ∀ s ≤ s₀, η s = 1) (h0 : ∀ s, s₁ ≤ s → η s = 0)
    {m : ℂ → ℂ} (hm : MeromorphicAt m c) (hr : 0 < r) (hs₁r : s₁ < r ^ 2)
    (hman : ∀ z ∈ ball c r \ {c}, AnalyticAt ℂ m z) :
    ∫ z : ℂ, DbarDisk.dbar (fun w => (η (Complex.normSq (w - c)) : ℂ) * m w) z
      = -(π : ℂ) * resAt m c

integral_radialDeriv_mul_eq_resAt

The closed-form version of the single-pole atom — the integrand the global ledger transports between charts:

∫_ℂ η′(normSq(z−c)) · (z−c) · m(z) = −π · Res_c m.

Off the centre this is literally ∂̄(χ·m) (Leibniz + holomorphy of m), and the centre is a null set.

theorem integral_radialDeriv_mul_eq_resAt (hη : ContDiff ℝ 1 η)
    (hs₀ : 0 < s₀) (hs : s₀ < s₁)
    (h1 : ∀ s ≤ s₀, η s = 1) (h0 : ∀ s, s₁ ≤ s → η s = 0)
    {m : ℂ → ℂ} (hm : MeromorphicAt m c) (hr : 0 < r) (hs₁r : s₁ < r ^ 2)
    (hman : ∀ z ∈ ball c r \ {c}, AnalyticAt ℂ m z) :
    ∫ z : ℂ, (Complex.ofReal (deriv η (Complex.normSq (z - c))) * (z - c) * m z)
      = -(π : ℂ) * resAt m c