Accumulating zeros of a solution of $|\partial_s g+i\partial_t g|\le M|g|$ force local vanishing

Proved

FiniteEnergyPlane.eventually_eq_zero_of_norm_dbar_le

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

pseudoholomorphic-curvessimilarity-principleunique-continuation

Let $U\subset\mathbb{C}$ be open and $g:U\to\mathbb{C}$ be $C^\infty$ with $|\partial_s g+i\,\partial_t g|\le M|g|$ on $U$ . If $z_0\in U$ is an accumulation point of the zero set of $g$ , then $g$ vanishes on a neighbourhood of $z_0$ .

Role: the identity theorem for perturbed Cauchy-Riemann solutions; it complements the positive local winding at isolated zeros.

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace FiniteEnergyPlane

open Filter Topology
open scoped ContDiff

/-- Let `g` be smooth on the open set `U ⊆ ℂ` with `|∂ₛg + i ∂ₜg| ≤ M |g|` on `U`, and let `z₀ ∈ U`
be an accumulation point of the zeros of `g`. Then `g` vanishes identically near `z₀`. -/
theorem eventually_eq_zero_of_norm_dbar_le (g : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U)
    (hg : ContDiffOn ℝ ∞ g U) (M : ℝ)
    (hM : ∀ z ∈ U, ‖fderiv ℝ g z 1 + Complex.I * fderiv ℝ g z Complex.I‖ ≤ M * ‖g z‖)
    (z₀ : ℂ) (hz₀ : z₀ ∈ U) (hacc : ∃ᶠ z in 𝓝[≠] z₀, g z = 0) :
    ∀ᶠ z in 𝓝 z₀, g z = 0 := by
  sorry

end FiniteEnergyPlane

Source

Cf. C. Wendl, Lectures on Holomorphic Curves in Symplectic and Contact Geometry, arXiv:1011.1690, Section 2.5, and H. Hofer, K. Wysocki, E. Zehnder, GAFA 5 (1995), Section 3

View graph

Accumulating zeros of a solution of ∣∂sg+i∂tg∣≤M∣g∣|\partial_s g+i\partial_t g|\le M|g|∣∂s​g+i∂t​g∣≤M∣g∣ force local vanishing

Accumulating zeros of a solution of $|\partial_s g+i\partial_t g|\le M|g|$ force local vanishing