Almost complex structures, pseudoholomorphic maps and weak solutions on planar domains

Definition

JHolomorphic_Setting

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

elliptic-regularitypseudoholomorphic-curvessobolev-spacessymplectic-geometryunique-continuation

Basic objects for pseudoholomorphic maps from planar domains into a finite-dimensional real vector space (C. Wendl, Lectures on Symplectic Field Theory, Lecture 2, § 2.4, and Lecture 9).

Almost complex structures on an open set. For an open $O\subseteq E$ , a map $J:E\to\operatorname{End}_{\mathbb{R}}(E)$ is a smooth almost complex structure on $O$ if it is $C^\infty$ on $O$ and $J(x)^2=-\mathrm{Id}$ for every $x\in O$ . Values of $J$ outside $O$ play no role.
The nonlinear Cauchy–Riemann operator. For $u:\mathbb{C}\to E$ and $z=s+it$ , $\bar\partial_Ju(z)=\partial_su(z)+J(u(z))\,\partial_tu(z)$ .
$J$ -holomorphic maps. $u$ is $J$ -holomorphic on $U\subseteq\mathbb{C}$ if it is differentiable at every $z\in U$ and $\bar\partial_Ju(z)=0$ there.
Weak partial derivatives. $u_s,u_t$ are weak partial derivatives of $u$ on $U$ if $\int(\partial_s\varphi)\,u=-\int\varphi\,u_s$ and $\int(\partial_t\varphi)\,u=-\int\varphi\,u_t$ for every real $C^\infty$ function $\varphi$ with compact support in $U$ .
$W^{1,p}_{\mathrm{loc}}$ solutions. $u$ is a weak solution of $\bar\partial_Ju=0$ on $U$ with values in $O$ if $u$ is continuous on $U$ , $u(U)\subseteq O$ , $u$ has weak partial derivatives $u_s,u_t$ on $U$ , the maps $u,u_s,u_t$ lie in $L^p(K)$ for every compact $K\subseteq U$ , and $u_s+J(u)\,u_t=0$ almost everywhere on $U$ .
$C^\infty_{\mathrm{loc}}$ convergence. $f_\nu\to g$ in $C^\infty_{\mathrm{loc}}$ on $O$ if for every compact $K\subseteq O$ and every $m\ge0$ the $m$ -th derivatives $D^mf_\nu$ converge to $D^mg$ uniformly on $K$ .

Formalization Note $E$ is a real normed space with [FiniteDimensional ℝ E]; no inner product is assumed (product norms are allowed). $J$ has type E → E →L[ℝ] E. $\partial_su$ and $\partial_tu$ are fderiv ℝ u z 1 and fderiv ℝ u z Complex.I. Smoothness is ContDiff ℝ ∞ / ContDiffOn ℝ ∞ ( $C^\infty$ , not analytic). $L^p$ membership is MemLp _ (ENNReal.ofReal p) (volume.restrict K) and integrals are Bochner integrals for Lebesgue measure on $\mathbb{C}$ . Derivatives of order $m$ are iteratedFDeriv ℝ m. The module imports the DbarRegularity setting, whose sobolevNorm k p U φ $=\sum_{j\le k}\|D^j\varphi\|_{L^p(U)}$ appears in the statements.

Definition code

import Definitions.Def_DbarRegularity_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Topology.UniformSpace.UniformConvergence

/-!
# Pseudoholomorphic maps from planar domains

C. Wendl, *Lectures on Symplectic Field Theory*, arXiv:1612.01009, Lecture 2 (§ 2.4–2.5) and
Lecture 9, Proposition 9.1.

Conventions. The target is a finite-dimensional real normed space `E`; an almost complex
structure is only required on an open subset `O ⊆ E`. A point of the domain is `z = s + i t ∈ ℂ`,
`∂ₛu = Du(z) 1` and `∂ₜu = Du(z) i`.

* `IsAlmostComplexOn J O`: `O` is open, `J : E → (E →L[ℝ] E)` is `C^∞` on `O` and
  `J(x)² = -1` for `x ∈ O` (Wendl, Lecture 2).
* `dbarJ J u z = ∂ₛu + J(u) ∂ₜu`, the nonlinear Cauchy–Riemann operator `∂̄_J` (Wendl § 2.4.2).
* `IsJHolomorphicOn J U u`: `u` is differentiable at every `z ∈ U` and `∂̄_J u(z) = 0`.
* `HasWeakPartialsOn U u uₛ uₜ`: `uₛ`, `uₜ` are the weak partial derivatives of `u` on `U`,
  tested against real `C^∞` functions with compact support in `U`.
* `IsWeakJHolomorphicOn p J O U u`: `u` is continuous on `U` with values in `O`, `u` and its
  weak partials lie in `L^p(K)` for every compact `K ⊆ U`, and `uₛ + J(u) uₜ = 0` almost
  everywhere on `U`. For `p > 2` this is a `W^{1,p}_loc` solution of `∂̄_J u = 0` (Wendl, Theorem 2.22 (1) and Remark 2.25).
* `TendstoCInftyLocOn f g O`: `f ν → g` in `C^∞_loc` on `O`, i.e. every derivative `Dᵐ f ν`
  converges to `Dᵐ g` uniformly on every compact subset of `O`.

The `W^{k,p}(U)` norm `DbarRegularity.sobolevNorm` of the `DbarRegularity` mission is reused.
-/

namespace JHolomorphic

noncomputable section

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]

/-- `J` is a smooth almost complex structure on the open set `O ⊆ E`: `J` is `C^∞` on `O` and
`J(x) ∘ J(x) = -1` for every `x ∈ O`. -/
def IsAlmostComplexOn (J : E → E →L[ℝ] E) (O : Set E) : Prop :=
  IsOpen O ∧ ContDiffOn ℝ ∞ J O ∧ ∀ x ∈ O, (J x).comp (J x) = -ContinuousLinearMap.id ℝ E

/-- The nonlinear Cauchy–Riemann operator `∂̄_J u = ∂ₛu + J(u) ∂ₜu` at `z = s + i t`. -/
def dbarJ (J : E → E →L[ℝ] E) (u : ℂ → E) (z : ℂ) : E :=
  fderiv ℝ u z 1 + J (u z) (fderiv ℝ u z Complex.I)

/-- `u` is `J`-holomorphic on `U`: it is differentiable at every `z ∈ U` and
`∂ₛu + J(u) ∂ₜu = 0` there. -/
def IsJHolomorphicOn (J : E → E →L[ℝ] E) (U : Set ℂ) (u : ℂ → E) : Prop :=
  ∀ z ∈ U, DifferentiableAt ℝ u z ∧ dbarJ J u z = 0

/-- `uₛ` and `uₜ` are weak partial derivatives of `u` on `U`: for every real `C^∞` function `φ`
with compact support in `U`, `∫ (∂ₛφ) u = -∫ φ uₛ` and `∫ (∂ₜφ) u = -∫ φ uₜ`. -/
def HasWeakPartialsOn (U : Set ℂ) (u us ut : ℂ → E) : Prop :=
  ∀ φ : ℂ → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ → tsupport φ ⊆ U →
    (∫ z, fderiv ℝ φ z 1 • u z = -∫ z, φ z • us z) ∧
      (∫ z, fderiv ℝ φ z Complex.I • u z = -∫ z, φ z • ut z)

/-- `u` is a `W^{1,p}_loc` solution of `∂̄_J u = 0` on `U` with values in `O`: `u` is continuous
on `U` with `u(U) ⊆ O`, `u` has weak partial derivatives `uₛ`, `uₜ` on `U`, the three maps lie in
`L^p(K)` for every compact `K ⊆ U`, and `uₛ + J(u) uₜ = 0` almost everywhere on `U`. -/
def IsWeakJHolomorphicOn (p : ℝ) (J : E → E →L[ℝ] E) (O : Set E) (U : Set ℂ) (u : ℂ → E) :
    Prop :=
  ContinuousOn u U ∧ Set.MapsTo u U O ∧
    ∃ us ut : ℂ → E, HasWeakPartialsOn U u us ut ∧
      (∀ K ⊆ U, IsCompact K →
        MemLp u (ENNReal.ofReal p) (volume.restrict K) ∧
        MemLp us (ENNReal.ofReal p) (volume.restrict K) ∧
        MemLp ut (ENNReal.ofReal p) (volume.restrict K)) ∧
      ∀ᵐ z ∂(volume.restrict U), us z + J (u z) (ut z) = 0

/-- `f ν → g` in `C^∞_loc` on `O`: for every compact `K ⊆ O` and every `m`, the `m`-th
derivatives `Dᵐ (f ν)` converge to `Dᵐ g` uniformly on `K`. -/
def TendstoCInftyLocOn {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : ℕ → X → Y) (g : X → Y) (O : Set X) : Prop :=
  ∀ K ⊆ O, IsCompact K → ∀ m : ℕ,
    TendstoUniformlyOn (fun ν => iteratedFDeriv ℝ m (f ν)) (iteratedFDeriv ℝ m g) atTop K

end

end JHolomorphic

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 2, Section 2.4 (nonlinear Cauchy–Riemann equation, p. 35), and Lecture 9, Proposition 9.1 (p. 151)

Read-back

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

Module `JHolomorphic` setting (definitions)

Common setting. Unless stated otherwise, $E$ is an arbitrary finite-dimensional real normed vector space (any dimension, including $E=\{0\}$ ). The complex plane $\mathbb C$ is treated as the real 2-dimensional space with coordinates $z=s+it$ ; " $Du(z)$ " below always means the real Fréchet derivative of a map at $z$ , so $Du(z)\cdot 1=\partial_s u(z)$ and $Du(z)\cdot i=\partial_t u(z)$ when $u$ is differentiable at $z$ . Wherever the code takes a Fréchet derivative of a map at a point where the map is not differentiable, the value is the zero linear map. Measures on $\mathbb C$ are the standard Lebesgue (volume) measure on $\mathbb C\cong\mathbb R^2$ . A "field of endomorphisms" $J$ means an arbitrary map $J:E\to\mathcal L(E,E)$ assigning to each point $x\in E$ a continuous real-linear map $J(x):E\to E$ , with no regularity assumed unless stated. The module imports the previously published module DbarRegularity (which defines a maximal function, closed cubes, the operator $\bar\partial\varphi=D\varphi(z)\cdot1+i\,D\varphi(z)\cdot i$ for complex-normed targets, and a Sobolev-type norm), but none of the five definitions below refers to any of those definitions.

1. IsAlmostComplexOn J O. For a field of endomorphisms $J:E\to\mathcal L(E,E)$ and a set $O\subseteq E$ , this is the proposition that all three of the following hold:

$O$ is open in $E$ ;
$J$ is $C^\infty$ (smooth: continuously differentiable to every finite order, not analytic) on $O$ , as a map into the normed space $\mathcal L(E,E)$ ;
for every $x\in O$ , $J(x)\circ J(x)=-\mathrm{id}_E$ .

Nothing is required of $J$ outside $O$ . If $O=\varnothing$ the condition holds for every $J$ . If $E=\{0\}$ then $-\mathrm{id}_E=\mathrm{id}_E=0$ , so the third clause holds automatically. If $O\neq\varnothing$ and $\dim E$ is odd, the third clause cannot be satisfied (no real linear map on an odd-dimensional space squares to $-\mathrm{id}$ ), so the condition is then false.

2. dbarJ J u z. For a field of endomorphisms $J$ , a map $u:\mathbb C\to E$ and a point $z\in\mathbb C$ , this is the vector

\bar\partial_J u(z)\;=\;Du(z)\cdot 1\;+\;J\big(u(z)\big)\big(Du(z)\cdot i\big)\;\in E,

i.e. $\partial_s u(z)+J(u(z))\,\partial_t u(z)$ when $u$ is differentiable at $z$ . There is no factor $\tfrac12$ . If $u$ is not real-differentiable at $z$ , both derivative terms are $0$ and $\bar\partial_J u(z)=0$ . No hypothesis on $J$ (almost complex or otherwise) is involved.

3. IsJHolomorphicOn J U u. For a field of endomorphisms $J$ , an arbitrary set $U\subseteq\mathbb C$ and a map $u:\mathbb C\to E$ , this is the proposition that for every $z\in U$ :

$u$ is real Fréchet-differentiable at $z$ (as a map on all of $\mathbb C$ ), and
$\bar\partial_J u(z)=Du(z)\cdot1+J(u(z))(Du(z)\cdot i)=0$ .

$U$ is not required to be open; no continuity of the derivative or higher smoothness of $u$ is required; there is no requirement that $u$ map $U$ into any particular set, nor that $J$ be almost complex anywhere. If $U=\varnothing$ the condition holds vacuously.

4. HasWeakPartialsOn U u us ut. For an arbitrary set $U\subseteq\mathbb C$ and three maps $u,u_s,u_t:\mathbb C\to E$ , this is the proposition that for every real-valued test function $\varphi:\mathbb C\to\mathbb R$ which is $C^\infty$ on all of $\mathbb C$ , has compact support, and whose closed support $\overline{\{\varphi\neq0\}}$ is contained in $U$ , both identities hold:

\int_{\mathbb C}\big(D\varphi(z)\cdot 1\big)\,u(z)\,dz=-\int_{\mathbb C}\varphi(z)\,u_s(z)\,dz, \qquad \int_{\mathbb C}\big(D\varphi(z)\cdot i\big)\,u(z)\,dz=-\int_{\mathbb C}\varphi(z)\,u_t(z)\,dz,

where $D\varphi(z)\cdot1=\partial_s\varphi(z)$ , $D\varphi(z)\cdot i=\partial_t\varphi(z)$ , the products are real scalars times vectors of $E$ , and the integrals are $E$ -valued Bochner integrals over all of $\mathbb C$ against Lebesgue measure. No integrability or measurability of $u,u_s,u_t$ is assumed by this definition; by convention a Bochner integral of a non-integrable function is $0$ , so an identity can hold because both sides are assigned the value $0$ (or one side is $0$ by this convention and the other happens to be $0$ ). If $U$ has empty interior, the only admissible test function is $\varphi\equiv0$ and the condition holds for all $u,u_s,u_t$ . $U$ is not required to be open or measurable.

5. IsWeakJHolomorphicOn p J O U u. For a real number $p$ (any real, no sign restriction), a field of endomorphisms $J$ , a set $O\subseteq E$ , a set $U\subseteq\mathbb C$ , and a map $u:\mathbb C\to E$ , this is the proposition that all of the following hold:

$u$ is continuous on $U$ (relative to $U$ );
$u(U)\subseteq O$ ;
there exist maps $u_s,u_t:\mathbb C\to E$ $u_{s}, u_{t} : C \to E$ such that
- $(u,u_s,u_t)$ satisfy definition 4 on $U$ (HasWeakPartialsOn U u u_s u_t);
- for every compact set $K\subseteq U$ , each of $u$ , $u_s$ , $u_t$ belongs to $L^{q}(K)$ with exponent $q=\max(p,0)\in[0,\infty)$ (the extended nonnegative real obtained from $p$ , so $q=0$ when $p\le0$ ), with respect to Lebesgue measure restricted to $K$ ; this means the function is almost-everywhere strongly measurable for that measure and its $L^q$ seminorm over $K$ is finite. When $p\le0$ (exponent $0$ ) the $L^0$ seminorm is $0$ by convention, so the requirement reduces to a.e.-strong measurability on $K$ . The exponent $\infty$ is never produced;
- for Lebesgue-almost every $z\in U$ (a.e. with respect to Lebesgue measure restricted to $U$ ),

u_s(z)+J\big(u(z)\big)\big(u_t(z)\big)=0.

The same witnesses $u_s,u_t$ must serve in all three bullet points. The definition does not require $O$ to be open, does not require $J$ to be almost complex (definition 1 is not used), does not require $U$ to be open, and places no constraint on $u$ outside $U$ . If $U=\varnothing$ , the condition reduces to the existence of some $u_s,u_t$ (which trivially holds, e.g. $u_s=u_t=0$ ; all constraints on $U$ , compact $K\subseteq U$ , and a.e. on $U$ are then vacuous).

6. TendstoCInftyLocOn f g O. Here, separately from $E$ , $X$ and $Y$ are arbitrary real normed vector spaces (no completeness or finite-dimensionality assumed). For a sequence of maps $f_\nu:X\to Y$ ( $\nu\in\mathbb N$ ), a map $g:X\to Y$ and a set $O\subseteq X$ , this is the proposition that for every compact set $K\subseteq O$ and every order $m\in\mathbb N$ (including $m=0$ ),

D^m f_\nu\;\longrightarrow\;D^m g\quad\text{uniformly on }K\text{ as }\nu\to\infty,

i.e. $\sup_{x\in K}\big\|D^m f_\nu(x)-D^m g(x)\big\|\to0$ , where $D^m h(x)$ is the $m$ -th iterated Fréchet derivative of $h$ at $x$ , a continuous $m$ -linear map $X^m\to Y$ , measured in the operator (multilinear) norm. For $m=0$ this is uniform convergence $f_\nu\to g$ on $K$ . The iterated derivatives are those of the maps on the whole space $X$ (not derivatives within $O$ ). No differentiability of $f_\nu$ or $g$ is assumed: at points where an iterated derivative does not exist in the Fréchet sense, the code's value is the zero multilinear map, and the uniform convergence is required of these values. $O$ is not required to be open; if $O=\varnothing$ the only compact $K\subseteq O$ is $\varnothing$ and the condition holds vacuously.

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

Almost complex structures, pseudoholomorphic maps and weak solutions on planar domains

Module JHolomorphic setting (definitions)

Module `JHolomorphic` setting (definitions)