Weakly holomorphic integrable functions are holomorphic

Proved

JHolomorphic.ae_eq_differentiableOn_of_weak_dbar_eq_zero

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

elliptic-regularitypseudoholomorphic-curvessobolev-spacessymplectic-geometryunique-continuation

Let $D\subset\mathbb{C}$ be the open unit disc and let $u\in L^1(D,\mathbb{C}^n)$ satisfy $\partial_su+i\,\partial_tu=0$ in the sense of distributions:

\int\big((\partial_s\varphi)\,u+(\partial_t\varphi)\,i\,u\big)=0

for every real $C^\infty$ function $\varphi$ with compact support in $D$ . Then $u$ agrees almost everywhere on $D$ with a holomorphic function $v:D\to\mathbb{C}^n$ .

Formalization Note $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n). Integrability is IntegrableOn u (ball 0 1); holomorphy is DifferentiableOn ℂ v (ball 0 1) and the agreement is u =ᵐ[volume.restrict (ball 0 1)] v.

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology DbarRegularity
open scoped ContDiff ENNReal NNReal

/-- Wendl, Lemma 2.19 (p. 35): an integrable `u` on the open unit disc that satisfies `∂̄u = 0` in
the sense of distributions, i.e. `∫ (∂ₛφ) u + (∂ₜφ) i u = 0` for every real `C^∞` function `φ`
with compact support in the disc, agrees almost everywhere with a holomorphic function. -/
theorem ae_eq_differentiableOn_of_weak_dbar_eq_zero (n : ℕ)
    (u : ℂ → EuclideanSpace ℂ (Fin n)) (hu : IntegrableOn u (ball 0 1))
    (hweak : ∀ φ : ℂ → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ → tsupport φ ⊆ ball 0 1 →
      ∫ z, (fderiv ℝ φ z 1 • u z + fderiv ℝ φ z Complex.I • (Complex.I • u z)) = 0) :
    ∃ v : ℂ → EuclideanSpace ℂ (Fin n), DifferentiableOn ℂ v (ball 0 1) ∧
      u =ᵐ[volume.restrict (ball 0 1)] v := by
  sorry

end JHolomorphic

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 2, Lemma 2.19, p. 35

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

`JHolomorphic.ae_eq_differentiableOn_of_weak_dbar_eq_zero`

Setting and data. Let $n \in \mathbb{N}$ be arbitrary (including $n = 0$ ). Let $D = \{z \in \mathbb{C} : |z| < 1\}$ denote the open unit disc in $\mathbb{C}$ , and let $\lambda$ be Lebesgue measure on $\mathbb{C} \cong \mathbb{R}^2$ . Let

u : \mathbb{C} \to \mathbb{C}^n

be a function, where $\mathbb{C}^n$ carries its Euclidean (Hermitian $\ell^2$ ) norm. No other structure is assumed on $u$ (no continuity, no measurability outside $D$ , no condition on its values outside $D$ ).

Hypothesis 1 (integrability on the disc). $u$ is Lebesgue integrable on $D$ : its restriction to $D$ is almost-everywhere strongly measurable with respect to $\lambda|_D$ and

\int_D |u(z)|\, d\lambda(z) < \infty .

Hypothesis 2 (integral identity against test functions). For every real-valued function $\varphi : \mathbb{C} \to \mathbb{R}$ such that

$\varphi$ is $C^\infty$ as a function of two real variables,
$\varphi$ has compact support, and
the closed support $\overline{\{\varphi \neq 0\}}$ is contained in the open disc $D$ ,

one has

\int_{\mathbb{C}} \Big( \partial_x \varphi(z)\, u(z) \;+\; \partial_y \varphi(z)\, \big(i\, u(z)\big) \Big)\, d\lambda(z) \;=\; 0 \quad\text{in } \mathbb{C}^n,

where, writing $z = x + i y$ , $\partial_x \varphi(z)$ is the real Fréchet derivative of $\varphi$ at $z$ applied to the direction $1$ , and $\partial_y \varphi(z)$ is that derivative applied to the direction $i$ ; these real numbers multiply the vectors $u(z)$ and $i\,u(z)$ (componentwise multiplication by $i$ ) in $\mathbb{C}^n$ . The integral is a Bochner integral over all of $\mathbb{C}$ ; by convention it takes the value $0$ whenever the integrand is not integrable, in which case the identity holds automatically for that $\varphi$ . (Since $\varphi$ is smooth with support in a compact subset of $D$ , its derivatives vanish outside that compact set and are bounded, so together with Hypothesis 1 the integrand is in fact integrable; the convention does not create extra vacuous cases for such $\varphi$ .)

Conclusion. There exists a function $v : \mathbb{C} \to \mathbb{C}^n$ such that

$v$ is complex-differentiable (holomorphic, componentwise) at every point of the open disc $D$ — stated as complex differentiability of $v$ within $D$ at each point of $D$ , which, $D$ being open, is ordinary complex differentiability at each point of $D$ ; and
$u = v$ almost everywhere on $D$ , i.e.

\lambda\big(\{ z \in D : u(z) \neq v(z) \}\big) = 0 .

Nothing is asserted about $v$ outside $D$ , and nothing is asserted about $u$ outside $D$ .

Remarks on the code. The statement uses none of the definitions from the imported setting files (IsAlmostComplexOn, dbarJ, IsJHolomorphicOn, HasWeakPartialsOn, IsWeakJHolomorphicOn, TendstoCInftyLocOn, dbar, maximalFunction, closedCube, sobolevNorm are not referenced); every condition above is written out directly in terms of Fréchet derivatives, Lebesgue integrals and the disc. Degenerate case: for $n = 0$ the target space $\mathbb{C}^0$ is a single point, so all hypotheses hold trivially and the conclusion is trivially true (take $v = u$ ). The hypotheses are satisfiable for every $n$ (e.g. $u \equiv 0$ , or any $u$ holomorphic on a neighbourhood of $\overline{D}$ ).

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph