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.
The Laplace fundamental solution is harmonic off its pole
Statement
Assume Countable Choice and . The displayed is smooth on and satisfies there; for every pole , is harmonic on .
Facts & Assumptions
Given: , , and the kernel with the normalization fixed in Fundamental solution for the positive operator minus Laplacian.
Countable Choice, written , is the assumption retained from the kernel convention (The Axiom of Countable Choice ()). The differentiation argument below does not use choice.
For , away from zero; for , (Fundamental solution for the positive operator minus Laplacian).
A scalar function is when all iterated coordinate derivatives through order exist and are continuous ( maps and multi-index derivative notation in Euclidean space).
A Euclidean map is when each component is ( Euclidean maps and diffeomorphisms).
Finite sums and products and compositions of Euclidean maps are ( Euclidean maps are closed under componentwise algebra and composition).
The total chain rule gives (The chain rule for total derivatives: ).
A total derivative's matrix gives the coordinate partial derivatives (A total derivative computes every directional derivative, and its matrix is the Jacobian).
For , for every real (Continuity and derivatives of positive-base real powers).
Sums, products and scalar multiples obey the derivative rules (Sums, scalar multiples, products and quotients: , , , and when ).
The Laplacian is the sum of the pure second coordinate partials (The Laplacian of a function and of a vector field).
A function whose Laplacian vanishes is harmonic (The Laplacian of a function and of a vector field).
Induction on the natural numbers proves a property once its base case and successor step hold (The principle of mathematical induction).
Proof
For any real , induction on using [F12] and [F7] gives on , where and . Each derivative is continuous by the real-power continuity in [F7], so is smooth under [F2]. Also by [F8]; applying the same derivative calculation to shows every higher derivative of exists and is continuous. Thus both radial profiles used in [F1] are smooth for .
On , put . Its coordinate functions and their finite sums and products are smooth by direct coordinate differentiation and [F2]–[F4]. Since on , the radius is smooth there by [F7], step 1.1, and closure under composition [F4]. Composing with the power profile for or the logarithm profile for proves that is smooth on .
For a smooth radial profile and , the chain rule [F5] and partial-derivative formula [F6] give . Differentiating again by the chain and product rules [F5], [F7] and [F9] gives . Summing over and using and the Laplacian definition [F10] yields . The calculation is on , where all derivatives used exist by steps 1.1 and 2.1.
If , set . Then and by [F7] and [F9], so step 3.1 gives . If , set . Then by [F8]–[F9] and by applying [F7] to ; hence . These cases exhaust .
For fixed , translation has affine coordinate functions, so direct differentiation gives its identity derivative and zero higher derivatives. The chain rule [F5] therefore gives whenever . The translated function is smooth there by [F4], hence is harmonic by [F11]. The assumption in [A1] is carried from the kernel convention but is not used in these pointwise derivative calculations.
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Fundamental solution for the positive operator minus Laplacian
- The Laplacian of a $C^2$ function and of a $C^2$ vector field
- $C^k$ maps and multi-index derivative notation in Euclidean space
- $C^k$ Euclidean maps and diffeomorphisms
- $C^k$ Euclidean maps are closed under componentwise algebra and composition
- The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$
- A total derivative computes every directional derivative, and its matrix is the Jacobian
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- Continuity and derivatives of positive-base real powers
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- The principle of mathematical induction
Used by
- An isolated boundary point obstructs pointwise-zero Green data Counterexample
- Dirichlet Green function for minus Laplacian Definition
- Poisson kernel from a Dirichlet Green function Definition
- Newton shell theorem from harmonic mean values Example
- Green representation for classical Poisson data Theorem
- Newtonian potentials solve the distributional Poisson equation Theorem
- Symmetry of the Dirichlet Green function Theorem
- The negative Laplacian of the fundamental solution is the unit Dirac distribution Theorem
Dependency tree · two levels
62 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
- John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)
- Thomas Schmidt, Partial Differential Equations I (2026) (standard reference, not scraped)