ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge 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.

The sample mean as a quadratic M-estimator

Example

Let $X_{1}, X_{2}, \dots$ be IID with law $P$ , where $P ∣ X ∣ < \infty$ and $P X^{2} < \infty$ . Let $Θ = R$ with its usual metric and set $m_{θ} (x) = - (x - θ)^{2}$ . For a finite observed sample $x_{1}, \dots, x_{n}$ , the empirical criterion $P_{n} m_{θ}$ has the unique maximizer ${\overset{ˉ}{x}}_{n} = n^{- 1} \sum_{i} x_{i}$ . The population criterion $P m_{θ}$ has the unique maximizer $μ = P X$ . The map from a sample to ${\overset{ˉ}{x}}_{n}$ is measurable, so it is an exact M-estimator.

Facts & Assumptions

Given: A finite real sample $x_{1}, \dots, x_{n}$ and, for the population claim, a probability law $P$ on $R$ with $P ∣ X ∣ < \infty$ and $P X^{2} < \infty$ .

[F1]

M-estimators: An M-estimator is a measurable exact or approximate maximizer or minimizer of the empirical criterion $P_{n} m_{θ}$ .

[F2]

Estimator sequences in IID experiments: An estimator sequence is a sequence of measurable maps on the finite IID product sample spaces.

[F3]

The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded: The usual metric on $R$ is $d (x, y) = ∣ x - y ∣$ .

[F4]

Identical distribution and IID families: IID means a common law and mutual independence of the whole family.

[A1]

The sample space is $R^{n}$ with product topology and Borel sigma-algebra generated by open sets. For finite $n$ , rational open boxes form a countable basis, so this Borel sigma-algebra is $B (R)^{\otimes n}$ . The criterion is $m_{θ} (x) = - (x - θ)^{2}$ .

[A2]

The population law has finite first and second absolute moments as stated.

Verification

1.1A1givenalgebra

Write ${\overset{ˉ}{x}}_{n} = n^{- 1} \sum_{i} x_{i}$ . Expanding both sides gives $\sum_{i} (x_{i} - θ)^{2} = \sum_{i} (x_{i} - {\overset{ˉ}{x}}_{n})^{2} + n (θ - {\overset{ˉ}{x}}_{n})^{2}$ , because $\sum_{i} (x_{i} - {\overset{ˉ}{x}}_{n}) = 0$ . Thus $P_{n} m_{θ} = P_{n} m_{{\overset{ˉ}{x}}_{n}} - (θ - {\overset{ˉ}{x}}_{n})^{2}$ , which is uniquely maximized at ${\overset{ˉ}{x}}_{n}$ .

1.2A2givenalgebra

Let $μ = P X$ . Expanding $X - θ = (X - μ) + (μ - θ)$ and using $P (X - μ) = 0$ gives $P m_{θ} = - P [(X - μ)^{2}] - (θ - μ)^{2}$ . The moment assumptions make the mean and centered second moment finite, so this is uniquely maximized at $μ$ .

2.1A1F1F2F3F4step 1.1givenalgebra∎

The IID sequence in [F4] gives the repeated-sampling context. If every coordinate of $x, y \in R^{n}$ differs by less than $δ$ , then $∣ {\overset{ˉ}{x}}_{n} (x) - {\overset{ˉ}{x}}_{n} (y) ∣ \leq n^{- 1} \sum_{i} ∣ x_{i} - y_{i} ∣ < δ$ . Hence the sample-mean map is continuous for the product topology. Inverse images of open sets are open, so the map is Borel measurable under [A1]; it is an estimator sequence by [F2] and is an exact M-estimator by [F1] and step 1.1. The target metric is the usual metric in [F3].

This example identifies the finite-sample and population criteria. It does not claim the global uniform-convergence premise on the noncompact set $R$ ; that premise must be checked separately before applying the consistency theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

Peter Bartlett, Theoretical Statistics, Stat 210B Lecture 15, mean criterion, PDF p. 5 (standard reference, not scraped)
Yen-Chi Chen, UW STAT 581, Chapter 3 M-estimation, nonlinear-regression least-squares criterion, lines 142–150 (standard reference, not scraped)