Smooth directional derivative helper

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Hessian

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

contDiff_fderiv_apply_infty states that if $f:V\to\mathbb{R}$ is $C^\infty$ , then for every fixed $v\in V$ the function $y\mapsto Df(y)[v]$ is also $C^\infty$ . It is a technical regularity lemma supporting the weak Hessian and curvature-form development; the module's larger statements concern the closed heat-model gradient and its domain.

Original module imports

import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity
import FunctionalInequalities.Analysis.BakryEmery.Bochner.Temperate
import FunctionalInequalities.KLS.LogConcave.Density.Tilted

Original declaration excerpt

Shown in the original module context.

private theorem contDiff_fderiv_apply_infty {f : V → ℝ} (hf : ContDiff ℝ ∞ f) (v : V) :
    ContDiff ℝ ∞ (fun y => fderiv ℝ f y v) :=
  ((contDiff_infty_iff_fderiv.mp hf).2).clm_apply contDiff_const

Module navigation

Direct project imports: KLS/LogConcave/HeatSemigroup/InteriorRegularity, Analysis/BakryEmery/Bochner/Temperate, KLS/LogConcave/Density/Tilted.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Hessian · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_InteriorRegularity
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Bochner_Temperate
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_Tilted

noncomputable section
open MeasureTheory Filter Topology InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
open Energy Energy.WeightedGradient
section Partial
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
/-- A directional derivative of a smooth function is smooth. -/
 theorem contDiff_fderiv_apply_infty {f : V → ℝ} (hf : ContDiff ℝ ∞ f) (v : V) :
    ContDiff ℝ ∞ (fun y => fderiv ℝ f y v) :=
  ((contDiff_infty_iff_fderiv.mp hf).2).clm_apply contDiff_const
variable [CompleteSpace V] [FiniteDimensional ℝ V]
end Partial
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Hessian.lean#L64-L67 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Hessian`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Hessian`; the repository is private at upload time).

View graph