Samplinglib mathematical lesson

The Laplacian of a product

Read this first

Mathematical statement

Multiply two locally C² real functions, then take the Laplacian.

\[\begin{aligned}\Delta(fg)(x)&=f(x)\Delta g(x)\\&\quad+2\langle\nabla f(x),\nabla g(x)\rangle\\&\quad+g(x)\Delta f(x).\end{aligned}\]

Lean statement · laplacian_mul

Exact local-C2 signature; no global smoothness, integrability, harmonicity or positive-dimension assumption.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem laplacian_mul
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] {f g : E → ℝ} {x : E}
    (hf : ContDiffAt ℝ 2 f x) (hg : ContDiffAt ℝ 2 g x) :
    Laplacian.laplacian (fun z => f z * g z) x =
      f x * Laplacian.laplacian g x +
      2 * inner ℝ (gradient f x) (gradient g x) +
      g x * Laplacian.laplacian f x

Exact module and namespace context

A local calculus identity. Poisson integral values remain open.

Full assumptions and notation

All objects and hypotheses

\(E\) is a finite-dimensional real inner product space, and \(x\in E\). No positive-dimension premise is required. The source book works in \(\mathbb R^n\), \(n>1\); the canonical coordinate-independent form explicitly includes dimensions zero and one.
\(f,g:E\to\mathbb R\) are twice continuously differentiable locally at \(x\). The book identity applies to C² functions on their open domain. Here the local germ is sufficient; the former compact-graph implementation required global C² functions on E.
\(\nabla\) is the actual Riesz gradient and \(\Delta\) is the actual Euclidean Laplacian defined from the canonical covariant tensor and second Fréchet derivative. Neither is defined by the identity being proved.

Notation and interpretation

\(D_vf,\nabla f,\Delta f\): Directional derivative, the actual Riesz gradient, and the orthonormal trace of the second Fréchet derivative.
\[D_vf(x)=Df(x)[v]=\langle\nabla f(x),v\rangle,\qquad\Delta f(x)=\sum_i D^2f(x)[e_i,e_i].\]
\(P_\zeta\): Concrete consumer: the spherical Poisson kernel for a unit vector zeta. At points inside the unit ball the pole is excluded and local C² regularity is discharged internally. Its harmonicity and normalized surface integral are not yet concluded.
\[P_\zeta(z)=\frac{1-\|z\|_2^2}{\|z-\zeta\|_2^n},\qquad\|\zeta\|_2=1,\quad\|x\|_2<1\ \Longrightarrow\ x\ne\zeta.\]

Mathematical proof

Open a step to read its argument and formula.

1. Differentiate the product twice locally

Local C² regularity gives a neighborhood on which the first product rule holds. Differentiate that equality at x, in the same direction v twice. This produces the two cross terms without assuming global smoothness.

\[D_v^2(fg)(x)=f(x)D_v^2g(x)+2D_vf(x)D_vg(x)+g(x)D_v^2f(x).\]

Corresponding Lean step

second_product uses ContDiffAt.eventually, the actual first Fréchet product derivative, and EventuallyEq.fderiv_eq. directional_second identifies evaluation of the second Fréchet derivative.

2. Take the orthonormal trace

Choose an orthonormal basis, apply the directional identity to each basis vector, and sum. The Laplacian is this trace; the coefficients f(x) and g(x) are independent of the summation index.

\[\Delta(fg)(x)=f(x)\Delta g(x)+2\sum_i D_{e_i}f(x)D_{e_i}g(x)+g(x)\Delta f(x).\]

Corresponding Lean step

The local ht identity uses InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis and iteratedFDeriv_two_apply. Finset.sum_add_distrib and Finset.mul_sum collect the three terms.

3. Identify the gradient pairing

Parseval identifies the middle sum with the real inner product of the two actual gradients. In dimension zero the trace is empty and the gradients vanish; in dimension one this recovers the ordinary second-derivative product rule.

\[\sum_i D_{e_i}f(x)D_{e_i}g(x)=\langle\nabla f(x),\nabla g(x)\rangle.\]

Corresponding Lean step

The local hi identity calls OrthonormalBasis.sum_inner_mul_inner, inner_gradient_left and inner_gradient_right. The same finite sum proof includes empty and singleton bases; no Nontrivial assumption is added.

Lean verification

Lean proof · laplacian_mul

Differentiate in one direction twice, take the orthonormal trace, and apply Parseval.

Download module (.lean)

theorem laplacian_mul
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] {f g : E → ℝ} {x : E}
    (hf : ContDiffAt ℝ 2 f x) (hg : ContDiffAt ℝ 2 g x) :
    Laplacian.laplacian (fun z => f z * g z) x =
      f x * Laplacian.laplacian g x +
      2 * inner ℝ (gradient f x) (gradient g x) +
      g x * Laplacian.laplacian f x := by
  have ht (h : E → ℝ) : Laplacian.laplacian h x =
      ∑ i, fderiv ℝ (fderiv ℝ h) x
        ((stdOrthonormalBasis ℝ E) i) ((stdOrthonormalBasis ℝ E) i) := by
    rw [InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis]
    apply Finset.sum_congr rfl
    intro i _
    rw [iteratedFDeriv_two_apply]
    rfl
  have hi : inner ℝ (gradient f x) (gradient g x) =
      ∑ i, fderiv ℝ f x ((stdOrthonormalBasis ℝ E) i) *
        fderiv ℝ g x ((stdOrthonormalBasis ℝ E) i) := by
    rw [← (stdOrthonormalBasis ℝ E).sum_inner_mul_inner (gradient f x) (gradient g x)]
    simp only [inner_gradient_left, inner_gradient_right, conj_trivial]
  rw [ht, ht, ht, hi]
  simp_rw [second_product hf hg]
  simp only [Finset.sum_add_distrib, ← Finset.mul_sum]

end AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LaplacianProduct

Exact module and namespace context

Scope and omitted-condition boundaries

Local differential identity only. The actual Poisson kernel product expansion and the existing compact smooth-graph consumer reuse this same node. Poisson harmonicity, sphere mean-value/normalization, both AppendixA1 numerical integrals, Eq24, actual TV/oracle/query/cost and main lower bounds remain separate. No weighted core or other PBPS/SPHMC completion follows.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ContDiffAt.eventually
ContDiffAt.fderiv_right
HasFDerivAt.mul
HasFDerivAt.clm_apply
Filter.EventuallyEq.fderiv_eq
InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis
iteratedFDeriv_two_apply
OrthonormalBasis.sum_inner_mul_inner
inner_gradient_left
inner_gradient_right

Mathematical sources

Axler–Bourdon–Ramey, Eq1.19: Laplacian product rule — Local differential identity only. The actual Poisson kernel product expansion and the existing compact smooth-graph consumer reuse this same node. Poisson harmonicity, sphere mean-value/normalization, both AppendixA1 numerical integrals, Eq24, actual TV/oracle/query/cost and main lower bounds remain separate. No weighted core or other PBPS/SPHMC completion follows.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.