Local Lipschitz Product Rule with a Bounded Factor

Proved

FunctionalInequalities.Energy.locallyLipschitz_mul_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement proves a local Lipschitz product rule.

Let $V$ be a normed additive commutative group, let $g,h:V\to\mathbb R$ , and let $N\in[0,\infty)$ . Assume:

$g$ is locally Lipschitz.
$h$ is globally $N$ -Lipschitz.
$|h(x)|\leq 1$ for every $x\in V$ .

Then the pointwise product is locally Lipschitz:

x\mapsto g(x)h(x)\quad\text{is locally Lipschitz on }V.

This is a technical reduction lemma for constructing locally Lipschitz cutoffs and products; no inner-product or finite-dimensional assumption is part of the statement.

Original Lean declaration header

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

theorem locallyLipschitz_mul {g h : V → ℝ} {N : ℝ≥0} (hg : LocallyLipschitz g)
    (hh : LipschitzWith N h) (hh1 : ∀ x, |h x| ≤ 1) :
    LocallyLipschitz (fun x ↦ g x * h x)

Module navigation

Module: Energy/Euclidean/Slope/Recovery.

Next: exists_lipschitzWith_of_eq_zero_outside_ball.

Source excerpt, lines 201–203 · 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.locallyLipschitz_mul_readable {g h : V → ℝ} {N : ℝ≥0} (hg : LocallyLipschitz g)
    (hh : LipschitzWith N h) (hh1 : ∀ x, |h x| ≤ 1) :
    LocallyLipschitz (fun x ↦ g x * h x) := by sorry

Source

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

View graph