25.7. AbelWeak.AbelPlanarPiece🔗

Jacobians.AbelWeak.AbelPlanarPiece — source

del

The Wirtinger holomorphic derivative ∂f = ½(∂ₓf − i·∂_yf), via the real Fréchet derivative at the basis directions 1, I (conjugate partner of DbarDisk.dbar).

def del (f : ℂ → ℂ) (z : ℂ) : ℂ

del_congr

∂ only depends on the germ.

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

del_eq_deriv_of_differentiableAt

∂ of a holomorphic function is its complex derivative (the Wirtinger split of the Cauchy–Riemann equations; companion of dbar_eq_zero_of_differentiableAt).

theorem del_eq_deriv_of_differentiableAt {f : ℂ → ℂ} {z : ℂ}
    (hf : DifferentiableAt ℂ f z) : del f z = deriv f z

del_fun_mul

Wirtinger–Leibniz product rule for ∂.

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

dbar_fun_inv

∂̄ of a pointwise inverse: ∂̄(f⁻¹) = −f⁻²·∂̄f at points where f ≠ 0.

theorem dbar_fun_inv {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z) (h0 : f z ≠ 0) :
    dbar (fun w => (f w)⁻¹) z = -((f z) ^ 2)⁻¹ * dbar f z

del_fun_inv

∂ of a pointwise inverse: ∂(f⁻¹) = −f⁻²·∂f at points where f ≠ 0.

theorem del_fun_inv {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z) (h0 : f z ≠ 0) :
    del (fun w => (f w)⁻¹) z = -((f z) ^ 2)⁻¹ * del f z

contDiff_fderiv_apply

The directional Fréchet read z ↦ (fderiv ℝ f z) v of a C^∞ function is C^∞.

theorem contDiff_fderiv_apply {f : ℂ → ℂ} (hf : ContDiff ℝ (⊤ : ℕ∞) f) (v : ℂ) :
    ContDiff ℝ (⊤ : ℕ∞) (fun z => fderiv ℝ f z v)

contDiff_dbar

∂̄f is C^∞ for C^∞ f.

theorem contDiff_dbar {f : ℂ → ℂ} (hf : ContDiff ℝ (⊤ : ℕ∞) f) :
    ContDiff ℝ (⊤ : ℕ∞) (dbar f)

contDiff_del

∂f is C^∞ for C^∞ f.

theorem contDiff_del {f : ℂ → ℂ} (hf : ContDiff ℝ (⊤ : ℕ∞) f) :
    ContDiff ℝ (⊤ : ℕ∞) (del f)

hasCompactSupport_del

∂f inherits compact support from f (companion of hasCompactSupport_dbar).

theorem hasCompactSupport_del {f : ℂ → ℂ} (hf : HasCompactSupport f) :
    HasCompactSupport (del f)

dbar_del_eq_del_dbar

∂̄∂f = ∂∂̄f for C^∞ f (symmetry of the second Fréchet derivative read in the Wirtinger frame).

theorem dbar_del_eq_del_dbar {f : ℂ → ℂ} (hf : ContDiff ℝ (⊤ : ℕ∞) f) (z : ℂ) :
    dbar (del f) z = del (dbar f) z

integral_del_eq_zero

∫_ℂ ∂φ = 0 for C¹ compactly-supported φ (named-del form of Jacobians.Dolbeault.integral_del_eq_zero).

theorem integral_del_eq_zero {φ : ℂ → ℂ} (hφ : ContDiff ℝ 1 φ)
    (hsupp : HasCompactSupport φ) : ∫ z, del φ z = 0

integral_dbar_eq_zero

∫_ℂ ∂̄φ = 0 for C¹ compactly-supported φ (re-export of the PlanarCompactSupportStokes atom in the dbar spelling).

theorem integral_dbar_eq_zero {φ : ℂ → ℂ} (hφ : ContDiff ℝ 1 φ)
    (hsupp : HasCompactSupport φ) : ∫ z, dbar φ z = 0

integral_logDeriv_cross_eq_zero

The 20.3 cross-term Stokes identity: for smooth nonvanishing W and G ∈ C_c^∞(ℂ),

∫_ℂ (∂W/W·∂̄G − ∂̄W/W·∂G) dA = 0.

This is ∬_ℂ d(G·dW/W) = 0 read in Wirtinger coordinates: expand ∫∂̄(G·∂W/W) = 0 and ∫∂(G·∂̄W/W) = 0 (compact-support Stokes) and cancel the mixed second Wirtinger derivatives of W (dbar_del_eq_del_dbar).

theorem integral_logDeriv_cross_eq_zero {W G : ℂ → ℂ}
    (hW : ContDiff ℝ (⊤ : ℕ∞) W) (hW0 : ∀ z, W z ≠ 0)
    (hG : ContDiff ℝ (⊤ : ℕ∞) G) (hGsupp : HasCompactSupport G) :
    ∫ z, (del W z / W z * dbar G z - dbar W z / W z * del G z) = 0

integrable_dbar_mul_inv

The pole pairing integrand ∂̄G·(z − a)⁻¹ is integrable for G ∈ C_c^∞ (transport of DbarDisk.integrable_dbar_mul_cauchyKernel).

theorem integrable_dbar_mul_inv {G : ℂ → ℂ} (hG : ContDiff ℝ (⊤ : ℕ∞) G)
    (hGsupp : HasCompactSupport G) (a : ℂ) :
    Integrable (fun z => dbar G z * (z - a)⁻¹) volume

integral_dbar_mul_inv_sub

The two-pole Cauchy–Pompeiu pairing (the residue half of Forster 20.3):

∫_ℂ ∂̄G·((z−α)⁻¹ − (z−β)⁻¹) dA = π·(G β − G α) for G ∈ C_c^∞(ℂ).

theorem integral_dbar_mul_inv_sub {G : ℂ → ℂ} (hG : ContDiff ℝ (⊤ : ℕ∞) G)
    (hGsupp : HasCompactSupport G) (α β : ℂ) :
    ∫ z, dbar G z * ((z - α)⁻¹ - (z - β)⁻¹) = (π : ℂ) * (G β - G α)

PlanarPieceSolution

Planar piece-solution data (Forster 20.5(a), normalized): a smooth nonvanishing cofactor W with W ≡ 1 inside and W = (z−α)/(z−β) outside; the per-piece weak solution is F = W·(z−β)/(z−α) and its global ∂̄-datum is U = ∂̄W/W.

structure PlanarPieceSolution (c₀ : ℂ) (ρ : ℝ) (α β : ℂ) where

F

The piece solution F = W·(z−β)/(z−α): simple zero at β, simple pole at α (junk-normalized to 0 at α), ≡ 1 outside ball c₀ (5ρ).

def F : ℂ → ℂ

U

The ∂̄-datum U = ∂̄W/W of the piece solution (equal to ∂̄F/F away from α, β, smooth everywhere).

def U : ℂ → ℂ

U_smooth

theorem U_smooth : ContDiff ℝ (⊤ : ℕ∞) S.U

U_continuous

theorem U_continuous : Continuous S.U

U_eq_zero_inner

U vanishes on the inner ball (W ≡ 1 there).

theorem U_eq_zero_inner {z : ℂ} (hz : dist z c₀ < 4 * ρ) : S.U z = 0

U_eq_zero_outer

U vanishes outside closedBall c₀ (5ρ) (W is holomorphic there).

theorem U_eq_zero_outer {z : ℂ} (hz : 5 * ρ < dist z c₀) : S.U z = 0

dist_mem_of_U_ne_zero

The support window of U: nonvanishing forces 4ρ ≤ dist z c₀ ≤ 5ρ.

theorem dist_mem_of_U_ne_zero {z : ℂ} (hz : S.U z ≠ 0) :
    4 * ρ ≤ dist z c₀ ∧ dist z c₀ ≤ 5 * ρ

U_hasCompactSupport

U has compact support (inside closedBall c₀ (5ρ)).

theorem U_hasCompactSupport : HasCompactSupport S.U

F_eq_one_outer

Outside ball c₀ (5ρ) the piece solution is ≡ 1.

theorem F_eq_one_outer {z : ℂ} (hz : 5 * ρ < dist z c₀) : S.F z = 1

F_ne_zero

The piece solution is nonvanishing away from the two endpoints.

theorem F_ne_zero {z : ℂ} (hzα : z ≠ α) (hzβ : z ≠ β) : S.F z ≠ 0

integral_U_mul

The planar piece identity (Forster 20.3 + 20.5(a) for holomorphic test data): if g is a primitive of h on ball c₀ (8ρ), then

∫_ℂ U·h dA = π·(g β − g α).

In Forster's notation this is (1/2πi)∬ (df₀/f₀)∧ω = ∫_c ω for ω = h·dz = dg: (df₀/f₀)∧(h dz) = U·h·dz̄∧dz = 2i·U·h·dA, so ∬(df₀/f₀)∧ω = 2i·π·(g β − g α) matches 2πi·(g(b) − g(a)) exactly.

theorem integral_U_mul {g h : ℂ → ℂ}
    (hg : ∀ z ∈ ball c₀ (8 * ρ), HasDerivAt g (h z) z) :
    ∫ z, S.U z * h z = (π : ℂ) * (g β - g α)

nonempty_planarPieceSolution

Planar piece solutions exist for any endpoints α, β ∈ ball c₀ ρ (Forster 20.5(a): bump times the principal branch of log((z−β)/(z−α))).

theorem nonempty_planarPieceSolution {c₀ α β : ℂ} {ρ : ℝ} (hρ : 0 < ρ)
    (hα : dist α c₀ < ρ) (hβ : dist β c₀ < ρ) :
    Nonempty (PlanarPieceSolution c₀ ρ α β)