Weyl's lemma for the conjugate Wirtinger derivative

A locally integrable distributional solution of \bar∂u=0 on an open subset of the plane has an almost-everywhere equal holomorphic representative. The proof first applies the conjugate real first-order operator on test functions to obtain weak harmonicity. The harmonic Weyl theorem supplies smooth representatives of the real and imaginary parts. The weak equation passes to the representative and agrees with the classical Cauchy–Riemann equation there.

Finite-dimensional complex coefficients follow by coordinates. No real weak first derivatives of the original function, or a Sobolev exponent, are assumed.

Main results

• HasWeakConjWirtingerDerivOn.weaklyHarmonicOn: the distributional first-order equation implies weak harmonicity, with arbitrary complex Banach coefficients.
• HasWeakConjWirtingerDerivOn.exists_differentiableOn_ae_eq: Weyl's lemma for finite-dimensional complex coefficients.
• HasWeakConjWirtingerDerivOn.differentiableOn: a continuous solution is itself holomorphic. The converse for holomorphic maps and the elementary conjugation counterexample live in Wirtinger.Weak.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, second edition, Appendix B.

theorem TauCeti.HasWeakConjWirtingerDerivOn.weaklyHarmonicOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u 0) : WeaklyHarmonicOn μ Ω u

A distributional solution of \bar∂u=0 is weakly harmonic, with arbitrary complex Banach coefficients.

theorem TauCeti.HasWeakConjWirtingerDerivOn.exists_differentiableOn_ae_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [FiniteDimensional ℂ F] [μ.IsAddHaarMeasure] (h : HasWeakConjWirtingerDerivOn μ Ω u 0) : ∃ (v : ℂ → F), DifferentiableOn ℂ v ↑Ω ∧ u =ᵐ[μ.restrict ↑Ω] v

Weyl's lemma for \bar∂. A distributional solution with finite-dimensional complex coefficients agrees almost everywhere on its domain with a holomorphic function.

theorem TauCeti.HasWeakConjWirtingerDerivOn.differentiableOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [FiniteDimensional ℂ F] [μ.IsAddHaarMeasure] (h : HasWeakConjWirtingerDerivOn μ Ω u 0) (hu : ContinuousOn u ↑Ω) : DifferentiableOn ℂ u ↑Ω

A continuous distributional solution is itself holomorphic; no representative change is needed.

theorem TauCeti.hasWeakConjWirtingerDerivOn_zero_iff_exists_differentiableOn_ae_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [FiniteDimensional ℂ F] [μ.IsAddHaarMeasure] : HasWeakConjWirtingerDerivOn μ Ω u 0 ↔ ∃ (v : ℂ → F), DifferentiableOn ℂ v ↑Ω ∧ u =ᵐ[μ.restrict ↑Ω] v

The distributional equation is equivalent to existence of an almost-everywhere equal holomorphic representative.

theorem TauCeti.hasWeakConjWirtingerDerivOn_zero_iff_of_continuousOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [FiniteDimensional ℂ F] [μ.IsAddHaarMeasure] (hu : ContinuousOn u ↑Ω) : HasWeakConjWirtingerDerivOn μ Ω u 0 ↔ DifferentiableOn ℂ u ↑Ω

For continuous finite-dimensional complex-valued maps, the distributional equation is precisely holomorphy.