Prove2Me

Uniform bound and Lipschitz constant of a C1C^1 map on balls of fixed radius around a compact set

Proved
FiniteEnergyPlane.exists_lipschitz_near_compact

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

compactnesslipschitzreal-analysis

Let EE be a finite-dimensional real normed space, FF a real normed space, O⊆EO\subseteq E open, f:E→Ff:E\to F of class C1C^1 on OO, and K⊆OK\subseteq O compact. Then there are δ>0\delta>0 and D≥0D\ge0 such that for every p∈Kp\in K:

  • the closed ball Bˉ(p,δ)\bar B(p,\delta) is contained in OO;
  • ∥f(y)∥≤D\|f(y)\|\le D for all y∈Bˉ(p,δ)y\in\bar B(p,\delta);
  • ∥f(y)−f(y′)∥≤D ∥y−y′∥\|f(y)-f(y')\|\le D\,\|y-y'\| for all y,y′∈Bˉ(p,δ)y,y'\in\bar B(p,\delta).

Role. Uniform size and Lipschitz constants for a C1C^1 coefficient field (such as an almost complex structure) on balls of a fixed radius centred anywhere in a compact set; used for estimates uniform in the centre point.

Preamble
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Topology.MetricSpace.Thickening
Formal statement
namespace FiniteEnergyPlane

open Metric Set

/-- Uniform bounds near a compact set. Let `f` be a `C¹` map on an open subset `O` of a
finite-dimensional real normed space and `K ⊆ O` compact. There are `δ > 0` and `D ≥ 0` such
that for every `p ∈ K` the closed ball `closedBall p δ` lies in `O`, `‖f y‖ ≤ D` on it, and `f` is
`D`-Lipschitz on it. -/
theorem exists_lipschitz_near_compact {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {O : Set E}
    (hO : IsOpen O) (hf : ContDiffOn ℝ 1 f O) {K : Set E} (hK : IsCompact K) (hKO : K ⊆ O) :
    ∃ δ > 0, ∃ D, 0 ≤ D ∧ ∀ p ∈ K, closedBall p δ ⊆ O ∧
      ∀ y ∈ closedBall p δ, ‖f y‖ ≤ D ∧ ∀ y' ∈ closedBall p δ, ‖f y - f y'‖ ≤ D * ‖y - y'‖ := by
  sorry

end FiniteEnergyPlane
Source
Standard (mean value inequality)

View graph