LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)

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.

A one-coordinate projection risk bound

Statement

Assume Countable Choice. Let $r \geq 0$ and $τ > 0$ . In the one-dimensional Gaussian location experiment with parameter $θ \in [- r, r]$ , action space $R$ , observation density $p_{θ, τ} (y) = \frac{1}{τ \sqrt{2 π}} \exp ⁣ (- \frac{(y - θ)^{2}}{2 τ^{2}})$ with respect to Lebesgue measure, and squared-error loss, let $M (r, τ)$ be the minimax expected risk over all measurable deterministic or randomized estimators. Put $b = \min {r, τ}$ and take the prior assigning mass $1 / 2$ to each of $- b$ and $b$ . The better of the estimators $y \mapsto 0$ and $y \mapsto y$ has worst-case risk $T (r, τ) = \min {r^{2}, τ^{2}}$ , and this prior has Bayes risk at least $T (r, τ) / \sqrt{2 e}$ , so $M (r, τ) \geq T (r, τ) / \sqrt{2 e}$ .

Statement references

Gaussian sequence inverse model and its standard-normal coordinates

Iain M. Johnstone, Gaussian estimation: Sequence and wavelet models, §2.3 and §4.6

Litao Ding and Peter Mathé, Minimax rates for statistical inverse problems under general source conditions, §2

Facts & Assumptions

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice is assumed for the Lebesgue change-of-variables and improper-integral results used below.

[F1]

Gaussian sequence inverse model and Isonormal Gaussian white-noise inverse experiment: A scalar coordinate has the stated Gaussian location density and can be written $Y = θ + τ ξ$ , where $E ξ = 0$ and $E ξ^{2} = 1$ ; the latter follows from the isonormal covariance at a unit basis vector.

[F2]

Statistical experiments and Measurable spaces and measurable sets: An experiment consists of a measurable sample space, a parameter set, and parameter-indexed sampling probabilities.

[F3]

The Borel sigma-algebra of a topological space, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ , A continuous map has Borel preimages of Borel sets, Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable, and Closure properties of measurable functions used by the integral: The displayed continuous densities and integrands are Borel and, under Countable Choice, Lebesgue measurable; products with indicators of Borel intervals remain measurable.

[F4]

Loss functions and risk, Randomized procedures as probability kernels, and Bayes risk and minimax risk: Squared-error risk is the expected nonnegative loss; a randomized rule is a parameter-independent probability kernel from data to actions; minimax risk is the infimum of worst-case risks, and every supported prior has Bayes risk no larger than the minimax value.

[F5]

The six hyperbolic functions and their natural domains: $\cosh x = (\exp x + \exp (- x)) / 2$ , $\tanh x = \sinh x / \cosh x$ , and $sech x = 1 / \cosh x$ ; the definitions give $\tanh 0 = 0$ .

[F6]

Addition formulas, identities, parity, and derivatives of the hyperbolic functions: $\cosh$ is even, $\cosh x \geq 1$ , it is increasing on $[0, \infty)$ , $\tanh$ is strictly increasing, $\cosh^{2} x - \sinh^{2} x = 1$ , $(\tanh x)^{'} = {sech}^{2} x$ , $(\cosh x)^{'} = \sinh x$ , and $(sech x)^{'} = - sech x \tanh x$ .

[F7]

The real exponential function and the number $e$ by a power series: $e = \exp (1)$ .

[F8]

The real exponential function and the number $e$ by a power series, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $\exp (0) = 1$ , $\exp (x + y) = \exp x \exp y$ , $\exp (- x) = 1 / \exp x$ , and $\exp x > 0$ .

[F9]

The exponential function is strictly increasing: $\exp$ is continuous and strictly increasing on $R$ .

[F10]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ and Improper integrals with several singular ends: The mixed improper Riemann integral of $x \mapsto e^{- x^{2}}$ is $\sqrt{π}$ , with the negative and positive tails treated separately.

[F11]

A nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral: Under Countable Choice, a nonnegative locally Riemann-integrable function with a finite improper integral on $[0, \infty)$ has the same Lebesgue integral there.

[F12]

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: Under Countable Choice, a $C^{1}$ diffeomorphism between open subsets of $R$ transforms a nonnegative Lebesgue integral with its absolute derivative factor; in particular this applies to affine bijections of $R$ .

[F13]

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included and A nonnegative integral over a null set vanishes: Under Countable Choice, the singleton ${0}$ is Lebesgue null and the integral of a nonnegative measurable function over it is zero.

[F14]

Additivity of the nonnegative Lebesgue integral: The nonnegative Lebesgue integral is additive.

[F15]

Change of variable in an improper integral: The substitution $x \mapsto - x$ identifies the two one-sided improper integrals of the even function $e^{- x^{2}}$ .

[F16]

The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , and The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : The exponential, product and composition rules differentiate the displayed smooth functions, and a differentiable function's increment on an interval equals its derivative at an intermediate point times the interval length.

[F17]

Monotonicity and nonnegative homogeneity of the nonnegative integral: The nonnegative Lebesgue integral is monotone and respects multiplication by positive constants.

Given: Countable Choice, $r \geq 0$ , $τ > 0$ , the Gaussian location experiment, squared-error loss, and the endpoint prior specified in the Statement.

Proof

1.1givenF3F8F9F10F11F12F13F14F15algebra

Put $g (x) = e^{- x^{2}}$ . By [F10] its mixed improper Riemann integral is $\sqrt{π}$ , and [F15] identifies its two one-sided improper integrals, so each equals $\sqrt{π} / 2$ . The half-line bridge [F11] gives $\int_{[0, \infty)} g d λ_{1} = \sqrt{π} / 2$ . The map $T (x) = - x$ is a $C^{1}$ diffeomorphism from $(0, \infty)$ to $(- \infty, 0)$ , so [F12] applied to $g$ gives $\int_{(- \infty, 0)} g d λ_{1} = \int_{(0, \infty)} g d λ_{1}$ . By [F13] the point $0$ contributes zero, and [F14] on the disjoint decompositions $(0, \infty) ⊔ {0} = [0, \infty)$ and $(- \infty, 0) ⊔ [0, \infty) = R$ therefore gives $\int_{R} e^{- x^{2}} d λ_{1} = \sqrt{π}$ . Applying [F12] with $T (x) = \sqrt{2} x$ and $f (y) = e^{- y^{2} / 2}$ now gives $\int_{R} e^{- x^{2} / 2} d λ_{1} = \sqrt{2} \sqrt{π}$ , hence $\int_{R} ϕ (x) d λ_{1} = 1$ .

1.2givenF1F4F5F6F8F9algebra

Write $b = \min {r, τ}$ and $u = b / τ \in [0, 1]$ . This location family is the scalar Gaussian coordinate experiment described in [F1]. Under the two-point prior, the likelihood ratio at observation $y$ is $p_{b, τ} (y) / p_{- b, τ} (y) = \exp (2 b y / τ^{2})$ by [F8]. Hence the posterior mean is $b \tanh (b y / τ^{2})$ and the posterior variance is $b^{2} {sech}^{2} (b y / τ^{2})$ by [F5]–[F6]; for any action $a$ , its conditional squared loss is the square of its distance from this posterior mean plus that posterior variance. Averaging this identity over any action kernel from [F4] leaves the posterior variance as a lower bound, including the degenerate case $b = 0$ .

2.1givenF2F3F8F9F12step 1.1algebra

The density in the Statement is positive by [F8], continuous by [F9], and measurable by [F3]. Applying [F12] to $T (x) = θ + \sqrt{2} τ x$ gives its Lebesgue integral as $(τ \sqrt{2 π})^{- 1} \sqrt{2} τ \int_{R} e^{- x^{2}} d λ_{1} = 1$ by step 1.1, so by [F2]–[F3] it defines the scalar sampling probability on the stated Borel sample space.

2.2givenF3F5F6F9F17step 1.1algebra

Define $I (u) : = \int_{R} ϕ (x) sech (u x) d λ_{1} (x)$ . Since $\cosh t \geq 1$ , the integrand lies between $0$ and $ϕ (x)$ , whose integral is $1$ by step 1.1; monotonicity [F17] makes $I (u)$ finite. Since $\cosh$ is even and increasing on $[0, \infty)$ by [F6], $sech (u x) \geq sech (x)$ for every real $x$ and $0 \leq u \leq 1$ . Therefore $I (u) \geq I (1)$ by [F17], while $e^{- u^{2} / 2} \geq e^{- 1 / 2}$ by [F9].

2.3F5F6F8F9F16F17step 1.1algebra

For $x \geq 0$ , [F6] gives $0 \leq \tanh x$ and $(\tanh x)^{'} \leq 1$ because $\cosh x \geq 1$ ; with $\tanh 0 = 0$ , [F16] yields $\tanh x \leq x$ . Set $g (x) = e^{- x^{2} / 2} \cosh x$ . Differentiation using [F6] and [F16] gives $g^{'} (x) = g (x) (\tanh x - x) \leq 0$ , so [F16] implies $g (x) \leq g (0) = 1$ . Evenness extends $\cosh x \leq e^{x^{2} / 2}$ to all real $x$ . Consequently $ϕ (x) sech x \geq (2 π)^{- 1 / 2} e^{- x^{2}}$ , and step 1.1 plus [F17] gives $I (1) \geq 1 / \sqrt{2}$ .

3.1step 1.2step 2.2F3F5F8F12algebra

The prior predictive density, after $x = y / τ$ , is $τ^{- 1} ϕ (x) e^{- u^{2} / 2} \cosh (u x)$ , where $ϕ (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ , by [F8]. Multiplying by the posterior variance from step 1.2 and applying the full-line Lebesgue affine substitution [F12] to this nonnegative measurable integrand gives Bayes risk $B (r, τ) = b^{2} e^{- u^{2} / 2} I (u)$ , with $I$ defined in step 2.2.

4.1givenF4F7F8F9step 3.1step 2.2step 2.3algebra

Steps 3.1, 2.2 and 2.3 give $B (r, τ) \geq b^{2} e^{- 1 / 2} / \sqrt{2} = b^{2} / \sqrt{2 e} = T (r, τ) / \sqrt{2 e}$ , where $e = \exp (1)$ by [F7] and the exponential laws [F8]–[F9]. Since the prior is supported in $[- r, r]$ , the supremum risk of every rule is at least its prior-averaged risk; taking the infimum over rules and using [F4] yields $M (r, τ) \geq B (r, τ)$ .

5.1givenF1F3step 4.1algebra∎

The constant estimator $0$ has maximum risk $r^{2}$ . For the identity estimator, [F1] gives $Y - θ = τ ξ$ with $E ξ^{2} = 1$ , so its risk is $τ^{2}$ at every parameter; hence their better maximum risk is $T (r, τ) = b^{2}$ . This proves the projection-risk claim together with step 4.1.

Depends on

Used by

Cutoff risk and minimax RMS error over statistical ellipsoids Theorem

Dependency tree · two levels

135 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

Iain M. Johnstone, Gaussian estimation: Sequence and wavelet models, 2011 draft, §2.3, equations (2.26)–(2.30), and §4.6, Theorem 4.17 proof, printed pp. 29–30 and 111–113 (standard reference, not scraped)
Litao Ding and Peter Mathé, Minimax rates for statistical inverse problems under general source conditions, §2, equations (12)–(13), PDF pp. 3–4 (standard reference, not scraped)