LemmaStatement: AI-adaptedProof: 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.

Exact recovery by the multivariate trimmed mean at zero covariance

Statement

Let $X$ be a Borel random vector in $R^{d}$ , $d \geq 1$ , with finite second moment, mean $μ$ , and covariance matrix $Σ$ as defined in Basic finite covariance matrix identities for robust mean bounds. Let two halves of size $N$ be iid clean copies, and let the observed vector be a sample-replacement version with at most $⌊ 2 η N ⌋$ changed coordinates in total. Assume $0 \leq η \leq 1 / 10$ , $0 < δ < 1$ , and $N \geq 2560 \log (2 / δ)$ . With $ε = \max {10 η, 2560 \log (2 / δ) / N}$ , if $tr Σ = 0$ , then Adaptive multivariate trimmed mean returns $μ$ almost surely.

Facts & Assumptions

Given: The clean iid halves, their zero-trace covariance, the sample-replacement budget, and the displayed parameter domain.

[F1]

For a finite-second-moment vector, zero covariance trace implies that the clean law is concentrated at its mean (Basic finite covariance matrix identities for robust mean bounds).

[F2]

The replacement model allows at most $⌊ 2 η N ⌋$ changed entries among the full vector of length $2 N$ ; the clean entries are iid and the observed entries may depend on all clean data (Adversarial sample replacement, Identical distribution and IID families).

[F3]

The algorithm uses the second-half directional order statistics at ranks $⌈ ε N / 2 ⌉$ and $⌈ (1 - ε / 2) N ⌉$ , clips first-half projections to the interval expanded by $Q$ , and returns the minimum-norm point of the all-scale intersection when every $K_{j}$ is nonempty (Adaptive multivariate trimmed mean).

[F4]

On the stated domain, $0 < ε \leq 1$ and $ε \geq 10 η$ (Adaptive multivariate trimmed mean).

[F5]

The all-scale minimum-norm selector is single-valued whenever its intersection is nonempty (Totality and measurability of the repaired multivariate trimmed-mean selector).

Proof

technique · direct

Given: The zero-trace covariance, iid clean halves of size $N$ , the sample-replacement budget, and the displayed $η, δ, N$ domain.

1.1F1F2F3F4givenalgebra

By [F1] and iid sampling in [F2], with probability one every clean coordinate in both halves equals $μ$ . Fix any such clean realization and any admissible replacement output. Each observed half has at most $m \leq ⌊ 2 η N ⌋ \leq 2 η N \leq ε N / 5$ changed coordinates. Put $q = ε N / 2$ , so $m < q \leq N / 2$ . The two ranks in [F3] are $r_{-} = ⌈ q ⌉$ and $r_{+} = ⌈ N - q ⌉ = N - ⌊ q ⌋$ . They satisfy $m < r_{-}, r_{+}$ and $r_{-}, r_{+} \leq N - m$ : indeed $r_{-} \leq ⌈ N / 2 ⌉ \leq N - m$ , while $r_{+} \geq ⌈ N / 2 ⌉ > m$ and $r_{+} = N - ⌊ q ⌋ \leq N - m$ . Thus for every unit $v$ , both order statistics of the second half equal $⟨ μ, v ⟩$ , since the unaltered projections occupy all ranks from $m + 1$ through $N - m$ .

2.1F3F4step 1.1algebra

For any $Q > 0$ and unit $v$ , the unaltered first-half projections equal $⟨ μ, v ⟩$ , while each changed projection after clipping to $[⟨ μ, v ⟩ - Q, ⟨ μ, v ⟩ + Q]$ differs from it by at most $Q$ . By step 1.1 these are the clipping endpoints used by [F3], so $∣ U_{Q} (v) - ⟨ μ, v ⟩ ∣ \leq m Q / N \leq 2 η Q \leq ε Q / 5 < 2 ε Q$ . Hence $μ \in Γ (Q)$ for every dyadic $Q = 2^{i}$ , and $μ \in K_{j}$ for every integer $j$ . Therefore $S = Z$ in [F3].

3.1F3F5step 1.1step 2.1algebra∎

Let $z$ belong to the algorithm's all-scale intersection. For each fixed unit $v$ and every integer $i$ , its slab constraint and step 2.1 imply $∣ ⟨ z - μ, v ⟩ ∣ \leq ∣ ⟨ z, v ⟩ - U_{2^{i}} (v) ∣ + ∣ U_{2^{i}} (v) - ⟨ μ, v ⟩ ∣ \leq 2 ε 2^{i} + 2 η 2^{i}$ . Letting $i \to - \infty$ gives $⟨ z - μ, v ⟩ = 0$ for every unit $v$ . If $z \neq μ$ , choosing $v = (z - μ) / ∥ z - μ ∥_{2}$ contradicts that equality; thus the all-scale intersection is exactly ${μ}$ . Since $S = Z$ , [F3] and [F5] make the algorithm return its unique point $μ$ . The argument holds on the probability-one event from step 1.1, proving the claim.

Depends on

Used by

Multivariate trimmed-mean bound under sample replacement Theorem

Dependency tree · two levels

30 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, §3.1 (standard reference, not scraped)
Gábor Lugosi, Mean Estimation in High Dimension, §3.2 (standard reference, not scraped)