Prove2Me

Continuous Wloc1,pW^{1,p}_{\mathrm{loc}} solutions of ∂ˉf=0\bar\partial f=0 are holomorphic

Proved
JHolomorphic.differentiableOn_of_hasWeakPartialsOn

by Mazecto · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysiselliptic-regularitypseudoholomorphic-curvessobolev-spaces

Let p>2p>2, let U⊂CU\subset\mathbb{C} be open, and let f:U→Cnf:U\to\mathbb{C}^n be continuous on UU. Suppose ff has weak partial derivatives fs,ftf_s,f_t on UU (that is, ∫(∂sφ) f=−∫φ fs\int (\partial_s\varphi)\,f=-\int\varphi\,f_s and ∫(∂tφ) f=−∫φ ft\int(\partial_t\varphi)\,f=-\int\varphi\,f_t for every real C∞C^\infty function φ\varphi with compact support in UU), that f,fs,ft∈Lp(K)f,f_s,f_t\in L^p(K) for every compact K⊂UK\subset U, and that

fs+i ft=0almost everywhere on U.f_s+i\,f_t=0\quad\text{almost everywhere on }U.

Then ff is holomorphic on UU.

This is the weak form of the Cauchy–Riemann equations for Sobolev maps: a continuous Wloc1,pW^{1,p}_{\mathrm{loc}} solution of ∂ˉf=0\bar\partial f=0 is a genuine holomorphic map. It is the step that turns weak solutions of Cauchy–Riemann type equations into holomorphic objects.

Formalization Note Cn\mathbb{C}^n is EuclideanSpace ℂ (Fin n); the weak partials are expressed with JHolomorphic.HasWeakPartialsOn U f fs ft from the imported setting, local LpL^p is MemLp _ (ENNReal.ofReal p) (volume.restrict K) for all compact K ⊆ U, and holomorphy is DifferentiableOn ℂ f U.

Preamble
import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Complex.Conformal
Formal statement
namespace JHolomorphic

open MeasureTheory Metric Filter Topology Set
open scoped ContDiff ENNReal

/-- Let `p > 2` and `U ⊆ ℂ` open. A map `f : U → ℂⁿ` that is continuous on `U`, has weak partial
derivatives `fₛ`, `fₜ` on `U` with `f, fₛ, fₜ ∈ L^p(K)` for every compact `K ⊆ U`, and satisfies
`fₛ + i fₜ = 0` almost everywhere on `U`, is holomorphic on `U`. -/
theorem differentiableOn_of_hasWeakPartialsOn (n : ℕ) (p : ℝ) (hp : 2 < p) {U : Set ℂ}
    (hU : IsOpen U) (f fs ft : ℂ → EuclideanSpace ℂ (Fin n)) (hf : ContinuousOn f U)
    (hw : HasWeakPartialsOn U f fs ft)
    (hLp : ∀ K ⊆ U, IsCompact K →
      MemLp f (ENNReal.ofReal p) (volume.restrict K) ∧
      MemLp fs (ENNReal.ofReal p) (volume.restrict K) ∧
      MemLp ft (ENNReal.ofReal p) (volume.restrict K))
    (heq : ∀ᵐ z ∂(volume.restrict U), fs z + Complex.I • ft z = 0) :
    DifferentiableOn ℂ f U := by
  sorry

end JHolomorphic
Source
Classical (weak Cauchy–Riemann equations); used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Theorem 2.26

View graph