Forster 13.2: Dolbeault's lemma on an open disk (Jacobian/Dbar/SolveDisk.lean)

Unit: dbar-solvability (docs/design/dbar-solvability.md §4.3, §6). Mathlib-only planar file.

The main theorem exists_dbar_solution_ball solves dbaru = g on a finite open disk for g smooth there, by an exhaustion + correction sequence: solve dbarfₙ = g on shrinking closed sub-balls via cauchyTransform of a cutoff of g (13.1), then correct each fₙ by a partial sum of the power series of the (holomorphic) difference f_{n+1} - fₙ, chosen small enough that the corrected sequence converges locally uniformly to a solution on the whole disk.

theorem RS.contDiff_indicator_bump_smul (g : ℂ → ℂ) (c : ℂ) {s : Set ℂ} (φ : ContDiffBump c) (hs : IsOpen s) (hg : ContDiffOn ℝ (↑⊤) g s) (hsub : Metric.closedBall c φ.rOut ⊆ s) : ContDiff ℝ (↑⊤) (s.indicator fun (z : ℂ) => ↑φ z • g z)

Extension by zero of a bump-cutoff of a function smooth on an open set: the cutoff s.indicator (φ • g) is smooth everywhere, provided φ's (closed) support stays inside s.

theorem RS.hasCompactSupport_indicator_bump_smul (g : ℂ → ℂ) (c : ℂ) {s : Set ℂ} (φ : ContDiffBump c) : HasCompactSupport (s.indicator fun (z : ℂ) => ↑φ z • g z)

theorem RS.eqOn_indicator_bump_smul (g : ℂ → ℂ) (c : ℂ) {s : Set ℂ} (φ : ContDiffBump c) (hsub : Metric.closedBall c φ.rOut ⊆ s) : Set.EqOn (s.indicator fun (z : ℂ) => ↑φ z • g z) (fun (z : ℂ) => ↑φ z • g z) (Metric.closedBall c φ.rIn)

The exhaustion radii ρ n = R - R/(n+2)

The cutoff bumps and cutoff functions

The raw (uncorrected) solutions on shrinking sub-balls

The corrected sequence: a Nat.rec into a Σ-type carrying invariants (i), (ii); the

correction bound (iii) is proved once, as a property of the step function itself.

theorem RS.exists_dbar_solution_ball (g : ℂ → ℂ) (c : ℂ) (R : ℝ) (hR : 0 < R) (hg : ContDiffOn ℝ (↑⊤) g (Metric.ball c R)) : ∃ (u : ℂ → ℂ), ContDiffOn ℝ (↑⊤) u (Metric.ball c R) ∧ ∀ z ∈ Metric.ball c R, wirtingerDbar u z = g z

Forster 13.2: Dolbeault's lemma on a finite open disk.