Smoothness and Second Derivative of the Affine-Orthogonal Part

Proved

FunctionalInequalities.L2.contDiff_affineOrthPart_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma states that subtracting the prescribed affine part preserves $C^2$ regularity and the second derivative.

Let $n\in\mathbb N$ , $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), $\mu$ any measure on $E$ , and $g:E\to\mathbb R$ a $C^2$ function. For the standard orthonormal basis $(e_j)_{j\in\operatorname{Fin}n}$ , define

\widetilde g(x)=g(x)-\int g\,d\mu-\sum_j\left(\int\langle e_j,y\rangle g(y)\,d\mu(y)\right)\langle e_j,x\rangle

using affineOrthPart. Then

\widetilde g\in C^2(E),\qquad \forall x\in E,\quad D(D\widetilde g)(x)=D(Dg)(x).

The second derivatives here are the iterated Fréchet derivatives fderiv. This result transfers bounded-second-derivative conditions to the affine-subtracted function.

Formalization Note No probability, moment, or integrability assumptions on $\mu$ or $g$ are present. The defining integrals use Lean's total Bochner integral; the lemma does not assert orthogonality under these unrestricted hypotheses.

Original Lean declaration header

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

theorem contDiff_affineOrthPart (μ : Measure (EuclideanSpace ℝ (Fin n)))
    {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ContDiff ℝ 2 g) :
    ContDiff ℝ 2 (affineOrthPart μ g) ∧
      ∀ x, fderiv ℝ (fderiv ℝ (affineOrthPart μ g)) x = fderiv ℝ (fderiv ℝ g) x

Module navigation

Module: L2/AffineDecomposition.

Previous: sub_affineOrthPart_eq · Next: integral_affineOrthPart_mul_sub.

Source excerpt, lines 530–533 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_L2_AffineDecomposition

open MeasureTheory
variable {n : ℕ}

Formal statement


theorem FunctionalInequalities.L2.contDiff_affineOrthPart_readable (μ : Measure (EuclideanSpace ℝ (Fin n)))
    {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ContDiff ℝ 2 g) :
    ContDiff ℝ 2 (affineOrthPart μ g) ∧
      ∀ x, fderiv ℝ (fderiv ℝ (affineOrthPart μ g)) x = fderiv ℝ (fderiv ℝ g) x := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/L2/AffineDecomposition.lean#L529-L592 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.L2.AffineDecomposition`, declaration `FunctionalInequalities.L2.contDiff_affineOrthPart`; the repository is private at upload time).

View graph