The Dolbeault lemma on discs

Let D ⊆ ℂ be an open disc of radius R ≤ ∞ and let f : ℂ → W be Cⁿ on D, for n ≥ 1, with values in a complex Banach space. Then the inhomogeneous Cauchy–Riemann equation \bar∂ g = f has a Cⁿ solution g on all of D. Here \bar∂ g is the conjugate Wirtinger derivative TauCeti.conjWirtingerDeriv g z 1 = (∂ₓ g + i ∂ᵧ g) / 2.

For compactly supported f the Cauchy transform solves the equation on the whole plane (TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eq_of_hasCompactSupport); cutting f off gives a solution h k on each disc of an exhaustion of D by concentric discs B k (TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eq_on_closedBall). These local solutions do not converge, but consecutive ones differ by a function h (k + 1) - h k that is holomorphic on a neighbourhood of the closure of B k. An entire function P k, a partial sum of the Taylor series of that difference, approximates it within 2⁻ᵏ on B k (DifferentiableOn.exists_differentiable_norm_sub_lt). The corrected solutions h k - ∑_{j < k} P j then converge locally uniformly on D: on B m the limit is h m plus a locally uniform limit of holomorphic functions, so it is Cⁿ and has the same \bar∂ as h m, namely f.

This is the local \bar∂-lemma behind the vanishing of H¹(D, 𝒪) on discs, which makes discs acyclic for the structure sheaf of a Riemann surface.

Main results

• TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_eball: the Dolbeault lemma on a disc Metric.eball c R, R ≤ ∞.
• TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_ball: the same for a disc of real radius.
• TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eq: every Cⁿ function on the plane is \bar∂ of a Cⁿ function, without any support condition.

References

• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, Lemma 13.1 and Theorem 13.2 (Dolbeault's lemma).
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990, Theorem 1.4.4.

theorem TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_eball {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {n : ℕ∞} {f : ℂ → W} {c : ℂ} {R : ENNReal} (hn : 1 ≤ n) (hf : ContDiffOn ℝ (↑n) f (Metric.eball c R)) : ∃ (g : ℂ → W), ContDiffOn ℝ (↑n) g (Metric.eball c R) ∧ ∀ z ∈ Metric.eball c R, (conjWirtingerDeriv g z) 1 = f z

The Dolbeault lemma on a disc. Let f be Cⁿ, n ≥ 1, on the open disc eball c R of radius R ≤ ∞. Then there is a function g, Cⁿ on the disc, with \bar∂ g = f on the disc.

theorem TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_ball {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {n : ℕ∞} {f : ℂ → W} {c : ℂ} {R : ℝ} (hn : 1 ≤ n) (hf : ContDiffOn ℝ (↑n) f (Metric.ball c R)) : ∃ (g : ℂ → W), ContDiffOn ℝ (↑n) g (Metric.ball c R) ∧ ∀ z ∈ Metric.ball c R, (conjWirtingerDeriv g z) 1 = f z

The Dolbeault lemma on a disc of real radius. If f is Cⁿ, n ≥ 1, on ball c R, there is a function g, Cⁿ on ball c R, with \bar∂ g = f there.

theorem TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eq {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {n : ℕ∞} {f : ℂ → W} (hn : 1 ≤ n) (hf : ContDiff ℝ (↑n) f) : ∃ (g : ℂ → W), ContDiff ℝ (↑n) g ∧ ∀ (z : ℂ), (conjWirtingerDeriv g z) 1 = f z

The Dolbeault lemma on the plane. Every Cⁿ function f : ℂ → W, n ≥ 1, is \bar∂ g for a Cⁿ function g; no support condition on f is needed.