Normal contractions for Dirichlet-form structures

Definition

KLSModular_FunctionalInequalities_Energy_Form_Dirichlet

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Energy.NormalContraction is a structure consisting of a function $\varphi:\mathbb R\to\mathbb R$ , a Lipschitz bound LipschitzWith 1 φ, and the normalization $\varphi(0)=0$ . Its coercion lets such a contraction be used as a real-valued function. This bundle defines the contraction object only; it does not state a Dirichlet form or a Markov inequality.

Original module imports

import FunctionalInequalities.Energy.Form.ClosedQuadratic
import Mathlib.MeasureTheory.Function.LpSpace.Basic

Original declaration excerpt

Shown in the original module context.

structure NormalContraction where
  /-- The underlying real function. -/
  toFun : ℝ → ℝ
  /-- The contraction estimate. -/
  lipschitz : LipschitzWith 1 toFun
  /-- Normalization at zero. -/
  map_zero : toFun 0 = 0

Module navigation

Direct project imports: Energy/Form/ClosedQuadratic.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Energy.Form.Dirichlet · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Form_ClosedQuadratic
import Mathlib.MeasureTheory.Function.LpSpace.Basic

noncomputable section
open MeasureTheory
namespace FunctionalInequalities
namespace Energy
/-- A normal contraction of the real line: it fixes zero and has Lipschitz constant at most one. -/
structure NormalContraction where
  /-- The underlying real function. -/
  toFun : ℝ → ℝ
  /-- The contraction estimate. -/
  lipschitz : LipschitzWith 1 toFun
  /-- Normalization at zero. -/
  map_zero : toFun 0 = 0
namespace NormalContraction
instance : CoeFun NormalContraction fun _ ↦ ℝ → ℝ :=
  ⟨NormalContraction.toFun⟩
end NormalContraction
end Energy
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Form/Dirichlet.lean#L19-L31 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Form.Dirichlet`, definition bundle `KLSModular_FunctionalInequalities_Energy_Form_Dirichlet`; the repository is private at upload time).

View graph