TheoremStatement: 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.

Boys integral, power series, recurrence, and incomplete-gamma representation

Statement

For every $m \in N_{0}$ and real $T$ , the extension in Boys functions and lower incomplete-gamma notation satisfies $0 < F_{m} (T) \leq \frac{1}{2 m + 1}, F_{m} (0) = \frac{1}{2 m + 1},$ $F_{m} (T) = \sum_{k = 0}^{\infty} \frac{(- T)^{k}}{k! (2 m + 2 k + 1)}, \frac{d}{d T} F_{m} (T) = - F_{m + 1} (T) .$ The upper bound in the first display is asserted for $T \geq 0$ . For $T > 0$ the function also satisfies $2 T F_{m + 1} (T) = (2 m + 1) F_{m} (T) - e^{- T}, F_{m} (T) = \frac{γ (m + \frac{1}{2}, T)}{2 T^{m + 1 / 2}} .$ The complete Gamma factor at a half-integer is $Γ (m + \frac{1}{2}) = \frac{(2 m)!}{4^{m} m!} \sqrt{π} .$

Facts & Assumptions

Given: An integer $m \geq 0$ , real $T$ , and the integral definitions of $F_{m}$ and $γ$ from Boys functions and lower incomplete-gamma notation.

[F1]

Boys functions and lower incomplete-gamma notation: $F_{m} (T) = \int_{0}^{1} t^{2 m} e^{- T t^{2}} d t$ and $γ (s, T) = \int_{0}^{T} u^{s - 1} e^{- u} d u$ for $s, T > 0$ .

[F2]

Euler's Gamma function on the right half-plane: for real $s > 0$ , $Γ (s) = \int_{0}^{\infty} u^{s - 1} e^{- u} d u$ .

[F3]

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

[F4]

The Gamma functional equation: $Γ (s + 1) = s Γ (s)$ for real $s > 0$ .

[F5]

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.

[F6]

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$ : on a compact interval, $\int u v^{'} = u v ∣_{\partial} - \int u^{'} v$ when the stated integrability hypotheses hold.

[F7]

Dominated convergence: pointwise limits may pass through a Lebesgue integral when one integrable majorant bounds the sequence almost everywhere.

[F8]

Mean value theorem on a closed real interval: a scalar difference quotient equals a derivative value at an intermediate point of the parameter interval.

[F9]

The real exponential function and the number $e$ by a power series: $\exp (x) = \sum_{k = 0}^{\infty} x^{k} / k!$ for real $x$ , with convergence for every $x$ .

[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.

Proof

1.1givenF1F7F8F9algebraL9

The integrand in [F1] is positive for every real $T$ ; when $T \geq 0$ it is at most $t^{2 m}$ , whose integral is $1 / (2 m + 1)$ . Setting $T = 0$ gives equality. By [F9], on a compact parameter interval $[- M, M]$ the exponential-series partial sums converge pointwise on $[0, 1]$ and are bounded in absolute value by $e^{M}$ ; [F7] therefore permits integration term by term and gives the displayed series. For a fixed $T$ , choose $M > ∣ T ∣ + 1$ and $∣ h ∣ < 1$ . By [F8] and the chain rule, the difference quotient of $e^{- T t^{2}}$ in $T$ is $- t^{2} e^{- ξ t^{2}}$ for some $ξ$ between $T$ and $T + h$ , so after multiplication by $t^{2 m}$ it is bounded by $e^{M} t^{2 m + 2}$ . Dominated convergence [F7] passes the difference-quotient limit through the integral and gives $F_{m}^{'} (T) = - F_{m + 1} (T)$ .

1.2givenF1F6algebra

On $[0, 1]$ , integrate by parts [F6] with $u (t) = t^{2 m + 1}$ and $v^{'} (t) = - 2 T t e^{- T t^{2}}$ , so $v (t) = e^{- T t^{2}}$ . The boundary increment is $e^{- T}$ , while the two integrals are $- 2 T F_{m + 1} (T)$ and $- (2 m + 1) F_{m} (T)$ . Rearranging gives $2 T F_{m + 1} = (2 m + 1) F_{m} - e^{- T}$ .

1.3givenF1F5algebra

For $T > 0$ , use the increasing surjection $t = \sqrt{u / T}$ from $(0, T]$ to $(0, 1]$ . Its derivative is continuous on compact truncations away from zero, as are the integrands, so the proper substitution hypotheses of [F5] hold there. Then $d t = \frac{1}{2} T^{- 1 / 2} u^{- 1 / 2} d u$ and $t^{2 m} = T^{- m} u^{m}$ , giving $γ (m + \frac{1}{2}, T) / (2 T^{m + 1 / 2})$ on passage to the zero endpoint. The original integrand is bounded there, and the transformed one is bounded by a constant times $u^{m - 1 / 2}$ , whose exponent is greater than $- 1$ ; both improper integrals therefore converge.

2.1givenF2F3F4F5algebra∎

In [F2], substitute $u = x^{2}$ for $Γ (1 / 2)$ . This is an increasing differentiable surjection of $(0, \infty)$ onto itself, with continuous derivative and continuous integrands on compact truncations away from zero; hence [F5] applies separately at zero and infinity. The transformed integrand is $2 e^{- x^{2}}$ , integrable at both ends by [F3], so symmetry gives $Γ (1 / 2) = 2 \int_{0}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ . Repeated use of [F4] gives $Γ (m + \frac{1}{2}) = \prod_{j = 0}^{m - 1} (j + \frac{1}{2}) \sqrt{π}$ . Multiplying the odd factors yields $(2 m)! / (4^{m} m!)$ , proving the half-integer formula, including the empty product when $m = 0$ .

Depends on

Used by

Dependency tree · two levels

54 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)