Weak Product Rule Under Global $L^2$ Bounds

Proved

FunctionalInequalities.Analysis.HasWeakDerivAlong.mul_of_memLp_two_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This is the scalar weak product rule under global $L^2$ hypotheses. It is listed as a partial formalization of Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $n\in\mathbb{N}$ , let $f,df,g,dg:\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)\to\mathbb{R}$ , and let $v$ be a vector in that space. Assume:

HasWeakDerivAlong f df v.
HasWeakDerivAlong g dg v.
$f,df,g,dg$ all belong to global $L^2(\operatorname{volume})$ .

Then

\operatorname{HasWeakDerivAlong}\bigl(x\mapsto f(x)g(x),\ x\mapsto df(x)g(x)+f(x)dg(x),\ v\bigr).

The conclusion is a weak directional derivative statement for the product, with no almost-everywhere qualification added to the displayed representative.

Original Lean declaration header

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

theorem HasWeakDerivAlong.mul_of_memLp_two {n : ℕ}
    {f df g dg : EuclideanSpace ℝ (Fin n) → ℝ}
    {v : EuclideanSpace ℝ (Fin n)}
    (hf : HasWeakDerivAlong f df v) (hg : HasWeakDerivAlong g dg v)
    (hf2 : MemLp f 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hdf2 : MemLp df 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hg2 : MemLp g 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hdg2 : MemLp dg 2 (volume : Measure (EuclideanSpace ℝ (Fin n)))) :
    HasWeakDerivAlong (fun x => f x * g x)
      (fun x => df x * g x + f x * dg x) v

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: lintegral_enorm_convolution_sq_le, tendsto_eLpNorm_convolution_sub, fderiv_convolution_eq_of_hasWeakDerivAlong.

Next: memLp_mul_of_hasCompactSupport.

Source excerpt, lines 55–64 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Calculus

open MeasureTheory Filter Set Metric InnerProductSpace
set_option maxHeartbeats 800000

Formal statement


theorem FunctionalInequalities.Analysis.HasWeakDerivAlong.mul_of_memLp_two_readable {n : ℕ}
    {f df g dg : EuclideanSpace ℝ (Fin n) → ℝ}
    {v : EuclideanSpace ℝ (Fin n)}
    (hf : HasWeakDerivAlong f df v) (hg : HasWeakDerivAlong g dg v)
    (hf2 : MemLp f 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hdf2 : MemLp df 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hg2 : MemLp g 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hdg2 : MemLp dg 2 (volume : Measure (EuclideanSpace ℝ (Fin n)))) :
    HasWeakDerivAlong (fun x => f x * g x)
      (fun x => df x * g x + f x * dg x) 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/Calculus.lean#L52-L181 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.WeakDerivative.Calculus`, declaration `FunctionalInequalities.Analysis.HasWeakDerivAlong.mul_of_memLp_two`; the repository is private at upload time).

View graph

Weak Product Rule Under Global L2L^2L2 Bounds

Weak Product Rule Under Global $L^2$ Bounds