Gradient Class Norm Equals Dirichlet Energy

Proved

FunctionalInequalities.KLS.LogConcave.norm_toLp_gradient_sq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement identifies the squared $L^2(\nu)$ norm of a classical gradient with its integrated Dirichlet energy.

Let $V$ be a complete real inner-product space with the stated measurable and second-countable structures, let $\nu$ be a probability measure, and let $f:V\to\mathbb R$ be smooth of class $C^\infty$ with compact support. Then

\|[\nabla f]_{L^2(\nu)}\|^2 =\int_V\|\nabla f(x)\|^2\,d\nu(x) =\int_V\Gamma(f,f)(x)\,d\nu(x).

The identity supplies the standard correspondence between the $L^2$ gradient norm and the Dirichlet energy in the heat-semigroup formalization.

Formalization Note. No finite-dimensionality assumption is present in the declaration. The gradient class is obtained through MemLp.toLp; the integrals are ordinary real-valued integrals.

Original Lean declaration header

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

theorem norm_toLp_gradient_sq {f : V → ℝ} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    ‖(memLp_gradient_of_contDiff_hasCompactSupport (ν := ν) hf hfc).toLp (gradient f)‖ ^ 2 =
      ∫ x, gamma f f x ∂(ν : Measure V)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

Definition modules: Analysis/BakryEmery/Gamma, KLS/LogConcave/HeatSemigroup/Generator.

Next: mul_norm_closedWeightedOperator_toLp_sq_le.

Source excerpt, lines 52–54 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open MeasureTheory Filter Topology InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)
omit [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.norm_toLp_gradient_sq_readable {f : V → ℝ} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    ‖(memLp_gradient_of_contDiff_hasCompactSupport (ν := ν) hf hfc).toLp (gradient f)‖ ^ 2 =
      ∫ x, gamma f f x ∂(ν : Measure V) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Curvature.lean#L50-L73 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Curvature`, declaration `FunctionalInequalities.KLS.LogConcave.norm_toLp_gradient_sq`; the repository is private at upload time).

View graph