Local solutions of the inhomogeneous Cauchy–Riemann equation

The Cauchy transform gives a right inverse for bar∂ on compactly supported Cⁿ functions into a complex Banach space, for n ≥ 1. Cutting off the source inside an open disc gives a solution on any smaller closed disc, hence near any specified point of an open domain, with the same regularity. This supplies integrating factors for scalar Cauchy–Riemann equations.

The construction uses the right-inverse identity in TauCeti.Analysis.Complex.Pompeiu.Basic, where the transform normalized by (2π)⁻¹ inverts 2 bar∂.

The same construction works for families. Cut off a family f, jointly C^n on s ×ˢ U for an open set U ⊆ ℂ, by a fixed smooth function of the plane variable which equals 1 near a compact set K ⊆ U. Its normalized transform (TauCeti.Analysis.Complex.Pompeiu.Parameter) is a family u, jointly C^n on s ×ˢ univ, with bar∂ (u p) = f p near K for every parameter p ∈ s. The cutoff does not depend on the parameter, so s need not be shrunk, and u is holomorphic in those parameters in which f is. This is the one-variable step of the bar∂-Poincaré lemma on polydiscs, which solves in one conjugate variable while keeping smooth dependence on some of the other variables and holomorphic dependence on the rest.

Main results

• TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eventually_eq: a local solution of bar∂ g = f near a point of the domain of f.
• TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eventually_eq_with_param: local solutions of bar∂ u = f depending smoothly on parameters.
• TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eventually_eq_with_holomorphic_param: local solutions depending smoothly on some parameters and holomorphically on the others.

References

• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990, Chapter I, Theorem 1.2.2.
• P. Griffiths and J. Harris, Principles of Algebraic Geometry, Wiley, 1978, Chapter 0, §§1–2 (the bar∂-Poincaré lemma in one and in several variables, where the solution depends holomorphically on the remaining variables).

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

A compactly supported Cⁿ source, for n ≥ 1, has a global Cⁿ bar∂ primitive.

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

A Cⁿ source on an open disc ball c R, for n ≥ 1, admits a global Cⁿ function whose bar∂ agrees with the source on any smaller closed disc closedBall c r, 0 < r < R.

theorem TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eventually_eq {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {n : ℕ∞} {f : ℂ → W} {U : Set ℂ} (hn : 1 ≤ n) (hU : IsOpen U) (hf : ContDiffOn ℝ (↑n) f U) {z : ℂ} (hz : z ∈ U) : ∃ (g : ℂ → W), ContDiff ℝ (↑n) g ∧ ∀ᶠ (w : ℂ) in nhds z, (conjWirtingerDeriv g w) 1 = f w

A Cⁿ source on an open domain, for n ≥ 1, admits a global Cⁿ function whose bar∂ agrees with the source near any specified point of the domain.

Local solutions of bar∂ u = f with parameters

theorem TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eventually_eq_with_param {n : ℕ∞} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {P : Type u_3} {U K : Set ℂ} [NormedAddCommGroup P] [NormedSpace ℝ P] [CompleteSpace F] {f : P → ℂ → F} {s : Set P} (hn : 1 ≤ n) (hs : IsOpen s) (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) (hf : ContDiffOn ℝ (↑n) (↿f) (s ×ˢ U)) : ∃ (u : P → ℂ → F), ContDiffOn ℝ (↑n) (↿u) (s ×ˢ Set.univ) ∧ ∀ᶠ (z : ℂ) in nhdsSet K, ∀ p ∈ s, (conjWirtingerDeriv (u p) z) 1 = f p z

Local solutions of bar∂ u = f with smooth parameters. Let f be a family of maps ℂ → F which is jointly Cⁿ, 1 ≤ n, on s ×ˢ U for an open set s of parameters and an open set U ⊆ ℂ, and let K ⊆ U be compact. Then some family u, jointly Cⁿ on s ×ˢ univ, satisfies bar∂ (u p) = f p near K for every p ∈ s, on a neighbourhood of K independent of p. No shrinking of the parameter domain is needed.

theorem TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eventually_eq_with_holomorphic_param {n : ℕ∞} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {P : Type u_3} {U K : Set ℂ} [NormedAddCommGroup P] [NormedSpace ℝ P] [CompleteSpace F] {Q : Type u_4} [NormedAddCommGroup Q] [NormedSpace ℂ Q] {f : P × Q → ℂ → F} {s : Set (P × Q)} (hn : 1 ≤ n) (hs : IsOpen s) (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) (hf : ContDiffOn ℝ (↑n) (↿f) (s ×ˢ U)) (hfq : ∀ x ∈ s, ∀ z ∈ U, DifferentiableAt ℂ (fun (q : Q) => f (x.1, q) z) x.2) : ∃ (u : P × Q → ℂ → F), ContDiffOn ℝ (↑n) (↿u) (s ×ˢ Set.univ) ∧ (∀ᶠ (z : ℂ) in nhdsSet K, ∀ x ∈ s, (conjWirtingerDeriv (u x) z) 1 = f x z) ∧ ∀ x ∈ s, ∀ (w : ℂ), DifferentiableAt ℂ (fun (q : Q) => u (x.1, q) w) x.2

Local solutions of bar∂ u = f with smooth and holomorphic parameters. Let f be a family of maps ℂ → F indexed by P × Q, for a real normed space P and a complex normed space Q, which is jointly Cⁿ, 1 ≤ n, on s ×ˢ U for an open set s ⊆ P × Q and an open set U ⊆ ℂ, and holomorphic in q ∈ Q at every point of s ×ˢ U. Let K ⊆ U be compact. Then some family u, jointly Cⁿ on s ×ˢ univ, satisfies bar∂ (u x) = f x near K for every x ∈ s, on a neighbourhood of K independent of x, and is holomorphic in q on s at every point of the plane.