ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated

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.

An exact Gaussian Laplace integral on the noncompact line

Example

For $c, μ \in R$ and integer $n \geq 1$ , define the noncompact integral $J_{n} : = \int_{R} \exp ⁣ (n [c - \frac{1}{2} (θ - μ)^{2}]) d θ .$ Then $J_{n} = e^{n c} \sqrt{2 π / n}$ exactly. The mode is $\hat{θ} = μ$ and $- h^{''} (\hat{θ}) = 1$ , so the usual one-dimensional quadratic expression is also exactly $e^{n c} \sqrt{2 π / n}$ . This calculation is a special noncompact Gaussian case; it does not extend the compact-domain theorem to arbitrary noncompact integrals.

Facts & Assumptions

Given: Reals $c, μ$ , an integer $n \geq 1$ , and $h (θ) = c - (θ - μ)^{2} / 2$ on $R$ .

[F1]

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

[F2]

Change of variable in an improper integral: for a monotone differentiable surjection with locally Riemann-integrable derivative, a locally Riemann-integrable integrand, and proper substitution valid on every compact truncation, the corresponding improper integrals converge simultaneously and are equal when convergent. Each singular end is treated separately.

[F3]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuous real function on a closed bounded interval is bounded and Riemann integrable.

Verification

1.1givenalgebra

The derivative is $h^{'} (θ) = - (θ - μ)$ , so the unique maximizer is $\hat{θ} = μ$ ; the second derivative is $h^{''} (μ) = - 1$ and $h (μ) = c$ .

1.2F1F2F3givenalgebra

Use $θ = ϕ (u) : = μ + \sqrt{2 / n} u$ . Since $n \geq 1$ , this is an increasing affine surjection of $R$ , with constant positive derivative $\sqrt{2 / n}$ . The original integrand and $ϕ^{'}$ are continuous, hence locally Riemann integrable by [F3], and on each compact truncation the map is differentiable through both endpoints, with integrable derivative and bounded continuous integrand, so the proper substitution hypotheses hold. By [F1], the transformed Gaussian converges at both infinite ends; applying [F2] separately at these ends proves convergence of $J_{n}$ and gives $J_{n} = e^{n c} \sqrt{2 / n} \int_{R} e^{- u^{2}} d u = e^{n c} \sqrt{2 π / n}$ .

2.1step 1.1step 1.2algebra∎

Substituting $h (μ) = c$ and $- h^{''} (μ) = 1$ into the one-dimensional quadratic expression gives $e^{n c} \sqrt{2 π / n}$ , which equals step 1.2 for every $n \geq 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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

Laplace method for integrals, PHYS 2400, University of Connecticut (standard reference, not scraped)