Lipschitz cutoff on a norm ball

Definition

KLSModular_FunctionalInequalities_Analysis_Cutoff_LipschitzBall

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Probability.Diffusion.ballCutoff R p is the scalar cutoff $\max(0,\min(1,R+1-\|p\|))$ on a finite-dimensional real normed space. It is the piecewise-linear norm-ball cutoff taking values between $0$ and $1$ , although this bundle only supplies the definition.

Original module imports

import Mathlib.Topology.EMetricSpace.Lipschitz
import Mathlib.Topology.Algebra.MetricSpace.Lipschitz
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Topology.Algebra.Support

Original declaration excerpt

Shown in the original module context.

noncomputable def ballCutoff (R : ℝ) (p : V) : ℝ := max 0 (min 1 (R + 1 - ‖p‖))

Module navigation

Theorems in source order:

exists_lipschitzWith_smul_of_locallyLipschitz

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Cutoff.LipschitzBall · Frozen source 408915f.

Definition code

import Mathlib.Topology.EMetricSpace.Lipschitz
import Mathlib.Topology.Algebra.MetricSpace.Lipschitz
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Topology.Algebra.Support

noncomputable section
open scoped NNReal
namespace FunctionalInequalities
namespace Probability
namespace Diffusion
section Cutoff
variable {V V' : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
  [NormedAddCommGroup V'] [NormedSpace ℝ V']
/-- The norm-ball cutoff `γ_R = clamp₀¹(R + 1 − ‖p‖)`. -/
noncomputable def ballCutoff (R : ℝ) (p : V) : ℝ := max 0 (min 1 (R + 1 - ‖p‖))
end Cutoff
end Diffusion
end Probability
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Cutoff/LipschitzBall.lean#L22-L23 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Cutoff.LipschitzBall`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Cutoff_LipschitzBall`; the repository is private at upload time).

View graph