Prove2Me

A real differentiable reparametrization between JJ-holomorphic maps is complex differentiable

Proved
FiniteEnergyPlane.differentiableAt_complex_of_eventuallyEq_comp

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

complex-analysispseudoholomorphic-curves

Let EE be a real normed space, J:E→EndR(E)J:E\to\mathrm{End}_{\mathbb{R}}(E), u,v:C→Eu,v:\mathbb{C}\to E and φ:C→C\varphi:\mathbb{C}\to\mathbb{C} with u=v∘φu=v\circ\varphi near zz. Suppose φ\varphi is real differentiable at zz, vv is real differentiable at φ(z)\varphi(z) with injective derivative, J(u(z))2=−1J(u(z))^2=-1, and the equation ∂s+J∂t=0\partial_s+J\partial_t=0 holds for uu at zz and for vv at φ(z)\varphi(z). Then φ\varphi is complex differentiable at zz.

Role: pointwise statement identifying reparametrizations between curves as holomorphic, needing no regularity beyond one derivative at the point.

Preamble
import Definitions.Def_JHolomorphic_Setting
Formal statement
namespace FiniteEnergyPlane

open Filter Topology

/-- Let `u = v ∘ φ` near `z`, with `φ : ℂ → ℂ` real differentiable at `z`, `v` real differentiable at
`φ z` with injective derivative, and suppose `J(u z)² = -1` and the Cauchy-Riemann equation
`∂ₛ + J ∂ₜ = 0` holds for `u` at `z` and for `v` at `φ z`. Then `φ` is complex differentiable at
`z`. -/
theorem differentiableAt_complex_of_eventuallyEq_comp {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] (J : E → E →L[ℝ] E) (u v : ℂ → E) (φ : ℂ → ℂ) (z : ℂ)
    (hJ2 : (J (u z)).comp (J (u z)) = -ContinuousLinearMap.id ℝ E)
    (hφ : DifferentiableAt ℝ φ z) (hv : DifferentiableAt ℝ v (φ z))
    (heq : u =ᶠ[𝓝 z] v ∘ φ)
    (huh : fderiv ℝ u z 1 + J (u z) (fderiv ℝ u z Complex.I) = 0)
    (hvh : fderiv ℝ v (φ z) 1 + J (v (φ z)) (fderiv ℝ v (φ z) Complex.I) = 0)
    (hvi : Function.Injective (fderiv ℝ v (φ z))) :
    DifferentiableAt ℂ φ z := by
  sorry

end FiniteEnergyPlane
Source
Standard fact on pseudoholomorphic maps, cf. D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, Chapter 2

View graph