16.9. Dbar.DbarLocal🔗

Jacobians.Dbar.DbarLocal — source

contDiffBump_eq_one_on_ball

The smooth cutoff χ is 1 on the open inner ball Metric.ball z₀ χ.rIn (not just on the closed ball), since ball ⊆ closedBall and ContDiffBump.one_of_mem_closedBall.

theorem contDiffBump_eq_one_on_ball {z₀ z : ℂ} (χ : ContDiffBump z₀)
    (hz : z ∈ Metric.ball z₀ χ.rIn) : (χ : ℂ → ℝ) z = 1

contDiff_hasCompactSupport_ofReal_contDiffBump

The ℝ→ℂ coercion of a smooth compactly-supported cutoff χ : ContDiffBump z₀ is itself a smooth, compactly-supported function ℂ → ℂ. Returned as a conjunction so callers get both facts from one cutoff.

theorem contDiff_hasCompactSupport_ofReal_contDiffBump {z₀ : ℂ} (χ : ContDiffBump z₀) :
    ContDiff ℝ (⊤ : ℕ∞) (fun z => ((χ z : ℝ) : ℂ)) ∧
      HasCompactSupport (fun z => ((χ z : ℝ) : ℂ))

dbar_solvable_locally

Local ∂̄-solvability (the first Dolbeault rung). Any smooth g : ℂ → ℂ can be ∂̄-solved on an open neighborhood V of an arbitrary point z₀: there is a smooth u with ∂̄u = g on V.

Proof: cut off g by a smooth bump χ that is 1 near z₀ and compactly supported, solve the compactly-supported equation ∂̄u = χ·g everywhere via DbarDisk.dbar_solvable_of_compactSupport, and observe χ·g = g on the inner ball V where χ ≡ 1.

theorem dbar_solvable_locally {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (z₀ : ℂ) :
    ∃ (V : Set ℂ) (u : ℂ → ℂ), IsOpen V ∧ z₀ ∈ V ∧ ContDiff ℝ (⊤ : ℕ∞) u ∧
      ∀ z ∈ V, DbarDisk.dbar u z = g z