Prove2Me

Hofer's topological lemma

Proved
FiniteEnergyPlane.hofer_lemma

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let (X,d)(X,d) be a complete metric space, g:X→[0,∞)g:X\to[0,\infty) continuous, x0∈Xx_0\in X and ε0>0\varepsilon_0>0. Then there are x∈Xx\in X and 0<ε≤ε00<\varepsilon\le\varepsilon_0 such that

ε g(x)≥ε0 g(x0),d(x,x0)≤2ε0,g(y)≤2g(x)  whenever d(y,x)≤ε.\varepsilon\,g(x)\ge\varepsilon_0\,g(x_0),\qquad d(x,x_0)\le2\varepsilon_0,\qquad g(y)\le2g(x)\ \text{ whenever } d(y,x)\le\varepsilon.

Formalization Note Wendl states the last property for yy in the open ball Bε(x)B_\varepsilon(x); here it is required on the closed ball closedBall x ε.

Preamble
import Definitions.Def_FiniteEnergyPlane_Setting
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hofer's topological lemma: Wendl, Lemma 9.4 (p. 154); Hofer 1993, Lemma 26 (p. 535). Let
`X` be a complete metric space, `g : X → [0, ∞)` continuous, `x₀ ∈ X` and `ε₀ > 0`. There are
`x ∈ X` and `0 < ε ≤ ε₀` with `ε g(x) ≥ ε₀ g(x₀)`, `d(x, x₀) ≤ 2ε₀`, and `g(y) ≤ 2 g(x)` whenever
`d(y, x) ≤ ε`. (Wendl states the last property on the ball `B_ε(x)`; the closed ball is used
here.) -/
theorem hofer_lemma {X : Type*} [MetricSpace X] [CompleteSpace X] (g : X → ℝ)
    (hg : Continuous g) (hg0 : ∀ x, 0 ≤ g x) (x₀ : X) (ε₀ : ℝ) (hε₀ : 0 < ε₀) :
    ∃ x : X, ∃ ε : ℝ, 0 < ε ∧ ε ≤ ε₀ ∧ ε₀ * g x₀ ≤ ε * g x ∧ dist x x₀ ≤ 2 * ε₀ ∧
      ∀ y ∈ closedBall x ε, g y ≤ 2 * g x := by
  sorry

end FiniteEnergyPlane
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lemma 9.4, p. 154; H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515–563, Lemma 26, p. 535
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: FiniteEnergyPlane.hofer_lemma

Setting. Let XX be an arbitrary type carrying a metric space structure dd that is complete (no other assumption on XX; it is nonempty because a point x0x_0 is supplied). Let g:X→Rg : X \to \mathbb{R} be a continuous function with g(x)≥0g(x) \ge 0 for every x∈Xx \in X. Let x0∈Xx_0 \in X be any point and let ε0∈R\varepsilon_0 \in \mathbb{R} with ε0>0\varepsilon_0 > 0. No positivity of g(x0)g(x_0) is assumed.

Conclusion. There exist a point x∈Xx \in X and a real number ε\varepsilon such that all of the following hold simultaneously:

  1. 0<ε≤ε00 < \varepsilon \le \varepsilon_0;
ε0 g(x0)≤ε g(x);\varepsilon_0 \, g(x_0) \le \varepsilon \, g(x);
  1. d(x,x0)≤2ε0d(x, x_0) \le 2\varepsilon_0 (non-strict inequality);
  2. for every yy in the closed ball Bˉ(x,ε)={y∈X:d(y,x)≤ε}\bar B(x, \varepsilon) = \{ y \in X : d(y, x) \le \varepsilon \},
g(y)≤2 g(x).g(y) \le 2\, g(x).

Edge cases. If g(x0)=0g(x_0) = 0, condition 2 reads 0≤ε g(x)0 \le \varepsilon\, g(x), which holds automatically for any ε>0\varepsilon > 0 since g≥0g \ge 0; the remaining conditions still have to be met by the chosen x,εx, \varepsilon. The doubling bound in condition 4 is relative to the value g(x)g(x) at the centre, and the ball in condition 4 is closed. The point xx is allowed to equal x0x_0 and ε\varepsilon is allowed to equal ε0\varepsilon_0. The statement makes no use of any definition specific to the finite-energy-plane setting.

Human review

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Mazecto · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph