LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

Cartesian Gaussian moments and exponent-parameter derivatives

Statement

Let $p > 0$ and $α \in N_{0}^{3}$ . If any component of $α$ is odd, then $\int_{R^{3}} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x = 0.$ If $α_{j} = 2 k_{j}$ for $j = 1, 2, 3$ , then $\int_{R^{3}} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x = π^{3 / 2} \prod_{j = 1}^{3} \frac{(2 k_{j})!}{4^{k_{j}} k_{j}! p^{k_{j} + 1 / 2}} .$ For every $q \in N_{0}$ , differentiation with respect to $p$ is valid and $\frac{d^{q}}{d p^{q}} \int_{R^{3}} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x = (- 1)^{q} \int_{R^{3}} ∥ x ∥_{2}^{2 q} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x .$

Facts & Assumptions

Given: $p > 0$ , a multi-index $α \in N_{0}^{3}$ , and the Lebesgue integral convention of Cartesian Gaussian primitives, contractions, and integral conventions.

[F1]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : $\int_{R} e^{- x^{2}} d x = \sqrt{π}$ .

[F2]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : finite-interval integration by parts holds when the displayed functions and derivatives are integrable.

[F3]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative measurable functions on a sigma-finite product may be integrated by sections in either order.

[F4]

Fubini's theorem for L^1 functions on a sigma-finite product: absolutely integrable functions on a sigma-finite product have equal iterated and product integrals.

[F5]

Dominated convergence: pointwise convergence under a single integrable majorant permits passage of the limit through the integral.

[F6]

Mean value theorem on a closed real interval: a difference quotient of a differentiable scalar function is bounded by the supremum of its derivative on the intervening segment.

[F7]

Change of variable in an improper integral: a monotone differentiable surjection between intervals preserves convergent improper integrals when its derivative and the target integrand are locally Riemann integrable and the proper change-of-variable hypotheses hold on every compact truncation. Each singular end is treated separately, with orientation adjusted for decreasing substitutions.

[L9]

The exponential function is smooth and $(\exp)^{'} = \exp$ and Sum, product, quotient, and chain rules from difference quotients: the exponential is smooth with derivative itself; finite sums, products and polynomial compositions obey the product, power and chain rules. Applying these rules one coordinate or parameter at a time justifies every displayed finite Gaussian derivative.

[F8]

The real exponential function and the number $e$ by a power series: $e^{x}$ is given by its convergent power series for real $x$ .

Proof

1.1givenF1F2F7F8algebraL9

For each integer $d \geq 0$ , $∣ x ∣^{d} e^{- p x^{2}}$ is absolutely integrable. If $d > 0$ , differentiating $r^{d} e^{- p r^{2} / 2}$ shows it increases up to $r = \sqrt{d / p}$ and decreases afterwards, so it is bounded by $(d / p)^{d / 2}$ ; for $d = 0$ it is bounded by $1$ . Thus $∣ x ∣^{d} e^{- p x^{2}} \leq C_{d} e^{- p x^{2} / 2}$ for a finite $C_{d}$ , whose right-hand side is integrable by scaling and [F1], [F7]. Write $J_{k} (p) = \int_{R} x^{2 k} e^{- p x^{2}} d x$ for $k \geq 0$ . Then $J_{0} (p) = \sqrt{π} p^{- 1 / 2}$ by scaling $y = \sqrt{p} x$ and [F1], [F7], and odd moments vanish by $x \mapsto - x$ , now with absolute convergence established. All these scaling and reflection maps are linear surjections with continuous derivatives; the integrands are continuous on every compact truncation, so [F7] applies separately at both infinite ends. Fix $k \geq 1$ for the moment recurrence below. For its boundary term choose an integer $N > (2 k - 1) / 2$ . By [F8] and $e^{- p R^{2} / 2} \leq 1$ , $R^{2 k - 1} e^{- p R^{2}} \leq N! (2 / p)^{N} R^{2 k - 1 - 2 N} ⟶ 0.$ Integration by parts [F2] on $[- R, R]$ with $d v = x e^{- p x^{2}} d x = - d (e^{- p x^{2}}) / (2 p)$ therefore gives $J_{k} (p) = (2 k - 1) J_{k - 1} (p) / (2 p)$ after $R \to \infty$ . Iterating yields $J_{k} (p) = \sqrt{π} (2 k)! / (4^{k} k! p^{k + 1 / 2})$ .

2.1givenF3F4step 1.1algebra

The absolute value of each three-dimensional integrand is a product of three one-dimensional polynomial-Gaussian factors. Their integrals are finite by step 1.1, so [F3] and then [F4] factor the integral into the product of the three one-dimensional moments. If a component is odd, its factor is zero; otherwise multiplying the three formulas from step 1.1 gives the displayed expression.

3.1givenF5F6step 1.1step 2.1inductionL9∎

Fix $p_{0} > 0$ and restrict $p$ to $[p_{0} / 2, 3 p_{0} / 2]$ . The absolute value of each $q$ -th parameter derivative integrand is bounded by $∥ x ∥^{∣ α ∣ + 2 q} e^{- (p_{0} / 2) ∥ x ∥^{2}}$ . This is integrable by step 2.1: bound $∥ x ∥^{d} \leq (∣ x_{1} ∣ + ∣ x_{2} ∣ + ∣ x_{3} ∣)^{d}$ , expand the finite power, and use the absolute one-dimensional moments established in step 1.1. Difference quotients for one derivative are bounded by the corresponding next polynomial-Gaussian majorant by [F6]; [F5] therefore passes each limit through the integral. Repeating this argument $q$ times gives the stated factor $(- 1)^{q} ∥ x ∥^{2 q}$ .

Depends on

Used by

Dependency tree · two levels

59 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

Trygve Helgaker, Molecular Integral Evaluation, 10th Sostrup Summer School lecture notes (2008) (standard reference, not scraped)
L. E. McMurchie and E. R. Davidson, One and Two Electron Integrals over Cartesian Gaussian Functions, UCRL-13791 (1976) (standard reference, not scraped)