Pseudoholomorphic maps under real affine reparametrization of the domain

Proved

JHolomorphic.isJHolomorphicOn_comp_affine

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

pseudoholomorphic-curvessymplectic-geometry

Let $E$ be a real normed space, $J : E \to \mathcal{L}(E,E)$ any map, $U\subseteq\mathbb{C}$ and $u:\mathbb{C}\to E$ a map that is $J$ -holomorphic on $U$ , i.e. differentiable at every $z\in U$ with $\partial_s u + J(u)\,\partial_t u = 0$ there. Then for every $a\in\mathbb{C}$ and $c\in\mathbb{R}$ the map

\zeta\mapsto u(a + c\,\zeta)

is $J$ -holomorphic on $\{\zeta\in\mathbb{C} : a + c\,\zeta\in U\}$ .

This is the basic reparametrization step used whenever a pseudoholomorphic map is blown up or shrunk around a point, e.g. when rescaling onto the unit disc near a puncture.

Formalization Note $J$ -holomorphicity is JHolomorphic.IsJHolomorphicOn: pointwise differentiability and vanishing of dbarJ on the set; no assumption on $J$ is needed. The real scalar $c$ enters as the complex number (c : ℂ).

Deprecated (2026-10-24): duplicate of FiniteEnergyPlane.isJHolomorphicOn_comp_add_smul, which was published in parallel and also gives the derivative formula. Cite that theorem instead.

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace JHolomorphic

open Metric Filter Topology

/-- A `J`-holomorphic map stays `J`-holomorphic under a real rescaling and translation of the
domain: if `u` is `J`-holomorphic on `U ⊆ ℂ`, then `ζ ↦ u (a + c ζ)` (`a ∈ ℂ`, `c ∈ ℝ`) is
`J`-holomorphic on the preimage `{ζ | a + c ζ ∈ U}`. -/
theorem isJHolomorphicOn_comp_affine {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (J : E → E →L[ℝ] E) (U : Set ℂ) (u : ℂ → E) (hu : IsJHolomorphicOn J U u)
    (a : ℂ) (c : ℝ) :
    IsJHolomorphicOn J {ζ | a + (c : ℂ) * ζ ∈ U} (fun ζ => u (a + (c : ℂ) * ζ)) := by
  sorry

end JHolomorphic

Source

Standard; used in C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 9 (rescaling near a puncture)

View graph