LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Finite Sudakov–Fernique comparison for Gaussian maxima

Statement

Assume AC. Let $m \geq 2$ , and let $X, Y \in R^{m}$ be independent, centered Gaussian vectors with finite covariance matrices. If

$E [(X_{i} - X_{j})^{2}] \geq E [(Y_{i} - Y_{j})^{2}] (i, j \in {1, \dots, m}),$

then $E [\max_{i} X_{i}] \geq E [\max_{i} Y_{i}]$ .

Statement references

Wainwright 2006, Appendix B, Lemma 10

Wainwright 2009, §VI

Facts & Assumptions

Given: AC and independent centered Gaussian vectors $X, Y \in R^{m}$ satisfying the displayed increment-variance inequalities.

[A1]

Under AC, Multivariate normal law, including singular covariance constructs $C^{1 / 2} Z$ with law $N_{m} (0, C)$ for $C ⪰ 0$ and independent standard-normal coordinates $Z$ . The uniqueness assertion of Characteristic function of a multivariate normal law identifies this law with that of any given centered Gaussian vector of covariance $C$ , including singular $C$ (The Axiom of Choice).

[F1]

A standard normal coordinate has density $ϕ (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ , with $ϕ^{'} (x) = - x ϕ (x)$ (Standard normal and normal laws).

[F2]

A product of sigma-finite measure spaces has a product measure with the rectangle formula (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique).

[F3]

Dominated convergence permits passage to limits when the integrands have an integrable common majorant (Dominated convergence).

[F4]

An integrable function on a sigma-finite product can be integrated in either order (Fubini's theorem for L^1 functions on a sigma-finite product).

Proof

1.1givenconstructalgebra

For $a > 0$ define $Φ_{a} (x) = a^{- 1} \log \sum_{i = 1}^{m} e^{a x_{i}}$ and $p_{i} (x) = e^{a x_{i}} / \sum_{j} e^{a x_{j}}$ . Direct differentiation gives $\partial_{i} Φ_{a} = p_{i}$ and $\partial_{i j} Φ_{a} = a (p_{i} 1_{i = j} - p_{i} p_{j})$ , while $\max_{i} x_{i} \leq Φ_{a} (x) \leq \max_{i} x_{i} + \log (m) / a$ .

2.1A1F1F2F3F4step 1.1algebra

Let $C_{X}, C_{Y}$ be the covariance matrices. By [A1], on a product probability space [F2] replace $X, Y$ by copies $X = C_{X}^{1 / 2} ξ$ , $Y = C_{Y}^{1 / 2} η$ with the same respective laws, where all coordinates of $ξ, η$ are independent standard normals. The desired expectations depend only on these laws. Put $Z_{t} = \sqrt{t} X + \sqrt{1 - t} Y$ and $F_{a} (t) = E Φ_{a} (Z_{t})$ . For $0 < t < 1$ , differentiate under the expectation; on every closed subinterval of $(0, 1)$ the derivative is bounded by a constant times $∥ ξ ∥_{2} + ∥ η ∥_{2}$ , which is integrable since $\int_{R} ∣ x ∣ ϕ (x) d x = \sqrt{2 / π}$ . Thus [F3] applies. Using [F4] to integrate one standard-normal coordinate at a time, one-dimensional integration by parts against [F1], with the bounded first and second derivatives from step 1.1, gives $F_{a}^{'} (t) = \frac{1}{2} \sum_{i, j} (C_{X} - C_{Y})_{i j} E [\partial_{i j} Φ_{a} (Z_{t})] .$ The boundary terms vanish because $ϕ (x)$ decays to zero and $\partial_{i} Φ_{a}$ is bounded.

3.1F3step 1.1step 2.1givenalgebra

Substituting the Hessian from step 1.1 into step 2.1 and using $\sum_{i} p_{i} = 1$ rewrites the derivative as $F_{a}^{'} (t) = \frac{a}{4} E [\sum_{i, j} p_{i} (Z_{t}) p_{j} (Z_{t}) (E [(X_{i} - X_{j})^{2}] - E [(Y_{i} - Y_{j})^{2}])] \geq 0.$ Hence $F_{a}$ is nondecreasing on $(0, 1)$ . For all $t \in [0, 1]$ , $∣ Φ_{a} (Z_{t}) ∣ \leq ∥ X ∥_{2} + ∥ Y ∥_{2} + \log (m) / a$ , an integrable bound, so [F3] gives continuity at the endpoints and therefore $F_{a} (1) \geq F_{a} (0)$ .

4.1step 1.1step 3.1algebra∎

The uniform approximation in step 1.1 gives $∣ E Φ_{a} (X) - E \max_{i} X_{i} ∣ \leq \log (m) / a$ and the analogous bound for $Y$ . Letting $a \to \infty$ in step 3.1 proves the asserted comparison.

Depends on

Used by

The unrestricted Wainwright signed-support threshold claim fails without active-dimension control False statement

Dependency tree · two levels

45 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

Wainwright, Sharp Thresholds for High-Dimensional and Noisy Recovery of Sparsity, 2006, Appendix B, Lemma 10 (standard reference, not scraped)
Wainwright, Sharp Thresholds for High-Dimensional and Noisy Sparsity Recovery Using L1-Constrained Quadratic Programming (Lasso), 2009, §VI (standard reference, not scraped)