How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Smooth sphere data have a harmonic replacement
Statement
Let , , , and be real. Write . There is a unique harmonic inside and equal to on the sphere. It is The kernel is positive and has integral one at each interior point.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
A real function is harmonic when the sum of its pure second derivatives, its Laplacian, vanishes. (The Laplacian of a function and of a vector field).
and is finite and positive. (Sphere and ball measures scale in Rn).
A classical harmonic function equals its sphere average on every compactly contained ball. (Spherical mean-value property for harmonic functions).
Classical harmonic functions continuous on a bounded open set’s closure and sharing boundary data agree. (Uniqueness for the classical dirichlet problem).
For measurable functions converging almost everywhere under a single integrable absolute majorant, dominated convergence permits passing their limit through the integral. (Dominated convergence).
Proof
Translate to zero. Put , , and , where . The sphere has finite positive measure . On compact interior sets is bounded away from zero; all -derivatives of the kernel times bounded have a constant integrable majorant. The mean value theorem bounds their difference quotients likewise. Dominated convergence therefore permits differentiation of every order under the sphere integral and proves continuity of those derivatives.
Cartesian differentiation gives , and . The product rule gives . Thus both and are smooth harmonic functions.
Rotation invariance of surface measure and the kernel makes constant on each sphere centered at zero. Its spherical mean equals by harmonic mean values; since it is already constant on that sphere, . At zero, , so . Also in the ball.
Fix . The mass identity gives . For a given , take so that when . That part of the integral has absolute value at most . On the remaining sphere, if , then , and uniformly tends to zero. The remaining integral is bounded by this supremum times . Thus , proving continuity on the closed ball.
Any two such harmonic replacements have identical boundary data on a bounded ball and are continuous on its closure, so classical Dirichlet uniqueness makes them equal. Translation restores the stated formula at .
Depends on
Used by
Dependency tree · two levels
21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gantumur, Harmonic functions (standard reference, not scraped)