LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Gaussian screened Coulomb kernel and its self limit

Statement

Assume Countable Choice. For $α > 0$ , define $g_{α} (x) = \frac{α^{3}}{π^{3 / 2}} e^{- α^{2} ∣ x ∣^{2}}, \erf (s) = \frac{2}{\sqrt{π}} \int_{0}^{s} e^{- t^{2}} d t, erfc (s) = 1 - \erf (s) .$ Here $Δ = \sum_{j = 1}^{3} \partial_{x_{j}}^{2}$ , $δ_{0}$ is the distribution $⟨ δ_{0}, φ ⟩ = φ (0)$ , and a test function is a smooth compactly supported function $φ$ . For $r = ∣ x ∣ > 0$ put $ϕ_{ℓ} (r) = \erf (α r) / r$ and $ϕ_{s} (r) = erfc (α r) / r$ . Then $ϕ_{ℓ}$ extends continuously to $r = 0$ , $- Δ ϕ_{ℓ} = 4 π g_{α}$ distributionally on $R^{3}$ , and $- Δ ϕ_{s} = 4 π δ_{0} - 4 π g_{α}$ . Moreover, for every $s \geq 0$ , $erfc (s) = \frac{2}{\sqrt{π}} \int_{s}^{\infty} e^{- t^{2}} d t,$ $ϕ_{s} (r) = \frac{1}{r} - \frac{2 α}{\sqrt{π}} + O (r^{2}) (r ↓ 0),$ and for every $r > 0$ , $0 \leq ϕ_{s} (r) \leq \frac{e^{- α^{2} r^{2}}}{\sqrt{π} α r^{2}}, ∣ ϕ_{s}^{'} (r) ∣ \leq \frac{2 α}{\sqrt{π}} \frac{e^{- α^{2} r^{2}}}{r} + \frac{e^{- α^{2} r^{2}}}{\sqrt{π} α r^{3}} .$

Facts & Assumptions

Given: Countable Choice, $α > 0$ , a point $x \in R^{3}$ , $r = ∣ x ∣$ , and an arbitrary $φ \in C_{c}^{\infty} (R^{3})$ .

[A1]

Countable Choice is assumed in the local divergence theorem and its volume interfaces (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The bounded $C^{1}$ divergence theorem applies to punctured balls and smooth vector fields on their closures (Divergence on a bounded C1 Euclidean domain).

[F2]

The integral function of a continuous integrand has derivative equal to that integrand (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

[F3]

$\int_{- \infty}^{\infty} e^{- t^{2}} d t = \sqrt{π}$ (The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ ).

[F4]

Absolutely integrable products may be integrated by successive coordinates (Fubini's theorem for L^1 functions on a sigma-finite product).

[F5]

The chain rule differentiates $r \mapsto \erf (α r)$ using its derivative and $r \mapsto α r$ (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[F6]

For $f \in L^{1} (R)$ , the substitution $y = α x$ gives $\int_{R} f (y) d y = α \int_{R} f (α x) d x$ ; its Jacobian is $α > 0$ (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

Proof

technique · direct

1.1givenF2F5algebra

By [F2], $\erf^{'} (s) = 2 e^{- s^{2}} / \sqrt{π}$ , and [F5] gives $h^{'} (r) = 2 α e^{- α^{2} r^{2}} / \sqrt{π}$ for $h (r) = \erf (α r)$ . Differentiating again gives $h^{''} (r) = - 4 α^{3} r e^{- α^{2} r^{2}} / \sqrt{π}$ . Since $∣ e^{- s^{2}} - 1 ∣ = \int_{0}^{s^{2}} e^{- v} d v \leq s^{2}$ , the integral definition yields $h (r) = 2 α r / \sqrt{π} + O (r^{3})$ , and the derivative formula yields $h^{'} (r) = 2 α / \sqrt{π} + O (r^{2})$ . Thus $h (r) / r \to 2 α / \sqrt{π}$ and $(h^{'} (r) r - h (r)) / r^{2} = O (r)$ as $r ↓ 0$ . For $r > 0$ , the radial Laplacian formula $Δ f (∣ x ∣) = (r f (r))^{''} / r$ follows by differentiating $\partial_{x_{j}} f = f^{'} (r) x_{j} / r$ and summing $j = 1, 2, 3$ . Applying it to $f = ϕ_{ℓ} = h / r$ gives $- Δ ϕ_{ℓ} = 4 α^{3} e^{- α^{2} r^{2}} / \sqrt{π} = 4 π g_{α}$ away from the origin.

2.1step 1.1A1F1F3F4F6

Let $F_{ε} = φ \nabla ϕ_{ℓ} - ϕ_{ℓ} \nabla φ$ on the punctured ball $B_{R} ∖ {\overline{B}}_{ε}$ , where $R$ is outside the support of $φ$ . The product rule gives $div F_{ε} = φ Δ ϕ_{ℓ} - ϕ_{ℓ} Δ φ$ . By [F1] its integral is the boundary flux. The outer flux is zero; at the inner sphere both $ϕ_{ℓ}$ and $\nabla ϕ_{ℓ}$ are bounded, and its area is $\int_{0}^{2 π} \int_{0}^{π} ε^{2} \sin θ d θ d ϕ = 4 π ε^{2}$ , so the flux tends to zero. Taking $ε ↓ 0$ proves $\int ϕ_{ℓ} (- Δ φ) = \int φ (- Δ ϕ_{ℓ}) = 4 π \int φ g_{α}$ , using step 1.1. By [F3], [F4], and [F6], applied coordinatewise and with $y = α x$ , $\int_{R^{3}} g_{α} = 1$ .

2.2step 1.1F3algebra

Step 1.1 gives $\erf (α r) = 2 α r / \sqrt{π} + O (r^{3})$ , so $erfc (α r) / r = 1 / r - 2 α / \sqrt{π} + O (r^{2})$ . By [F3] and evenness, $erfc (s) = (2 / \sqrt{π}) \int_{s}^{\infty} e^{- t^{2}} d t \geq 0$ . For $s > 0$ , $\int_{s}^{\infty} e^{- t^{2}} d t \leq s^{- 1} \int_{s}^{\infty} t e^{- t^{2}} d t = e^{- s^{2}} / (2 s)$ ; multiplying by $2 / \sqrt{π}$ gives $erfc (s) \leq e^{- s^{2}} / (\sqrt{π} s)$ . This proves the bound for $ϕ_{s}$ .

3.1A1F1step 2.1algebra

On the punctured ball $Δ (1 / r) = 0$ . Put $G_{ε} = φ \nabla (1 / r) - (1 / r) \nabla φ$ . The product rule gives $div G_{ε} = - (1 / r) Δ φ$ , so [F1] makes the integral of $(1 / r) (- Δ φ)$ equal to its boundary flux. The outer flux is zero. The inner outward normal is $- x / r$ , hence $\partial_{n} (1 / r) = ε^{- 2}$ ; the flux is $\int_{∣ x ∣ = ε} (φ ε^{- 2} - (1 / ε) \partial_{n} φ) d S$ . Since $d S = ε^{2} \sin θ d θ d ϕ$ , its first term tends to $4 π φ (0)$ and the second is bounded by $4 π ε \sup ∣ \nabla φ ∣$ , hence tends to zero. Therefore $- Δ (1 / r) = 4 π δ_{0}$ distributionally. Subtracting step 2.1 proves $- Δ ϕ_{s} = 4 π δ_{0} - 4 π g_{α}$ .

4.1step 2.2algebra∎

Differentiating $ϕ_{s}$ for $r > 0$ gives $ϕ_{s}^{'} (r) = - 2 α e^{- α^{2} r^{2}} / (\sqrt{π} r) - erfc (α r) / r^{2}$ . Apply step 2.2 with $s = α r$ to its second term to obtain the displayed derivative bound.

Remarks

The distributional delta is in the unscreened Coulomb part. The smooth Gaussian term has no delta mass.
The self expansion is the source of the Ewald energy correction $- α \sum_{i} q_{i}^{2} / \sqrt{π}$ after the potential is multiplied by $q_{i} / 2$ .

Depends on

Used by

Dependency tree · two levels

63 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

Hark Lee and Wei Cai, Ewald Summation for Coulomb Interactions in a Periodic Supercell (2009 lecture notes) (standard reference, not scraped)
Cameron F. Abrams, Modern Molecular Simulations (CHE T580, 2021 lecture notes) (standard reference, not scraped)