Global Lipschitzness of Locally Lipschitz Compactly Supported Functions

Proved

FunctionalInequalities.Energy.exists_lipschitzWith_of_eq_zero_outside_ball_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement is the bounded-support Lipschitz principle.

Let $V$ be a finite-dimensional real inner-product space, let $g:V\to\mathbb R$ be locally Lipschitz, and let $R\in\mathbb R$ . Assume that $g$ vanishes outside the closed ball of radius $R$ centered at the origin, in the sense that

R\leq\|x\|\quad\Longrightarrow\quad g(x)=0

for every $x\in V$ .

Then there exists some $K\in[0,\infty)$ such that $g$ is globally $K$ -Lipschitz:

\exists K\in[0,\infty),\qquad \operatorname{LipschitzWith}(K,g).

The conclusion is existential and does not specify a particular Lipschitz constant. It supplies a standard reduction from locally Lipschitz functions with bounded support to globally Lipschitz tests.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy. Shown in its original module context. Proof omitted.

theorem exists_lipschitzWith_of_eq_zero_outside_ball {g : V → ℝ} {R : ℝ}
    (hg : LocallyLipschitz g) (hR : ∀ x, R ≤ ‖x‖ → g x = 0) :
    ∃ K : ℝ≥0, LipschitzWith K g

Module navigation

Module: Energy/Euclidean/Slope/Recovery.

Previous: locallyLipschitz_mul · Next: apply_mul_le.

Source excerpt, lines 251–253 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_Slope_Recovery

open scoped ENNReal NNReal ContDiff
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.Energy.exists_lipschitzWith_of_eq_zero_outside_ball_readable {g : V → ℝ} {R : ℝ}
    (hg : LocallyLipschitz g) (hR : ∀ x, R ≤ ‖x‖ → g x = 0) :
    ∃ K : ℝ≥0, LipschitzWith K g := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Euclidean/Slope/Recovery.lean#L250-L300 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Euclidean.Slope.Recovery`, declaration `FunctionalInequalities.Energy.exists_lipschitzWith_of_eq_zero_outside_ball`; the repository is private at upload time).

View graph