LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

Two-sided Mills bounds for the standard normal tail

Statement

Let $φ (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ and $\overline{Φ} (x) = \int_{x}^{\infty} φ (y) d y$ for $x \in R$ . Then for every $x > 0$ $\frac{x φ (x)}{1 + x^{2}} \leq \overline{Φ} (x) \leq \frac{φ (x)}{x},$ and consequently, for every $x > 1$ , $(\frac{1}{x} - \frac{1}{x^{3}}) φ (x) \leq \overline{Φ} (x) \leq \frac{φ (x)}{x} .$ Both bounds are sharp as $x \to \infty$ in the sense that the ratio of each side to $\overline{Φ} (x)$ tends to $1$ .

Facts & Assumptions

Given: AC, AC $_{ω}$ , DC, and a real $x > 0$ .

[F1]

$φ$ is the strictly positive, Borel measurable standard normal density, with $\int_{R} φ = 1$ , and $N (0, 1)$ is the probability measure $φ d y$ . Standard normal and normal laws The standard normal density has total mass one

[F2]

On a compact interval every $C^{1}$ function is Lipschitz, hence absolutely continuous and of bounded variation; in particular $φ$ and $y \mapsto 1 / y$ are absolutely continuous on $[x, R]$ for $0 < x < R$ . $C^{1}$ implies Lipschitz, Lipschitz implies absolutely continuous, and absolutely continuous implies continuous and bounded variation

[F3]

Integration by parts for absolutely continuous functions: $\int_{a}^{b} F G^{'} + \int_{a}^{b} F^{'} G = F (b) G (b) - F (a) G (a)$ , under AC $_{ω}$ and DC. Integration by parts for absolutely continuous functions The Axiom of Countable Choice ( ${A C}_{ω}$ ) The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain

[F4]

Substitution computes $\int_{x}^{R} y e^{- y^{2} / 2} d y = e^{- x^{2} / 2} - e^{- R^{2} / 2}$ , and monotone convergence justifies passing to the limit $R \to \infty$ in the integrals of the nonnegative functions $φ$ and $φ (y) / y^{2}$ over $[x, R]$ . Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ Monotone convergence for the integral

[F5]

AC is the ambient assumption; AC $_{ω}$ and DC are the hypotheses of the integration-by-parts interface used in [F3]. The Axiom of Choice The Axiom of Countable Choice ( ${A C}_{ω}$ ) The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain

Proof

technique · direct

1.1givenF1F4

For $y \geq x > 0$ one has $φ (y) \leq (y / x) φ (y)$ ; integrating over $[x, R]$ and letting $R \to \infty$ with [F4] gives $\overline{Φ} (x) \leq \frac{1}{x} \int_{x}^{\infty} y φ (y) d y$ , and [F4] computes $\int_{x}^{R} y φ (y) d y = (2 π)^{- 1 / 2} (e^{- x^{2} / 2} - e^{- R^{2} / 2}) \to φ (x)$ , so $\overline{Φ} (x) \leq φ (x) / x$ .

1.2F2F3

For $0 < x < R$ , [F2] and [F3] applied to $F (y) = 1 / y$ and $G = φ$ on $[x, R]$ , together with $φ^{'} (y) = - y φ (y)$ , give $\int_{x}^{R} φ (y) d y = φ (x) / x - φ (R) / R - \int_{x}^{R} φ (y) y^{- 2} d y$ .

2.1step 1.2F4

Letting $R \to \infty$ in [step 1.2] with [F4] gives $\overline{Φ} (x) = φ (x) / x - \int_{x}^{\infty} φ (y) y^{- 2} d y$ , and since $y^{- 2} \leq x^{- 2}$ on $[x, \infty)$ one gets $\overline{Φ} (x) \geq φ (x) / x - \overline{Φ} (x) / x^{2}$ , that is, $\overline{Φ} (x) (1 + x^{- 2}) \geq φ (x) / x$ and hence $\overline{Φ} (x) \geq x φ (x) / (1 + x^{2})$ .

3.1step 1.1step 2.1

The algebraic comparison $x / (1 + x^{2}) \geq (1 / x - 1 / x^{3})$ for $x > 0$ is equivalent to $x^{4} \geq (x^{2} - 1) (1 + x^{2}) = x^{4} - 1$ , which holds; combining it with [step 2.1] gives the displayed form for $x > 1$ , and the ratio claim follows because $(1 / x - 1 / x^{3}) / (1 / x) = 1 - x^{- 2} \to 1$ and $(x / (1 + x^{2})) / (1 / x) = 1 / (1 + x^{- 2}) \to 1$ while the upper bound already is $φ (x) / x$ .

4.1step 1.2step 2.1F3F5given∎

The endpoint and degenerate cases are covered: $x > 0$ is required so that $1 / x$ and the integration interval $[x, R]$ are meaningful and $F = 1 / y$ is $C^{1}$ on it; $x = 0$ is excluded by the statement because the upper bound would divide by zero, while $\overline{Φ} (0) = \frac{1}{2}$ is finite; the limit $R \to \infty$ is handled by monotone convergence over the increasing family $[x, R]$ ; the constants AC $_{ω}$ and DC are those declared for [F3] and are used nowhere else; and AC enters only through [F5].

Source notes

Durrett, Lemma 1.2.6 and the estimates (8.5.2) in the proof of Theorem 8.5.1, states the two-sided bound $(x^{- 1} - x^{- 3}) e^{- x^{2} / 2} \leq \int_{x}^{\infty} e^{- y^{2} / 2} d y \leq x^{- 1} e^{- x^{2} / 2}$ for $x > 0$ (up to the normalization constant), together with the asymptotic ratio $1$ used in the law of the iterated logarithm. The proof above derives the stronger lower bound $x φ (x) / (1 + x^{2})$ from the identity obtained by integrating by parts, which is the form consumed by the LIL item.

Depends on

Used by

Dependency tree · two levels

70 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

Rick Durrett, Probability: Theory and Examples, fifth edition, Lemma 1.2.6 and the Gaussian tail estimates (8.5.2) in the proof of Theorem 8.5.1 (standard reference, not scraped)