LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Standard-normal Mills bounds and logarithmic tail asymptotics

Statement

Let $ϕ (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ be the standard-normal density and $\overset{ˉ}{Φ} (x) = \int_{x}^{\infty} ϕ (t) d t$ . For every $x > 0$ , $\frac{x}{x^{2} + 1} ϕ (x) \leq \overset{ˉ}{Φ} (x) \leq \frac{ϕ (x)}{x} .$ Consequently $\overset{ˉ}{Φ} (x) \sim ϕ (x) / x$ and $\log \overset{ˉ}{Φ} (x) \sim - x^{2} / 2$ as $x \to \infty$ .

Facts & Assumptions

Given: The standard-normal density $ϕ$ from Standard normal and normal laws, $x > 0$ , and the tail integral in the Statement.

[F1]

Standard normal and normal laws: $N (0, 1)$ has density $ϕ (t) = e^{- t^{2} / 2} / \sqrt{2 π}$ with total mass one.

[A1]

The Axiom of Choice: AC is assumed only because the cited standard-normal definition uses it through its normalization suppliers.

Proof

1.1F1A1givenalgebra

Since $ϕ^{'} (t) = - t ϕ (t)$ , for $t \geq x > 0$ we have $ϕ (t) \leq t ϕ (t) / x$ . Integrating and using $\int_{x}^{\infty} t ϕ (t) d t = ϕ (x)$ , obtained by integrating $- ϕ^{'}$ , gives $\overset{ˉ}{Φ} (x) \leq ϕ (x) / x$ .

2.1F1step 1.1givenalgebra

Integration by parts on $[x, R]$ , followed by $R \to \infty$ , gives $\overset{ˉ}{Φ} (x) = \frac{ϕ (x)}{x} - \int_{x}^{\infty} \frac{ϕ (t)}{t^{2}} d t .$ The remainder is at most $\overset{ˉ}{Φ} (x) / x^{2}$ , hence $\overset{ˉ}{Φ} (x) (1 + x^{- 2}) \geq ϕ (x) / x$ , which is the stated lower bound.

3.1step 1.1step 2.1algebra∎

Dividing the two bounds by $ϕ (x) / x > 0$ traps the ratio $\overset{ˉ}{Φ} (x) / (ϕ (x) / x)$ between $x^{2} / (x^{2} + 1)$ and $1$ , so it tends to $1$ . Taking logarithms gives $\log \overset{ˉ}{Φ} (x) = - x^{2} / 2 - \log x - \frac{1}{2} \log (2 π) + o (1)$ ; division by $- x^{2} / 2$ yields the asserted logarithmic limit.

Depends on

Used by

Gaussian tail tilting is logarithmically efficient but not bounded-relative-error Theorem

Dependency tree · two levels

10 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

NIST Digital Library of Mathematical Functions, `7.12(i), Equation (7.12.1) (standard reference, not scraped)