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.
Dense Gaussian Huber covariance: high-probability upper and capped lower bounds
Statement
Assume AC. Fix . Let be independent with common law from Gaussian Huber contamination model for covariance estimation, where and is arbitrary. If , , and for a sufficiently large universal , then every Borel measurable dense matrix-depth estimator, from either the global positive semidefinite correspondence or the bounded-class correspondence, from Matrix depth and covariance estimators 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 for every and every , The infimum is over all Borel maps . The constants may depend on .
Facts & Assumptions
Given: AC, the Gaussian Huber model, , arbitrary contaminating law , and the stated confidence and sample-size conditions.
Operator error bound for the Gaussian Huber matrix-depth estimator gives the directional operator-error bound for the dense sphere family, for a Borel statistic satisfying the empirical-depth comparison.
Clean Gaussian covariance has a capped squared operator lower rate gives, under AC, the clean tail-risk lower bound of order for all , retaining the original small-ratio result.
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.
Bounded-spectrum covariance class: every is positive semidefinite and has operator norm at most .
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 every such maximizer satisfies the comparison premise in [F1]. Take , one support , and in [F1]. For a real symmetric matrix , [F5] gives . Thus . Squaring and using gives the stated upper rate.
The all-regime clean lower bound [F2] supplies constants such that the clean tail-risk premise in [F4] holds for every with and . By [F3], the contamination modulus is at least . It is finite because for every pair in the bounded class.
Apply [F4] with the same unrestricted matrix-valued estimator class as in the Statement and the inputs from step 1.2. Its threshold is at least . Since , . Lowering to this capped threshold only enlarges the event, and the probability lower bound is . Renaming the two positive constants proves the all-dimension lower assertion. Its original uncapped rate remains valid whenever .
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
- Bounded-spectrum covariance class
- Matrix depth and covariance estimators
- Measurable selection of a matrix-depth maximizer
- Operator error bound for the Gaussian Huber matrix-depth estimator
- Clean Gaussian covariance has a capped squared operator lower rate
- 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||
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
63 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.1, 3.2 and 5.1 (standard reference, not scraped)
- Philippe Rigollet, 18.S997 High-Dimensional Statistics Lecture Notes, MIT OpenCourseWare, Chapter 5 (standard reference, not scraped)