Local-Slope Product Bound With A Bounded Lipschitz Factor

Proved

FunctionalInequalities.Energy.LocalSlope.apply_mul_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a one-moving-point product estimate for the local slope.

Let $V$ be a normed additive group, let $g,h:V\to\mathbb R$ , and let $N\in[0,\infty)$ be represented by NNReal. Assume that $h$ is globally $N$ -Lipschitz and bounded in absolute value by one:

\operatorname{LipschitzWith}(N,h), \qquad |h(y)|\le 1\quad\text{for every }y\in V.

Then for every $x\in V$ ,

\operatorname{apply}(y\mapsto g(y)h(y),x) \le \operatorname{apply}(g,x)+\operatorname{ENNReal.ofReal}(|g(x)|)\,N.

The declaration is apply_mul_le_readable. The target values are in $[0,\infty]$ ; no inner-product, completeness, or finite-dimensionality assumptions are part of the statement.

Original Lean declaration header

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

theorem apply_mul_le (g h : V → ℝ) {N : ℝ≥0} (hh : LipschitzWith N h)
    (hh1 : ∀ y, |h y| ≤ 1) (x : V) :
    apply (fun y ↦ g y * h y) x ≤ apply g x + ENNReal.ofReal |g x| * N

Module navigation

Module: Energy/Euclidean/Slope/Recovery.

Definition modules: Energy/LocalSlope/Basic.

Previous: exists_lipschitzWith_of_eq_zero_outside_ball · Next: lipschitzOnWith_mollify_ball.

Source excerpt, lines 403–405 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_Slope_Recovery

open scoped ENNReal NNReal ContDiff
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
omit [InnerProductSpace ℝ V]

Formal statement


theorem FunctionalInequalities.Energy.LocalSlope.apply_mul_le_readable (g h : V → ℝ) {N : ℝ≥0} (hh : LipschitzWith N h)
    (hh1 : ∀ y, |h y| ≤ 1) (x : V) :
    apply (fun y ↦ g y * h y) x ≤ apply g x + ENNReal.ofReal |g x| * N := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Euclidean/Slope/Recovery.lean#L400-L446 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Euclidean.Slope.Recovery`, declaration `FunctionalInequalities.Energy.LocalSlope.apply_mul_le`; the repository is private at upload time).

View graph