Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

The Laplacian of a product

Sheldon Axler, Paul Bourdon and Wade Ramey. ASTIS states the coordinate-independent local form and explicitly extends the standing source dimension n>1 to all finite real Hilbert spaces.

Harmonic Function Theory, second edition (author-hosted PDF SHA256 4e64124f7e36993ee784e575a024505f99d484ccf959d2d3864eae9232af8bf1) · Printed page13/PDF page21, Eq1.19; the product rule used in Proposition1.18. Downstream use in Proposition1.20(b), Theorem1.21 and arXiv2610.20492v1 AppendixA1 remains open. · faithful paraphrase

Complete source statement and conditions

Canonical local form of Eq1.19: for a finite-dimensional real inner product space \(E\), including dimensions zero and one, a point \(x\in E\), and real functions \(f,g\) which are C² locally at \(x\), the actual Laplacian and Riesz gradients satisfy \(\Delta(fg)(x)=f(x)\Delta g(x)+2\langle\nabla f(x),\nabla g(x)\rangle+g(x)\Delta f(x)\). The book states the real product rule for C² functions on their open domain in its standing dimension \(n>1\); the displayed canonical form localizes at one point and makes the low-dimensional extension explicit. It asserts no harmonicity or integral value.

  • \(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.

Local-C2 product rule

\[\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}\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

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.

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 := 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

Source correspondence and review

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Eq1.19: real C² observables on an open domain, under standing Euclidean n>1.ContDiffAt R2 for both observables at x on an arbitrary finite real Hilbert space, including dimensions0/1.generalizationThe proof uses only the germ at x; orthonormal trace and Riesz gradients remove coordinate choices. Empty/singleton basis cases are retained. The book is not claimed to state these low-dimensional interfaces.
Prop1.18 multiplies 1-norm(x)^2 by norm(x-zeta)^(-n) away from the unit pole.The concrete literal quotient kernel consumer discharges local C² inside the unit ball; no global C²-at-the-pole premise is imposed.source-implicitA consumer regularity discharge, not a proof of harmonicity or either Poisson value.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • assumptions: Faithful paraphrase is a publication wording enum, while the actual source text explicitly presents a canonical local/coordinate-independent extension beyond the book standing n>1. The low-dimensional/local extension remains a proved generalization and is not silently attributed to the raw book. — Current publication source.attribution, source scope, statement, assumptions and candidate_assumptions; pinned HFT printed1,2,13.
  • conclusion: Raw source suggests using Eq1.19 to compute Poisson harmonicity. The current genuine quotient consumer gives only product expansion and leaves derivative evaluation/cancellation and all integral values separate. — Printed13/PDF21 reader-calculation paragraph; actual Tests.GaussianComplexityPoissonProduct conclusion; current reader notation and boundary.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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.

    Which proof obligations and prerequisites are covered?

    • TODO — not closed by these contributions Multiply two locally C² real functions, then take the Laplacian.