Prove2Me

Product Rule for the Laplacian

Proved
FunctionalInequalities.Analysis.BakryEmery.laplacian_mul_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem is the pointwise product rule for the Euclidean Laplacian.

Let EE be a finite-dimensional complete real inner-product space, let f,g:E→Rf,g:E\to\mathbb R be twice continuously differentiable, and let x∈Ex\in E. Then

Δ(fg)(x)=f(x)Δg(x)+g(x)Δf(x)+2⟨∇f(x),∇g(x)⟩.\Delta(fg)(x)=f(x)\Delta g(x)+g(x)\Delta f(x)+2\langle\nabla f(x),\nabla g(x)\rangle.

The identity is a local calculus tool and involves no measure, integrability, or curvature assumptions.

Original Lean declaration header

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

theorem laplacian_mul {f g : E → ℝ} (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) (x : E) :
    Laplacian.laplacian (fun y => f y * g y) x =
      f x * Laplacian.laplacian g x + g x * Laplacian.laplacian f x +
        2 * ⟪gradient f x, gradient g x⟫

Module navigation

Module: Analysis/BakryEmery/Calculus.

Source excerpt, lines 594–597 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Calculus

open scoped ContDiff RealInnerProductSpace
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E]
variable [CompleteSpace E]
Formal statement

theorem FunctionalInequalities.Analysis.BakryEmery.laplacian_mul_readable {f g : E → ℝ} (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) (x : E) :
    Laplacian.laplacian (fun y => f y * g y) x =
      f x * Laplacian.laplacian g x + g x * Laplacian.laplacian f x +
        2 * ⟪gradient f x, gradient g x⟫ := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Calculus.lean#L593-L620 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Calculus`, declaration `FunctionalInequalities.Analysis.BakryEmery.laplacian_mul`; the repository is private at upload time).

View graph