16.4. Dbar.CechDiskAcyclic🔗

Jacobians.Dbar.CechDiskAcyclic — source

dbarFun_add

∂̄ is additive at a point where both summands are real-differentiable.

theorem dbarFun_add {f g : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z)
    (hg : DifferentiableAt ℝ g z) :
    DbarDisk.dbar (fun x => f x + g x) z = DbarDisk.dbar f z + DbarDisk.dbar g z

dbarFun_sub

∂̄ is subtractive at a point where both functions are real-differentiable.

theorem dbarFun_sub {f g : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z)
    (hg : DifferentiableAt ℝ g z) :
    DbarDisk.dbar (fun x => f x - g x) z = DbarDisk.dbar f z - DbarDisk.dbar g z