CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Matching minimax rate in a Gaussian orthogonal sequence model

Statement

Assume the Axiom of Choice. Let $n = d \geq 2$ , let $1 \leq s \leq n / 2$ , and take the fixed design $X = \sqrt{n} I_{n}$ . For $Θ_{s} : = {θ \in R^{n} : ∣ {j \in {1, \dots, n} : θ_{j} \neq 0} ∣ \leq s},$ observe $Y = X θ + ε$ with one common noise law $ε \sim N_{n} (0, σ^{2} I_{n})$ , where $σ > 0$ . For Borel fitted-vector estimators $T : R^{n} \to R^{n}$ , define $R_{n, s}^{*} : = \inf_{T B o r e l} \sup_{θ \in Θ_{s}} E_{θ} [\frac{1}{n} ∥ T (Y) - X θ ∥_{2}^{2}] .$ Then for $C = 32 (4 + 2 \log 6)$ , $\frac{σ^{2} s \log (e n / s)}{200000 n} \leq R_{n, s}^{*} \leq \sup_{θ \in Θ_{s}} E_{θ} [\frac{1}{n} ∥ {\hat{μ}}_{s} (Y) - X θ ∥_{2}^{2}] \leq C \frac{σ^{2} s \log (e n / s)}{n},$ where ${\hat{μ}}_{s}$ is the constrained support-search fitted vector. Thus this Gaussian orthogonal-sequence model has a matching minimax rate up to universal constants. The sparse upper-bound theorem itself is choice-free; this corollary assumes AC for its Gaussian law and Fano lower-bound suppliers.

Facts & Assumptions

Given: AC; integers $n = d \geq 2$ , $1 \leq s \leq n / 2$ ; $X = \sqrt{n} I_{n}$ ; and a common noise vector $ε \sim N_{n} (0, σ^{2} I_{n})$ with $σ > 0$ .

[A1]

AC is assumed by the multivariate-normal and Fano lower-bound suppliers (The Axiom of Choice).

[F1]

For every fixed design and every truth with at most $s$ nonzero coordinates, the constrained least-squares fitted vector has expected normalized squared error at most $C σ^{2} s \log (e n / s) / n$ (Sparse constrained least-squares risk bound).

[F2]

The finite tie-broken support-search output is Borel measurable (Finite tie-broken projection searches are Borel measurable).

[F3]

Isotropic Gaussian noise is centered sub-Gaussian with proxy $σ^{2}$ (Isotropic Gaussian noise has the matching sub-Gaussian proxy).

[F4]

By Multivariate normal law, including singular covariance, $N_{n} (0, σ^{2} I_{n})$ has the independent-coordinate realization $σ (G_{1}, \dots, G_{n})$ for independent standard-normal $G_{j}$ . Its characteristic-function formula and uniqueness in Characteristic function of a multivariate normal law identify that realization with the stated multivariate-normal law. Since $σ > 0$ , its coordinates are independent $N (0, σ^{2})$ variables.

[F5]

In the Gaussian sequence model $Z_{j} \sim N (θ_{j}, σ^{2} / n)$ with at most $s$ nonzero coordinates, every Borel vector estimator has maximum squared-error risk at least $σ^{2} s \log (e n / s) / (200000 n)$ (Gaussian sparse-sequence minimax lower bound).

[F6]

The general risk definition integrates a nonnegative loss against the sampling law and, for randomized rules, the action kernel (Loss functions and risk).

[F7]

Measurable coordinatewise transformations preserve independence, and an affine image $a + b G$ of a standard normal $G$ has law $N (a, b^{2})$ (Measurable coordinatewise functions preserve independence, Standard normal and normal laws).

[F8]

Continuous affine maps on Euclidean spaces are Borel, and compositions of measurable maps remain measurable (Continuous functions on Euclidean spaces are Borel measurable, Composition with a Borel measurable outer map preserves measurability).

Proof

1.1A1F1F2F3F6algebra

By [F3], the noise satisfies the centered vector proxy condition required by [F1]. The support-search fitted vector is Borel by [F2], so it is an admissible estimator for [F6]. Applying [F1] at each $θ \in Θ_{s}$ and taking the supremum and then the infimum gives the upper bound.

1.2A1F4F5F7F8algebra

Fix any Borel fitted-vector estimator $T$ . Put $Z = Y / \sqrt{n}$ and $S (z) = T (\sqrt{n} z) / \sqrt{n}$ , which is Borel by [F8]. Under the independent realization in [F4], the coordinates of $Z$ are coordinatewise measurable affine transforms of independent standard normals. By [F7], they remain independent and have laws $N (θ_{j}, σ^{2} / n)$ , exactly the sequence experiment in [F5]. Applying [F5] to the Borel estimator $S$ gives $\sup_{θ \in Θ_{s}} E_{θ} ∥ S (Z) - θ ∥_{2}^{2} \geq \frac{σ^{2} s \log (e n / s)}{200000 n} .$

2.1F6step 1.2algebra

Since $X = \sqrt{n} I_{n}$ , pointwise $\frac{1}{n} ∥ T (Y) - X θ ∥_{2}^{2} = {∥ \frac{T (Y)}{\sqrt{n}} - θ ∥}_{2}^{2} = ∥ S (Z) - θ ∥_{2}^{2} .$ By [F6] these pointwise losses define the respective risks. Thus every Borel $T$ has supremum fitted-value risk at least the lower bound in step 1.2. Taking the infimum over $T$ proves the minimax lower bound.

3.1step 1.1step 2.1algebra∎

The upper bound in step 1.1 and the lower bound in step 2.1 give the displayed comparison, with universal constants $1 / 200000$ and $C$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

82 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

Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 2, Corollaries 2.8–2.9 (standard reference, not scraped)