ExampleConstruction: AI-generatedVerification: 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.

A polynomial-tail law with finite variance

Example

Let $X$ have density $f (x) = \frac{3}{2 (1 + ∣ x ∣)^{4}}$ on $R$ . This law has mean $0$ and variance $1$ , but it is not sub-Gaussian in the moment-generating-function sense. The geometric-median-of-means theorem therefore applies even though no finite sub-Gaussian proxy exists.

Facts & Assumptions

Given: Countable Choice, the density $f (x) = 3 / (2 (1 + ∣ x ∣)^{4})$ , and the definitions of sub-Gaussianity and variance. Fix $0 < δ < 1$ and a positive integer $n$ for which $k = ⌊ \log (1 / δ) / ψ (7 / 18; 1 / 10) ⌋ + 1 \leq n / 2$ , with $ψ$ as defined in Finite-variance Hilbert mean bound for geometric medians of means. Let $X_{1}, \dots, X_{n}$ be iid Borel real-valued observations with this density, and let $\hat{μ}$ be their geometric-median-of-block-means output using $k$ blocks and the minimum-norm selection rule specified by that theorem. Countable Choice is an explicit hypothesis of Finite-variance Hilbert mean bound for geometric medians of means, whose selector uses Measurable minimum-norm geometric-median selection.

[F1]

A centered real random variable is sub-Gaussian with proxy $s^{2}$ only if $E e^{λ X} \leq e^{λ^{2} s^{2} / 2}$ for every real $λ$ (Sub-Gaussian variables and vectors, and sub-exponential variables).

[F2]

For the density displayed in the Example, symmetry and finite second moment identify the mean and variance; the geometric-median theorem requires a separable Hilbert-valued iid sample with finite second moment (Finite-variance Hilbert mean bound for geometric medians of means).

[F3]

With inner product $⟨ x, y ⟩ = x y$ , $R$ is a real inner-product space: ordered-field arithmetic gives bilinearity, symmetry, and $x^{2} \geq 0$ with equality only for $x = 0$ (The reals form a totally ordered field, Real and complex inner-product spaces and their induced length). Its induced norm is $\sqrt{x^{2}} = ∣ x ∣$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Basic properties of the absolute value), so completeness of the real line makes it a Hilbert space (The reals are complete, Hilbert space). The embedded rationals are countable and dense, so this Hilbert space is separable ( $Q$ is countably infinite, The rationals embed densely in the reals, Separability: the existence of an at most countable dense subset).

Verification

technique · direct

Given: Countable Choice, the displayed density, the iid sample $X_{1}, \dots, X_{n}$ , the admissible confidence parameter $δ$ and block count $k$ , and the estimator $\hat{μ}$ specified in Facts & Assumptions.

1.1F2algebra

The density is normalized because $\int_{R} f (x) d x = 3 \int_{0}^{\infty} (1 + x)^{- 4} d x = 1$ . Its second moment is $3 \int_{0}^{\infty} x^{2} (1 + x)^{- 4} d x = 3 \int_{1}^{\infty} (u^{- 2} - 2 u^{- 3} + u^{- 4}) d u = 1$ . Since $∣ x ∣ \leq 1 + x^{2}$ , the first absolute moment is finite, and symmetry then gives $E X = 0$ .

1.2F1algebra

For every $λ > 0$ , $E e^{λ X} \geq \frac{3}{2} \int_{1}^{\infty} e^{λ x} (1 + x)^{- 4} d x = \infty$ , since $λ x - 4 \log (1 + x) \to \infty$ and the integrand is eventually at least $1$ . Thus the defining MGF inequality in [F1] fails for every finite proxy.

2.1F2F3givenalgebra∎

The law is Borel and takes values in the separable Hilbert space $H = R$ by [F3], with finite second moment $1$ . For the iid sample and geometric-median-of-means estimator specified in the Given, the admissible $n$ , $δ$ , and $k$ therefore satisfy all hypotheses of Finite-variance Hilbert mean bound for geometric medians of means, which gives $P (∣ \hat{μ} ∣ \geq 11 \sqrt{\log (7 / (5 δ)) / n}) \leq δ$ . The conclusion uses only the finite variance just computed, not a sub-Gaussian assumption.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

90 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, §1 (standard reference, not scraped)