16.8. Dbar.DbarDiskCohomology🔗

Jacobians.Dbar.DbarDiskCohomology — source

dbar_solvable_ball

∂̄-solvability on a ball (full-disk solvability). For g : ℂ → ℂ smooth on all of ℂ and any ball ball c r (r > 0), there is a smooth u : ℂ → ℂ with ∂̄u = g on ball c r.

Proof: take a smooth bump χ with χ.rIn = r, χ.rOut = r + 1, so χ ≡ 1 on the *compact* closedBall c r ⊇ ball c r and χ has compact support. The product χ·g is smooth with compact support, so DbarDisk.dbar_solvable_of_compactSupport gives a global smooth u with ∂̄u = χ·g everywhere; on ball c r the cutoff is 1, so ∂̄u = g there.

Strictly stronger than the local rung DbarLocal.dbar_solvable_locally (it solves on the *whole* ball, not just a neighborhood of the center). The crucial point making this elementary — no exhaustion — is that a bounded ball has *compact* closure, so a single compactly-supported cutoff suffices.

theorem dbar_solvable_ball {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (c : ℂ) {r : ℝ}
    (hr : 0 < r) :
    ∃ u : ℂ → ℂ, ContDiff ℝ (⊤ : ℕ∞) u ∧ ∀ z ∈ Metric.ball c r, DbarDisk.dbar u z = g z

differentiableAt_of_dbar_eq_zero

∂̄ = 0 ⇒ holomorphic (Wirtinger). A function smooth on ℂ whose Wirtinger ∂̄ vanishes at x is complex-differentiable at x. dbar g x = ½((fderiv 1) + I·(fderiv I)) = 0 rearranges to fderiv I = I·(fderiv 1), the Cauchy–Riemann condition of differentiableAt_complex_iff_differentiableAt_real.

theorem differentiableAt_of_dbar_eq_zero {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) {x : ℂ}
    (hdb : DbarDisk.dbar g x = 0) : DifferentiableAt ℂ g x