Large-Measurable-Set Lipschitz Patch

Proved

FunctionalInequalities.Energy.LocalSlope.exists_patch_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem produces a globally Lipschitz approximation agreeing with a globally Lipschitz function on most of a probability space.

Let $V$ be a finite-dimensional real inner-product normed space with its Borel measurable structure, let $\nu$ be a probability measure on $V$ , and let $f:V\to\mathbb R$ be globally $L$ -Lipschitz. Let $\alpha>0$ be represented by NNReal, and let $\delta>0$ be an ENNReal value. Then there exist a function $F:V\to\mathbb R$ and a measurable set $K\subseteq V$ such that

$F$ is globally $(9L+8\alpha)$ -Lipschitz;
$\nu(K^c)\le\delta$ ;
$F=f$ on $K$ ;
for every $x\in V$ ,

|F(x)-f(x)|\le 2L+2\alpha;

for every $x\in K$ ,

\operatorname{AsymptoticLipschitz.apply}(F,x) \le \operatorname{apply}(f,x)+2\alpha.

The declaration is exists_patch_readable. The measure bound and slope comparison use $[0,\infty]$ values (ENNReal), and the conclusion is existential for each strictly positive $\alpha$ and $\delta$ .

Original Lean declaration header

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

theorem exists_patch (ν : ProbabilityMeasure V) {f : V → ℝ} {L : ℝ≥0} (hf : LipschitzWith L f)
    {α : ℝ≥0} (hα : 0 < α) {δ : ℝ≥0∞} (hδ : 0 < δ) :
    ∃ (F : V → ℝ) (K : Set V), LipschitzWith (9 * L + 8 * α) F ∧ MeasurableSet K ∧
      (ν : Measure V) Kᶜ ≤ δ ∧ (∀ x ∈ K, F x = f x) ∧
      (∀ x, |F x - f x| ≤ 2 * (L : ℝ) + 2 * (α : ℝ)) ∧
      ∀ x ∈ K, AsymptoticLipschitz.apply F x ≤ apply f x + 2 * (α : ℝ≥0∞)

Module navigation

Module: Energy/Euclidean/Slope/Density.

Definition modules: Energy/LocalSlope/Basic, Energy/LocalSlope/Relaxation.

Supporting theorems: exists_partition, exists_patch_of_isCompact.

Previous: exists_partition · Next: relaxation_le_localSlope_of_lipschitzWith.

Source excerpt, lines 685–690 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_Slope_Density

open MeasureTheory Filter Topology Set
open scoped ENNReal NNReal ContDiff
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
omit [CompleteSpace V]

Formal statement


theorem FunctionalInequalities.Energy.LocalSlope.exists_patch_readable (ν : ProbabilityMeasure V) {f : V → ℝ} {L : ℝ≥0} (hf : LipschitzWith L f)
    {α : ℝ≥0} (hα : 0 < α) {δ : ℝ≥0∞} (hδ : 0 < δ) :
    ∃ (F : V → ℝ) (K : Set V), LipschitzWith (9 * L + 8 * α) F ∧ MeasurableSet K ∧
      (ν : Measure V) Kᶜ ≤ δ ∧ (∀ x ∈ K, F x = f x) ∧
      (∀ x, |F x - f x| ≤ 2 * (L : ℝ) + 2 * (α : ℝ)) ∧
      ∀ x ∈ K, AsymptoticLipschitz.apply F x ≤ apply f x + 2 * (α : ℝ≥0∞) := by sorry

Source

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

View graph