Prove2Me

Almost-Everywhere Invariance of Weak Directional Derivatives

Proved
FunctionalInequalities.Analysis.HasWeakDerivAlong.congr_ae_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This is the almost-everywhere congruence principle for weak directional derivatives. It is listed as a partial formalization of Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let EE be a finite-dimensional real inner-product space with its Borel measurable structure. Let f,f′,g,g′:E→Rf,f',g,g':E\to\mathbb{R} and v∈Ev\in E. Assume HasWeakDerivAlong f g v, and suppose

f=f′a.e. with respect to volume,f=f'\quad\text{a.e. with respect to volume}, g=g′a.e. with respect to volume.g=g'\quad\text{a.e. with respect to volume}.

Then

HasWeakDerivAlong⁡(f′,g′,v).\operatorname{HasWeakDerivAlong}(f',g',v).

The result permits replacing both a function and its weak derivative by almost-everywhere equal representatives.

Original Lean declaration header

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

theorem HasWeakDerivAlong.congr_ae {E : Type u}
    [instNormedAddCommGroup : NormedAddCommGroup E]
    [instInnerProductSpace : InnerProductSpace ℝ E]
    [instFiniteDimensional : FiniteDimensional ℝ E]
    [instMeasurableSpace : MeasurableSpace E] [instBorelSpace : BorelSpace E]
    {f f' g g' : E → ℝ} {v : E}
    (h : HasWeakDerivAlong f g v)
    (hf : f =ᵐ[(volume : Measure E)] f')
    (hg : g =ᵐ[(volume : Measure E)] g') :
    HasWeakDerivAlong f' g' v

Module navigation

Module: Analysis/WeakDerivative/Basic.

Previous: HasWeakDerivAlong.mul_contDiff.

Source excerpt, lines 261–270 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Basic

open MeasureTheory
universe u
Formal statement

theorem FunctionalInequalities.Analysis.HasWeakDerivAlong.congr_ae_readable {E : Type u}
    [instNormedAddCommGroup : NormedAddCommGroup E]
    [instInnerProductSpace : InnerProductSpace ℝ E]
    [instFiniteDimensional : FiniteDimensional ℝ E]
    [instMeasurableSpace : MeasurableSpace E] [instBorelSpace : BorelSpace E]
    {f f' g g' : E → ℝ} {v : E}
    (h : HasWeakDerivAlong f g v)
    (hf : f =ᵐ[(volume : Measure E)] f')
    (hg : g =ᵐ[(volume : Measure E)] g') :
    HasWeakDerivAlong f' g' v := by sorry
Source
Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Theorem 2.5. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/WeakDerivative/Basic.lean#L259-L288 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.WeakDerivative.Basic`, declaration `FunctionalInequalities.Analysis.HasWeakDerivAlong.congr_ae`; the repository is private at upload time).

View graph