A differentiable map on an open subset of $\mathbb{C}$ with a compact fibre has nonzero derivative at points with values arbitrarily close to that fibre value

Proved

FiniteEnergyPlane.exists_fderiv_ne_zero_of_isCompact_fiber

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

complex-analysispseudoholomorphic-curvestopology

Let $F$ be a real normed space, $U\subseteq\mathbb{C}$ open and $u:\mathbb{C}\to F$ real-differentiable on $U$ . Let $p\in u(U)$ and assume that the fibre $U\cap u^{-1}(p)$ is compact. Then for every $\varepsilon>0$ there is $z\in U$ with

\|u(z)-p\|<\varepsilon\qquad\text{and}\qquad Du(z)\neq 0 .

This holds for every map that is proper onto a neighbourhood of $p$ (for example a proper map of $U$ into a ball around $p$ ), so such maps have regular points with values arbitrarily close to $p$ .

Formalization Note Differentiability is DifferentiableOn ℝ u U, the fibre hypothesis is IsCompact (U ∩ u ⁻¹' {p}), and $Du(z)$ is fderiv ℝ u z.

Preamble

import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Connected.Clopen

Formal statement

namespace FiniteEnergyPlane

open Metric Filter Topology

/-- Let `u` be differentiable on an open set `U ⊆ ℂ` and let `p ∈ u(U)` have compact fibre
`U ∩ u⁻¹(p)`. Then every neighbourhood `B_ε(p)` contains a value `u(z)`, `z ∈ U`, at which the
derivative of `u` is nonzero. -/
theorem exists_fderiv_ne_zero_of_isCompact_fiber {F : Type*} [NormedAddCommGroup F]
    [NormedSpace ℝ F] {U : Set ℂ} (hU : IsOpen U) {u : ℂ → F} (hu : DifferentiableOn ℝ u U)
    {p : F} (hp : p ∈ u '' U) (hK : IsCompact (U ∩ u ⁻¹' {p})) {ε : ℝ} (hε : 0 < ε) :
    ∃ z ∈ U, ‖u z - p‖ < ε ∧ fderiv ℝ u z ≠ 0 := by
  sorry

end FiniteEnergyPlane

Source

Standard; used for the monotonicity lemma, A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331, Proposition 3.12; C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, p. 152

View graph

A differentiable map on an open subset of C\mathbb{C}C with a compact fibre has nonzero derivative at points with values arbitrarily close to that fibre value

A differentiable map on an open subset of $\mathbb{C}$ with a compact fibre has nonzero derivative at points with values arbitrarily close to that fibre value