Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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 M>0. Let X1,…,Xn be independent with common law Pϵ,Σ,Q from Gaussian Huber contamination model for covariance estimation, where Σ∈Fp(M) and Q is arbitrary. If 0≤ϵ<1/5, 0<δ<1/2, and C1(p+log⁡(1/δ))/n<1 for a sufficiently large universal C1, 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 ∥Σ^−Σ∥op2≤CM[(pn∨ϵ2)+log⁡(1/δ)n] with probability at least 1−2δ, uniformly over Q and Σ∈Fp(M).

Such Borel maximizing selectors exist by Measurable selection of a matrix-depth maximizer.

There are constants cM,cM′>0 such that for every p,n≥1 and every 0≤ϵ≤1, inf⁡Σ~sup⁡Σ∈Fp(M)sup⁡QPϵ,Σ,Q⊗n ⁣{∥Σ~−Σ∥op2≥cMmin⁡{1,pn∨ϵ2}}≥cM′. The infimum is over all Borel maps (Rp)n→Rp×p. The constants may depend on M.

Facts & Assumptions

Given: AC, the Gaussian Huber model, Σ∈Fp(M), arbitrary contaminating law Q, and the stated confidence and sample-size conditions.

[F1]

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.

[F2]

Clean Gaussian covariance has a capped squared operator lower rate gives, under AC, the clean tail-risk lower bound of order min⁡{1,p/n} for all p,n≥1, retaining the original small-ratio result.

[F3]

The Huber covariance contamination modulus has a quadratic lower bound gives ω(ϵ,Fp(M))≥dMϵ2.

[F4]

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 116(M0∨ω), for the same unrestricted action space.

[F5]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: for real symmetric A, ∥A∥op=sup⁡∥u∥2=1∣uTAu∣.

[F6]

Bounded-spectrum covariance class: every Σ∈Fp(M) is positive semidefinite and has operator norm at most M.

[F7]

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

1.1F1F5F7algebra

By [F7], Borel maximizers exist in both versions and every such maximizer satisfies the comparison premise in [F1]. Take U=Sp−1, one support S1=[p], and r=p in [F1]. For a real symmetric matrix A, [F5] gives ∥A∥op=sup⁡∥u∥2=1∣uTAu∣. Thus ∥Σ^−Σ∥op≤CM(ϵ+(p+log⁡(1/δ))/n). Squaring and using (a+b)2≤2a2+2b2 gives the stated upper rate.

1.2F2F3F4F6algebra

The all-regime clean lower bound [F2] supplies constants aM,b0>0 such that the clean tail-risk premise in [F4] holds for every p,n≥1 with M0=aMmin⁡{1,p/n} and c0=b0. By [F3], the contamination modulus is at least dMϵ2. It is finite because ∥Σ0−Σ1∥op2≤4M2 for every pair in the bounded class.

2.1F2F3F4step 1.2algebra∎

Apply [F4] with the same unrestricted matrix-valued estimator class as in the Statement and the inputs from step 1.2. Its threshold 116(M0∨ω) is at least 116min⁡{aM,dM}(min⁡{1,p/n}∨ϵ2). Since 0≤ϵ≤1, min⁡{1,p/n}∨ϵ2=min⁡{1,(p/n)∨ϵ2}. Lowering to this capped threshold only enlarges the event, and the probability lower bound is min⁡(b0,1/2). Renaming the two positive constants proves the all-dimension lower assertion. Its original uncapped rate remains valid whenever p/n≤1.

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

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