Prove2Me

Holomorphic factorization of a map with ∣∂sh+Jˉ(z)∂th∣≤M∣h∣|\partial_s h+\bar J(z)\partial_t h|\le M|h| near a point

Proved
JHolomorphic.exists_factorization_of_norm_dbar_le

by Mazecto · Nov 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysispseudoholomorphic-curvessimilarity-principle

Let EE be a real vector space of dimension 2n2n, U⊆CU\subseteq\mathbb{C} open, and Jˉ:U→EndR(E)\bar J:U\to\mathrm{End}_{\mathbb{R}}(E) smooth with Jˉ(z)2=−1\bar J(z)^2=-1. Let h:U→Eh:U\to E be smooth with

∥∂sh(z)+Jˉ(z) ∂th(z)∥≤M ∥h(z)∥(z∈U)\big\|\partial_s h(z)+\bar J(z)\,\partial_t h(z)\big\|\le M\,\|h(z)\|\qquad(z\in U)

for some constant MM, and let z0∈Uz_0\in U. Then there is ε>0\varepsilon>0 with B(z0,ε)⊆UB(z_0,\varepsilon)\subseteq U, a continuous map Θ:B‾(z0,ε)→HomR(Cn,E)\Theta:\overline{B}(z_0,\varepsilon)\to\mathrm{Hom}_{\mathbb{R}}(\mathbb{C}^n,E) such that every Θ(z)\Theta(z) is bijective and satisfies Θ(z)(iw)=Jˉ(z)Θ(z)w\Theta(z)(iw)=\bar J(z)\Theta(z)w, and a holomorphic f:B(z0,ε)→Cnf:B(z_0,\varepsilon)\to\mathbb{C}^n with

h(z)=Θ(z)f(z)(z∈B(z0,ε)).h(z)=\Theta(z)f(z)\qquad(z\in B(z_0,\varepsilon)).

This is the similarity principle for a complex structure varying with the point, in the form of a differential inequality and around an arbitrary point of an open set. It transfers the local zero structure of holomorphic maps (isolated zeros of finite order, or vanishing identically) to hh.

Formalization Note ∂sh,∂th\partial_s h,\partial_t h are fderiv ℝ h z 1 and fderiv ℝ h z Complex.I; Cn\mathbb{C}^n is EuclideanSpace ℂ (Fin n); the dimension hypothesis is Module.finrank ℝ E = 2 * n.

Preamble
import Definitions.Def_JHolomorphic_Setting
Formal statement
namespace JHolomorphic

open MeasureTheory Metric Filter Topology
open scoped ContDiff

/-- Let `E` have real dimension `2n`, let `U ⊆ ℂ` be open and let `J̄ : U → End_ℝ(E)` be smooth with
`J̄(z)² = -1`. Let `h : U → E` be smooth with `‖∂ₛh + J̄(z) ∂ₜh‖ ≤ M ‖h‖` on `U`, and let `z₀ ∈ U`.
Then for some `ε > 0` with `B(z₀, ε) ⊆ U` there are a continuous `Θ : B̄(z₀, ε) → Hom_ℝ(ℂⁿ, E)`
with every `Θ(z)` bijective and `Θ(z) ∘ i = J̄(z) ∘ Θ(z)`, and a holomorphic
`f : B(z₀, ε) → ℂⁿ` with `h = Θ f` on `B(z₀, ε)`. -/
theorem exists_factorization_of_norm_dbar_le {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] (n : ℕ) (hn : Module.finrank ℝ E = 2 * n)
    (Jbar : ℂ → E →L[ℝ] E) (U : Set ℂ) (hU : IsOpen U) (hJbar : ContDiffOn ℝ ∞ Jbar U)
    (hJbar2 : ∀ z ∈ U, (Jbar z).comp (Jbar z) = -ContinuousLinearMap.id ℝ E)
    (h : ℂ → E) (hh : ContDiffOn ℝ ∞ h U) (M : ℝ)
    (hM : ∀ z ∈ U, ‖fderiv ℝ h z 1 + Jbar z (fderiv ℝ h z Complex.I)‖ ≤ M * ‖h z‖)
    (z₀ : ℂ) (hz₀ : z₀ ∈ U) :
    ∃ ε > (0 : ℝ), ball z₀ ε ⊆ U ∧ ∃ Θ : ℂ → EuclideanSpace ℂ (Fin n) →L[ℝ] E,
      ∃ f : ℂ → EuclideanSpace ℂ (Fin n), ContinuousOn Θ (closedBall z₀ ε) ∧
        (∀ z ∈ closedBall z₀ ε, Function.Bijective (Θ z) ∧
          ∀ w, Θ z (Complex.I • w) = Jbar z (Θ z w)) ∧
        DifferentiableOn ℂ f (ball z₀ ε) ∧ ∀ z ∈ ball z₀ ε, h z = Θ z (f z) := by
  sorry

end JHolomorphic
Source
C. Wendl, Lectures on Holomorphic Curves in Symplectic and Contact Geometry (arXiv:1011.1690), Theorem 2.26 (similarity principle), local version on an open set

View graph