Oscillation on circles from a weighted gradient bound near the origin

Proved

FiniteEnergyPlane.norm_sub_le_of_norm_mul_fderiv_le

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

pseudoholomorphic-curvesreal-analysis

Let $E$ be a real normed space, $R,\eta\in\mathbb{R}$ and $f:\mathbb{C}\to E$ a map that is differentiable at every $z$ with $0<|z|<R$ and satisfies

|z|\,\|Df(z)\|\le\eta\qquad(0<|z|<R),

where $\|Df(z)\|$ is the operator norm of the real derivative. Then for all $z,w\in\mathbb{C}$ with $z\ne0$ , $|z|<R$ and $|w|=|z|$ ,

\|f(z)-f(w)\|\le\pi\,\eta .

So the image of each circle $|z|=\rho<R$ has diameter at most $\pi\eta$ . This controls the oscillation of a map on small circles around a puncture.

Formalization Note Differentiability and the bound are assumed pointwise on $0<\|z\|<R$ ; $\|Df(z)\|$ is ‖fderiv ℝ f z‖.

Preamble

import Mathlib.Analysis.SpecialFunctions.Complex.Arg
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.Calculus.MeanValue

Formal statement

namespace FiniteEnergyPlane

open Metric Filter Topology
open scoped Real

/-- Oscillation on circles: let `f : ℂ → E` be differentiable on the punctured disc `0 < |z| < R`
with `|z| ‖Df(z)‖ ≤ η` there. Then any two points `z, w` on a common circle `|z| = |w| < R`
around the origin satisfy `‖f z - f w‖ ≤ π η`. -/
theorem norm_sub_le_of_norm_mul_fderiv_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : ℂ → E) (R η : ℝ)
    (hf : ∀ z : ℂ, z ≠ 0 → ‖z‖ < R → DifferentiableAt ℝ f z ∧ ‖z‖ * ‖fderiv ℝ f z‖ ≤ η) :
    ∀ z w : ℂ, z ≠ 0 → ‖z‖ < R → ‖w‖ = ‖z‖ → ‖f z - f w‖ ≤ π * η := by
  sorry

end FiniteEnergyPlane

Source

Elementary; used in C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, proof of Theorem 9.2, pp. 154-155

View graph