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.
Single-block sparse Gaussian Huber covariance: high-probability upper and low-ratio lower bounds
Statement
Assume AC. Fix and an integer . Let be independent with common law from Gaussian Huber contamination model for covariance estimation, where and is arbitrary. If , , and for sufficiently large universal , then every Borel measurable restricted matrix-depth estimator, from either the global single-block correspondence or the bounded-class correspondence, satisfies with probability at least , uniformly over and .
Such Borel maximizing selectors exist by Measurable selection of a matrix-depth maximizer.
There are constants such that whenever , for every , The constants may depend on . The class is one common correlated block, not a row-sparsity class. The infimum is over all Borel maps .
Facts & Assumptions
Given: AC, , , the Gaussian Huber model, and the stated confidence and sample-size restrictions.
Operator error bound for the Gaussian Huber matrix-depth estimator gives the directional error bound over a union of coordinate spheres, for a Borel statistic satisfying the empirical-depth comparison.
Clean block-sparse Gaussian covariance has squared operator lower rate s log(ep/s) over n gives, under AC, the clean tail-risk lower bound of order when its sample-size condition holds.
Huber covariance modulus lower bound for unrestricted matrix-valued actions: under AC, a clean tail-risk lower bound for all matrix-valued estimators and a finite contamination modulus give the Huber lower bound at threshold , for the same unrestricted action space.
Single-block sparse covariance class and restricted directions: off-diagonal support lies in one common coordinate block of size at most , and the operator norm is bounded by .
The set of -element subsets and the binomial coefficient , for ; hence , the quotient is a natural number, and , The factorial and the falling factorial , defined by recursion in , The canonical natural of a field, and Laws of finite sums and products in , and : identifying naturals with their real embeddings, for integers , and .
The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Sums, scalar multiples, products and quotients: , , , and when , The second fundamental theorem: if is differentiable on with and is integrable, then , The real exponential function and the number by a power series, The exponential function is strictly increasing, Integer powers , and Laws of integer exponents: is increasing, , and the integral of on is by the antiderivative .
Every nonempty finite set of reals has a maximum and a minimum: a nonempty finite set of real numbers has a maximum; applying this to the absolute diagonal entries gives a coordinate attaining their largest absolute value.
Measurable selection of a matrix-depth maximizer supplies Borel maximizers for the global and bounded-class correspondences. A global maximizer dominates in depth; in the bounded case belongs to the search class by the target spectrum bound.
Proof
By [F7], Borel maximizers exist in both versions and satisfy [F1]'s empirical-depth comparison. Put and . By [F8], . Since for and , summing over these intervals and using [F9] gives . Exponentiating with [F9] yields , hence and . Enumerate the coordinate sets of size and take , in [F1]. If , choose blocks of size at most supporting the off-diagonal entries of its two summands, and let be their union. Then , entries between and vanish, and the block on is diagonal. Thus is block diagonal on , with symmetric block and diagonal block on . Its operator norm is the larger block norm: for , is the sum of the squared norms of the two block outputs, and a norm-maximizing vector in either nonempty finite-dimensional block attains its block norm. If and either or , [F5] gives a unit eigenvector attaining , supported in . If and , then , and any coordinate unit vector belongs to because ; it attains . In every remaining case and (with the empty-block norm set to zero). Write . By [F10] choose with . For every unit , , and the coordinate vector attains equality. By [F5], therefore attains . In either case some unit vector attaining has support of size at most . Since , its support extends to a set of size exactly , so the vector belongs to . Conversely every unit vector in is among all unit vectors, hence by [F5]. Finally, Squaring [F1]'s bound proves the displayed upper rate after adjusting .
By [F2], the clean lower premise holds at for sufficiently small , with a fixed positive probability . By [F3], the contamination modulus is at least . It is finite because for all pairs in the bounded class.
Apply [F4] with these clean and modulus bounds and the unrestricted matrix-valued estimator class in the Statement. Its threshold is at least a constant multiple of , and the probability lower bound is . Lowering the threshold only enlarges the event, which proves the lower assertion for the event probabilities in the Statement.
Authoring status
The lower proof uses the current batch-17 and batch-31 supplier bodies. The local measurable-selection proof discharges the selector-existence obligation for both global and bounded-class matrix-depth versions.
Depends on
- Gaussian Huber contamination model for covariance estimation
- Single-block sparse covariance class and restricted directions
- Matrix depth and covariance estimators
- Measurable selection of a matrix-depth maximizer
- Operator error bound for the Gaussian Huber matrix-depth estimator
- Clean block-sparse Gaussian covariance has squared operator lower rate s log(ep/s) over n
- The Huber covariance contamination modulus has a quadratic lower bound
- Huber covariance modulus lower bound for unrestricted matrix-valued actions
- The Axiom of Choice
- Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis
- The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le n$; hence $\binom{n}{k}\,k! = n^{\underline{k}}$, the quotient $n!/(k!(n-k)!)$ is a natural number, and $\binom{n}{k} = \binom{n}{n-k}$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Laws of finite sums and products in $\mathbb{N}$, and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- The natural logarithm as the inverse of the exponential function
- Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- The real exponential function and the number $e$ by a power series
- The exponential function is strictly increasing
- Integer powers $a^m$
- Laws of integer exponents
- Every nonempty finite set of reals has a maximum and a minimum
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
144 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
- Mengjie Chen, Chao Gao and Zhao Ren, Robust Covariance and Scatter Matrix Estimation under Huber's Contamination Model, Theorems 3.6, 3.7 and 5.1 (standard reference, not scraped)
- Philippe Rigollet, 18.S997 High-Dimensional Statistics Lecture Notes, MIT OpenCourseWare, Chapter 5 (standard reference, not scraped)