TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Multivariate trimmed-mean bound under sample replacement

Statement

Let $X$ be an absolutely continuous random vector in $R^{d}$ with mean $μ$ and finite covariance matrix $Σ$ as defined in Basic finite covariance matrix identities for robust mean bounds. Let $X_{1}, \dots, X_{N}, Y_{1}, \dots, Y_{N}$ be $2 N$ iid clean copies and let their observed replacement sample have at most $⌊ 2 η N ⌋$ changed coordinates in total. Assume $0 \leq η \leq 1 / 10$ , $0 < δ < 1$ , and $N \geq 2560 \log (2 / δ)$ . Set $ε = \max {10 η, 2560 \log (2 / δ) / N}$ and let $\hat{μ}$ be the repaired, total selector in Adaptive multivariate trimmed mean. Then there is a universal constant $c > 0$ such that

P ⁣ (∥ \hat{μ} - μ ∥ \leq c [\sqrt{\frac{tr Σ}{N}} + \sqrt{\frac{λ_{\max} (Σ) \log (1 / δ)}{N}} + \sqrt{λ_{\max} (Σ) η}]) \geq 1 - δ .

The claim is restricted to the displayed domain, which ensures $ε \leq 1$ . No guarantee is asserted for $1 / 10 < η < 1 / 2$ , for $η \geq 1 / 2$ , or for atomic laws.

Facts & Assumptions

Given: The iid clean law, replacement coupling and parameters in the Statement.

[F1]

Correct-scale slab bound for multivariate trimming gives a nonempty dyadic tail intersection with radius $16 ε Q_{0}$ outside probability $δ$ when the covariance trace is positive.

[F2]

The multivariate trimmed-mean rate follows from a correct-scale slab event turns a radius $b ε Q_{0}$ into the displayed rate with an explicit universal constant $c_{b}$ ; it applies at $b = 16$ .

[F3]

Exact recovery by the multivariate trimmed mean at zero covariance gives exact recovery when the covariance trace is zero. Basic finite covariance matrix identities for robust mean bounds gives nonnegative covariance trace.

[F4]

Adaptive multivariate trimmed mean and Totality and measurability of the repaired multivariate trimmed-mean selector supply the total Borel selector on every admissible observed input.

Proof

Given: The objects and hypotheses in the Statement.

1.1F1F2F4given

If $tr Σ > 0$ , [F1] supplies, with probability at least $1 - δ$ , the nonempty correct-scale tail intersection of radius $16 ε Q_{0}$ . On that event [F2] at $b = 16$ bounds the output of [F4] by exactly the displayed three-term rate, with universal constant $c_{16}$ . The selector's measurability in [F4] makes the error event measurable.

2.1F3step 1.1algebra∎

If $tr Σ = 0$ , [F3] gives exact recovery almost surely, so the error bound holds with probability one. These are the only cases by [F3], and the same positive constant $c_{16}$ works in both. Thus the claimed probability is at least $1 - δ$ throughout the stated domain.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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

Gábor Lugosi and Shahar Mendelson, Robust Multivariate Mean Estimation: The Optimality of Trimmed Mean, Theorem 2 and proof (standard reference, not scraped)
Gábor Lugosi, Mean Estimation in High Dimension, §3.2 (standard reference, not scraped)