Solutions of real-linear Cauchy–Riemann equations factor locally through holomorphic maps

Proved

JHolomorphic.exists_holomorphic_factorization

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

elliptic-regularitypseudoholomorphic-curvessobolev-spacessymplectic-geometryunique-continuation

Let $E$ be a real vector space of dimension $2n$ , let $D\subset\mathbb{C}$ be the open unit disc, and let $\bar J,A:D\to\operatorname{End}_{\mathbb{R}}(E)$ be $C^\infty$ with $\bar J(z)^2=-\mathrm{Id}$ . Let $h:D\to E$ be $C^\infty$ with

\partial_sh+\bar J(z)\,\partial_th+A(z)\,h=0\quad\text{on }D.

Then there are $\varepsilon>0$ , a continuous map $\Phi$ from the closed disc $\bar D_\varepsilon$ to the real-linear maps $\mathbb{C}^n\to E$ , each $\Phi(z)$ bijective with $\Phi(z)(iw)=\bar J(z)\,\Phi(z)w$ , and a holomorphic $f:D_\varepsilon\to\mathbb{C}^n$ , such that

h(z)=\Phi(z)\,f(z)\quad\text{for }z\in D_\varepsilon.

Formalization Note Wendl's Theorem 2.26 is the case $E=\mathbb{C}^n$ , $\bar J\equiv i$ , and assumes in addition $h(0)=0$ . $E$ is a normed space with Module.finrank ℝ E = 2 * n, $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n), $\Phi$ has type ℂ → EuclideanSpace ℂ (Fin n) →L[ℝ] E with ContinuousOn Φ (closedBall 0 ε), and $f$ satisfies DifferentiableOn ℂ f (ball 0 ε).

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology DbarRegularity
open scoped ContDiff ENNReal NNReal

/-- Wendl, Theorem 2.26 (p. 39), generalized to a complex structure that varies with the
point: let `E` have real dimension `2n`, let `J̄ : D → End_ℝ(E)` be smooth on the open
unit disc `D` with `J̄(z)² = -1`, let `A : D → End_ℝ(E)` be smooth, and let `h : D → E` be smooth
with `∂ₛh + J̄(z) ∂ₜh + A(z) h = 0`. For some `ε > 0` there are a continuous
`Φ : D̄_ε → Hom_ℝ(ℂⁿ, E)` with every `Φ(z)` bijective and `Φ(z) ∘ i = J̄(z) ∘ Φ(z)`, and a
holomorphic `f : D_ε → ℂⁿ` with `h = Φ f` on `D_ε`. (Wendl's Theorem 2.26 is the case
`E = ℂⁿ`, `J̄ ≡ i`; he also assumes `h(0) = 0`.) -/
theorem exists_holomorphic_factorization {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (n : ℕ)
    (hn : Module.finrank ℝ E = 2 * n) (Jbar A : ℂ → E →L[ℝ] E)
    (hJbar : ContDiffOn ℝ ∞ Jbar (ball 0 1))
    (hJbar2 : ∀ z ∈ ball (0 : ℂ) 1, (Jbar z).comp (Jbar z) = -ContinuousLinearMap.id ℝ E)
    (hA : ContDiffOn ℝ ∞ A (ball 0 1)) (h : ℂ → E) (hh : ContDiffOn ℝ ∞ h (ball 0 1))
    (heq : ∀ z ∈ ball (0 : ℂ) 1,
      fderiv ℝ h z 1 + Jbar z (fderiv ℝ h z Complex.I) + A z (h z) = 0) :
    ∃ ε > (0 : ℝ), ∃ Φ : ℂ → EuclideanSpace ℂ (Fin n) →L[ℝ] E,
      ∃ f : ℂ → EuclideanSpace ℂ (Fin n), ContinuousOn Φ (closedBall 0 ε) ∧
        (∀ z ∈ closedBall (0 : ℂ) ε, Function.Bijective (Φ z) ∧
          ∀ w, Φ z (Complex.I • w) = Jbar z (Φ z w)) ∧
        DifferentiableOn ℂ f (ball 0 ε) ∧ ∀ z ∈ ball (0 : ℂ) ε, h z = Φ z (f z) := by
  sorry

end JHolomorphic

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 2, Theorem 2.26, p. 39, generalized to a complex structure that varies with the point

Read-back

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

`JHolomorphic.exists_holomorphic_factorization`

Setting. Let $E$ be a finite-dimensional real normed vector space, and let $n \in \mathbb{N}$ be a natural number with $\dim_{\mathbb{R}} E = 2n$ . (The case $n = 0$ is allowed; then $E = \{0\}$ .) Write $\mathbb{D} = \{ z \in \mathbb{C} : |z| < 1 \}$ for the open unit disc, and identify $\mathbb{C}$ with $\mathbb{R}^2$ via $z = s + it$ . The statement does not use any of the named definitions of the imported bundles (such as $\bar\partial_J$ , $J$ -holomorphy, or weak $J$ -holomorphy); every condition below is written out directly.

Data and hypotheses. Given:

a map $\bar J : \mathbb{C} \to \mathcal{L}_{\mathbb{R}}(E, E)$ (continuous $\mathbb{R}$ -linear endomorphisms of $E$ , depending on the point $z \in \mathbb{C}$ , not on a point of $E$ ) which is $C^\infty$ (smooth, in the real sense) on $\mathbb{D}$ , and which satisfies

\bar J(z) \circ \bar J(z) = -\mathrm{id}_E \qquad \text{for every } z \in \mathbb{D};

a map $A : \mathbb{C} \to \mathcal{L}_{\mathbb{R}}(E, E)$ which is $C^\infty$ on $\mathbb{D}$ (no further condition on $A$ );
a map $h : \mathbb{C} \to E$ which is $C^\infty$ on $\mathbb{D}$ and satisfies, for every $z \in \mathbb{D}$ ,

\partial_s h(z) + \bar J(z)\,\partial_t h(z) + A(z)\,h(z) = 0,

where $\partial_s h(z) = Dh(z)[1]$ and $\partial_t h(z) = Dh(z)[i]$ are the values of the real Fréchet derivative of $h$ at $z$ on the vectors $1$ and $i$ .

The values of $\bar J$ , $A$ and $h$ outside $\mathbb{D}$ are unconstrained.

Conclusion. There exist a real number $\varepsilon > 0$ , a map $\Phi : \mathbb{C} \to \mathcal{L}_{\mathbb{R}}(\mathbb{C}^n, E)$ (continuous $\mathbb{R}$ -linear maps from $\mathbb{C}^n$ , with its Euclidean structure, to $E$ ), and a map $f : \mathbb{C} \to \mathbb{C}^n$ such that:

$\Phi$ is continuous on the closed disc $\overline{B}(0,\varepsilon) = \{ |z| \le \varepsilon \}$ (with respect to the operator-norm topology on $\mathcal{L}_{\mathbb{R}}(\mathbb{C}^n, E)$ );
for every $z$ with $|z| \le \varepsilon$ , the $\mathbb{R}$ -linear map $\Phi(z) : \mathbb{C}^n \to E$ is bijective, and

\Phi(z)(i\,w) = \bar J(z)\big(\Phi(z)\,w\big) \qquad \text{for all } w \in \mathbb{C}^n;

$f$ is complex-differentiable (holomorphic) at every point of the open disc $B(0,\varepsilon) = \{ |z| < \varepsilon \}$ ;
for every $z$ with $|z| < \varepsilon$ ,

h(z) = \Phi(z)\big(f(z)\big).

Remarks on what is and is not asserted. No upper bound on $\varepsilon$ is required; in particular $\varepsilon \ge 1$ is not excluded, in which case conditions 2 and 4 would also refer to points outside $\mathbb{D}$ , where $\bar J$ and $h$ are arbitrary (condition 2 forces $\bar J(z)^2 = -\mathrm{id}_E$ at every point of the closed disc). No regularity of $\Phi$ beyond continuity on the closed disc is asserted, and nothing is asserted about $f$ or $\Phi$ outside the respective discs. Nothing is asserted about $f$ being nonzero, and $h \equiv 0$ is allowed (then $f \equiv 0$ is permitted). The intertwining relation in condition 2 says that $\Phi(z)$ carries multiplication by $i$ on $\mathbb{C}^n$ to $\bar J(z)$ on $E$ . When $n = 0$ all spaces involved are zero and every condition holds trivially for any $\varepsilon > 0$ .

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