LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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 block budget for the covariance geometric-median pilot

Statement

Assume Countable Choice. Let $X_{1}, \dots, X_{m} \in R^{p}$ be iid with mean $μ$ , finite covariance $Σ$ , and $T = tr Σ$ . For $β > 1$ , put $k = ⌊ 3.5 β ⌋ + 1 \leq m / 2$ . Partition the sample into $k$ consecutive blocks by the deterministic balanced rule of Geometric median of block means, and let $\hat{μ}$ be the selected minimum-norm geometric median of their block means. Then $P ⁣ (∥ \hat{μ} - μ ∥_{2} > 11 \sqrt{\frac{T (β + 1)}{m}}) \leq e^{- β} .$ In particular the larger radius $B = 11 \sqrt{2 T β / m}$ has the same failure bound. This proves the prescribed covariance-pilot block count without relying on the robust-mean theorem's different confidence convention.

Facts & Assumptions

Given: Countable Choice, iid observations with finite covariance, the balanced block partition, and $β > 1$ , $k = ⌊ 3.5 β ⌋ + 1 \leq m / 2$ .

[F1]

A geometric median is close when a strict majority is close: if a geometric median of $k$ points is farther than $C_{a} r$ from $z$ , more than $a k$ points are farther than $r$ from $z$ , where $C_{a} = (1 - a) / \sqrt{1 - 2 a}$ for $0 < a < 1 / 2$ .

[F2]

Covariance matrix of a finite-dimensional random vector: $T = tr Σ = E ∥ X_{i} - μ ∥_{2}^{2}$ .

[F3]

Independent random elements, Disjoint groups of an independent sigma-algebra family remain independent, Measurable coordinatewise functions preserve independence, Independent random elements have product joint law, and Fubini's theorem for L^1 functions on a sigma-finite product: disjoint blocks of an iid sample, their block means, and the bad-block indicators are independent; integrable cross-products of independent centered vectors have expectation zero by the product law and Fubini.

[F4]

Expectation of a nonnegative or integrable random variable, Markov's inequality for random variables, and Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: nonnegative Markov bounds apply, and finite second moment implies integrability for the block cross-products.

[F5]

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, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, and For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : the logarithm has derivative $1 / x$ and its laws, the chain rule and FTC apply, the mean value theorem turns a zero derivative into constancy, and $t^{N} \to 0$ for $0 < t < 1$ . These facts justify the logarithmic series calculation in step 3.1.

[F6]

The real exponential function and the number $e$ by a power series, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , and The exponential function is strictly increasing: $\exp (x + y) = \exp (x) \exp (y)$ and $\exp$ is strictly increasing.

[F7]

Geometric median of block means, Measurable minimum-norm geometric-median selection, and The Axiom of Countable Choice ( ${A C}_{ω}$ ): the prescribed deterministic partition and minimum-norm geometric-median selector are single-valued and Borel under Countable Choice.

Proof

technique · direct

Given: The iid sample, its finite covariance, the deterministic balanced partition, Countable Choice, and the displayed $β, k$ conditions.

1.1givenF2F3F4F7algebra

Suppose $T > 0$ , put $a = 7 / 18$ , $q = 1 / 10$ , $b = ⌊ m / k ⌋$ , and $r = \sqrt{T / (q b)}$ . For a block of size $b_{j}$ , expand $E ∥ b_{j}^{- 1} \sum_{i \in B_{j}} (X_{i} - μ) ∥_{2}^{2}$ : diagonal terms sum to $b_{j} T$ by [F2], and each cross term has expectation zero by [F3], because it is integrable by [F4] and the centered factors are independent. Thus $E ∥ M_{j} - μ ∥_{2}^{2} = T / b_{j} \leq T / b$ . Markov [F4] gives $P (∥ M_{j} - μ ∥_{2} > r) \leq q$ . Grouping and measurable images in [F3] make the bad-block indicators independent.

2.1F1F3F4F6step 1.1algebra

Let $W$ be the number of bad blocks. For any $λ > 0$ , independence gives $E e^{λ W} \leq (1 - q + q e^{λ})^{k}$ : each Bernoulli factor is $1 + P (bad) (e^{λ} - 1) \leq 1 + q (e^{λ} - 1)$ , and [F3, F6] factor the product. Since $a > q$ , choose $λ = \log (a (1 - q) / (q (1 - a))) > 0$ . Markov [F4] then gives $P (W \geq a k) \leq e^{- k ψ (a; q)}$ , where $ψ (a; q) = a \log (a / q) + (1 - a) \log ((1 - a) / (1 - q))$ , by substituting this $λ$ and simplifying. By [F1], $∥ \hat{μ} - μ ∥_{2} > C_{a} r$ implies $W > a k$ , so its probability is at most this bound.

3.1F5F6step 2.1algebra

For $x > 1$ put $t = (x - 1) / (x + 1) \in (0, 1)$ , so $x = (1 + t) / (1 - t)$ . For $0 \leq u \leq t$ , the function $g (u) = \log ((1 + u) / (1 - u))$ has $g (0) = 0$ and, by [F5], $g^{'} (u) = 1 / (1 + u) + 1 / (1 - u) = 2 / (1 - u^{2})$ . The function $I (u) = 2 \int_{0}^{u} (1 - v^{2})^{- 1} d v$ has the same derivative by FTC and the same value at zero, so the mean value theorem applied to $g - I$ gives $g (t) = I (t)$ . Integrating $\frac{1}{1 - u^{2}} = \sum_{j = 0}^{N} u^{2 j} + \frac{u^{2 N + 2}}{1 - u^{2}}$ yields the partial logarithm series plus a remainder between zero and $2 t^{2 N + 3} / ((2 N + 3) (1 - t^{2}))$ , which tends to zero by [F5]. Thus $\log x = 2 \sum_{j \geq 0} t^{2 j + 1} / (2 j + 1)$ . For $t_{1} = 13 / 22$ and $t_{2} = 13 / 68$ , the positive series and its geometric tail give $\log (35 / 9) > 2 (t_{1} + t_{1}^{3} / 3 + t_{1}^{5} / 5 + t_{1}^{7} / 7) > 27 / 20$ and $\log (81 / 55) \leq 2 (t_{2} + t_{2}^{3} / 3 + t_{2}^{5} / (5 (1 - t_{2}^{2}))) < 39 / 100$ . Hence $ψ (7 / 18; 1 / 10) > (7 / 18) (27 / 20) - (11 / 18) (39 / 100) = 43 / 150 > 2 / 7$ . Since $k > (7 / 2) β$ , [F6] gives $e^{- k ψ} < e^{- β}$ .

4.1givenF2F4F7step 3.1algebra∎

For $a = 7 / 18$ and $q = 1 / 10$ , $C_{a}^{2} = 121 / 72$ . Since $b \geq m / (2 k)$ and $k \leq (7 / 2) β + 1$ , the radius in step 3.1 satisfies $C_{a}^{2} r^{2} \leq (605 / 18) ((7 / 2) β + 1) T / m \leq 121 (β + 1) T / m$ . Thus the event at radius $11 \sqrt{T (β + 1) / m}$ is contained in the event bounded in step 3.1. If $T = 0$ , Markov's inequality applied to $∥ X_{i} - μ ∥_{2}^{2}$ shows $X_{i} = μ$ almost surely for each $i$ ; a finite intersection makes every block mean equal $μ$ , and the selected median equals $μ$ . Finally, because $β > 1$ , $11 \sqrt{2 T β / m}$ is at least the stated radius.

Depends on

Used by

Dependency tree · two levels

122 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

Minsker and Wei, Estimation of the Covariance Structure of Heavy-Tailed Distributions (standard reference, not scraped)