18.4. PlanarStokes.AnnulusResidueIntegral🔗

Jacobians.PlanarStokes.AnnulusResidueIntegral — source

dbar_congr

∂̄ only depends on the germ: functions agreeing near z have equal ∂̄ at z.

theorem dbar_congr {f g : ℂ → ℂ} {z : ℂ} (h : f =ᶠ[𝓝 z] g) : dbar f z = dbar g z

dbar_fun_add

Additivity of ∂̄ at a common point of real differentiability.

theorem dbar_fun_add {f g : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z)
    (hg : DifferentiableAt ℝ g z) :
    dbar (fun w => f w + g w) z = dbar f z + dbar g z

dbar_fun_sub

Subtraction rule for ∂̄ at a common point of real differentiability.

theorem dbar_fun_sub {f g : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z)
    (hg : DifferentiableAt ℝ g z) :
    dbar (fun w => f w - g w) z = dbar f z - dbar g z

dbar_fun_sum

Finite sums commute with ∂̄ at a common point of real differentiability.

theorem dbar_fun_sum {ι : Type*} {s : Finset ι} {f : ι → ℂ → ℂ} {z : ℂ}
    (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) z) :
    dbar (fun w => ∑ i ∈ s, f i w) z = ∑ i ∈ s, dbar (f i) z

dbar_fun_mul

Wirtinger–Leibniz product rule: ∂̄(f·g) = f·∂̄g + g·∂̄f at a common point of real differentiability (∂̄ is a derivation, like each directional fderiv ℝ).

theorem dbar_fun_mul {f g : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z)
    (hg : DifferentiableAt ℝ g z) :
    dbar (fun w => f w * g w) z = f z * dbar g z + g z * dbar f z

dbar_fun_const_mul

Constants scale through ∂̄ at points of real differentiability.

theorem dbar_fun_const_mul (a : ℂ) {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z) :
    dbar (fun w => a * f w) z = a * dbar f z

continuousAt_dbar_of_contDiffAt

∂̄ of a C¹ function is continuous at points of C¹-ness (local statement: only ContDiffAt ℝ 1 is assumed, which yields a neighbourhood on which fderiv ℝ is continuous).

theorem continuousAt_dbar_of_contDiffAt {f : ℂ → ℂ} {z : ℂ} (hf : ContDiffAt ℝ 1 f z) :
    ContinuousAt (dbar f) z

hasFDerivAt_normSq_sub

The shifted squared modulus w ↦ normSq (w − c) is real-differentiable, with derivative v ↦ 2((z−c).re·v.re + (z−c).im·v.im) (assembled from reCLM/imCLM).

theorem hasFDerivAt_normSq_sub (c z : ℂ) :
    HasFDerivAt (fun w : ℂ => Complex.normSq (w - c))
      ((z - c).re • (Complex.reCLM : ℂ →L[ℝ] ℝ) + (z - c).re • (Complex.reCLM : ℂ →L[ℝ] ℝ)
        + ((z - c).im • (Complex.imCLM : ℂ →L[ℝ] ℝ)
          + (z - c).im • (Complex.imCLM : ℂ →L[ℝ] ℝ))) z

dbar_comp_normSq

∂̄ of a complexified radial profile: ∂̄(η ∘ normSq(·−c))(z) = η'(normSq(z−c))·(z−c). Valid at every z (no puncture needed): normSq is polynomial.

theorem dbar_comp_normSq {η : ℝ → ℝ} (hη : ContDiff ℝ 1 η) (c z : ℂ) :
    DbarDisk.dbar (fun w => (η (Complex.normSq (w - c)) : ℂ)) z
      = Complex.ofReal (deriv η (Complex.normSq (z - c))) * (z - c)

differentiableAt_comp_normSq

The radial profile is real-differentiable at every point (needed as a DifferentiableAt ℝ input to the Leibniz rule).

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

deriv_profile_eq_zero_left

The derivative of a profile that is constant 1 on (-∞, s₀] vanishes on the open ray (-∞, s₀) (local constancy).

theorem deriv_profile_eq_zero_left {η : ℝ → ℝ} {s₀ : ℝ} (h1 : ∀ s ≤ s₀, η s = 1)
    {s : ℝ} (hs : s < s₀) : deriv η s = 0

deriv_profile_eq_zero_right

The derivative of a profile that is constant 0 on [s₁, ∞) vanishes on the open ray (s₁, ∞) (local constancy).

theorem deriv_profile_eq_zero_right {η : ℝ → ℝ} {s₁ : ℝ} (h0 : ∀ s, s₁ ≤ s → η s = 0)
    {s : ℝ} (hs : s₁ < s) : deriv η s = 0

differentiableAt_zpow_sub

(w − c)^n is holomorphic off c.

theorem differentiableAt_zpow_sub (c : ℂ) (n : ℤ) {z : ℂ} (hz : z ≠ c) :
    DifferentiableAt ℂ (fun w => (w - c) ^ n) z

holoPunctured_const_mul_zpow

Scaled negative powers of (· − c) have isolated singularities at c.

theorem holoPunctured_const_mul_zpow (a c : ℂ) (n : ℤ) :
    HoloPunctured (fun z => a * (z - c) ^ n) c

HoloPunctured.add

HoloPunctured is closed under pointwise addition (intersect the two punctured balls).

theorem HoloPunctured.add {f g : ℂ → ℂ} {c : ℂ} (hf : HoloPunctured f c)
    (hg : HoloPunctured g c) : HoloPunctured (fun z => f z + g z) c

holoPunctured_finset_sum

HoloPunctured is closed under finite sums.

theorem holoPunctured_finset_sum {ι : Type*} (s : Finset ι) (f : ι → ℂ → ℂ) {c : ℂ}
    (hf : ∀ i ∈ s, HoloPunctured (f i) c) :
    HoloPunctured (fun z => ∑ i ∈ s, f i z) c

resAt_finset_sum

resAt of a finite sum of functions with isolated singularities.

theorem resAt_finset_sum {ι : Type*} (s : Finset ι) (f : ι → ℂ → ℂ) {c : ℂ}
    (hf : ∀ i ∈ s, HoloPunctured (f i) c) :
    resAt (fun z => ∑ i ∈ s, f i z) c = ∑ i ∈ s, resAt (f i) c

resAt_zpow_neg_of_ne

Res_c((·−c)^{−k}) = 0 for k ≠ 1 (all small contour integrals vanish: circleIntegral.integral_sub_zpow_of_ne).

theorem resAt_zpow_neg_of_ne {c : ℂ} {k : ℕ} (hk : k ≠ 1) :
    resAt (fun z => (z - c) ^ (-(k : ℤ))) c = 0

resAt_zpow_neg_one

Res_c((·−c)^{−1}) = 1 (the zpow phrasing of resAt_sub_inv).

theorem resAt_zpow_neg_one (c : ℂ) :
    resAt (fun z => (z - c) ^ (-(1 : ℕ) : ℤ)) c = 1

resAt_const_mul_zpow_neg

resAt of a single principal-part term: Res_c(b·(·−c)^{−k}) = b·δ_{k,1}.

theorem resAt_const_mul_zpow_neg (b c : ℂ) (k : ℕ) :
    resAt (fun z => b * (z - c) ^ (-(k : ℤ))) c = b * (if k = 1 then 1 else 0)

dbar_radialProfile_mul_zpow

Pointwise closed form off the centre: ∂̄(η(normSq(·−c))·(·−c)^n)(z) = η'(normSq(z−c))·(z−c)^{n+1} for z ≠ c.

theorem dbar_radialProfile_mul_zpow {η : ℝ → ℝ} (hη : ContDiff ℝ 1 η) (c : ℂ) (n : ℤ)
    {z : ℂ} (hz : z ≠ c) :
    DbarDisk.dbar (fun w => (η (Complex.normSq (w - c)) : ℂ) * (w - c) ^ n) z
      = Complex.ofReal (deriv η (Complex.normSq (z - c))) * (z - c) ^ (n + 1)

integral_rmul_deriv_profile

The radial FTC integral: ∫_0^∞ r·η'(r²) dr = ½(η(∞) − η(0)) = −½ for a profile going 1 → 0. (η' has compact support, so the improper integral is honest.)

theorem integral_rmul_deriv_profile {η : ℝ → ℝ} {s₀ s₁ : ℝ} (hη : ContDiff ℝ 1 η)
    (hs₀ : 0 < s₀) (hs : s₀ < s₁) (h1 : ∀ s ≤ s₀, η s = 1) (h0 : ∀ s, s₁ ≤ s → η s = 0) :
    ∫ r in Ioi (0 : ℝ), r * deriv η (r ^ 2) = -(1 / 2)

integral_Ioo_exp_mul_I_zpow

The angular integral ∫_{−π}^{π} (e^{iθ})^m dθ vanishes for m ≠ 0: FTC with antiderivative e^{imθ}/(im), and e^{±imπ} = (−1)^m agree.

theorem integral_Ioo_exp_mul_I_zpow {m : ℤ} (hm : m ≠ 0) :
    ∫ θ in Ioo (-π) π, Complex.exp (θ * Complex.I) ^ m = 0

integral_Ioo_one_complex

The angular integral for m = 0: ∫_{−π}^{π} 1 dθ = 2π.

theorem integral_Ioo_one_complex :
    ∫ _ in Ioo (-π) π, (1 : ℂ) = ((2 * π : ℝ) : ℂ)

integral_dbar_radialCutoff_zpow

The Forster (10.21) single-term computation. For the radial cutoff χ = η(normSq(·−c)) (profile 1 → 0 between s₀ and s₁),

∫_ℂ ∂̄(χ·(·−c)^{−k}) = −π·δ_{k,1}.

Off c the integrand is η'(normSq(z−c))·(z−c)^{1−k} (supported in the closed annulus s₀ ≤ normSq(z−c) ≤ s₁); in polar coordinates it separates into the radial FTC factor and the angular character integral.

theorem integral_dbar_radialCutoff_zpow (c : ℂ) {η : ℝ → ℝ} {s₀ s₁ : ℝ} (hη : ContDiff ℝ 1 η)
    (hs₀ : 0 < s₀) (hs : s₀ < s₁) (h1 : ∀ s ≤ s₀, η s = 1) (h0 : ∀ s, s₁ ≤ s → η s = 0)
    (k : ℕ) :
    ∫ z : ℂ, DbarDisk.dbar
        (fun w => (η (Complex.normSq (w - c)) : ℂ) * (w - c) ^ (-(k : ℤ))) z
      = if k = 1 then -(π : ℂ) else 0