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

Bounded sample-mean change under replacements and a common corrupted sample

Example

For integers $N \geq 1$ and $0 \leq k \leq N$ , if $x_{i}, y_{i} \in [0, 1]$ and at most $k$ coordinates differ, then

∣ N^{- 1} \sum_{i = 1}^{N} y_{i} - N^{- 1} \sum_{i = 1}^{N} x_{i} ∣ \leq k / N .

For the coupling example, take $X = Θ = {0, 1}$ with their full power-set sigma-algebras (Measurable spaces and measurable sets) and the experiment $P_{θ} = δ_{θ}$ (Statistical experiments, The Dirac set function at a point, A Dirac set function is a probability measure). For $N = 2$ and replacement fraction $η = 1 / 2$ , the clean samples $(0, 0)$ and $(1, 1)$ can both be changed to $(0, 1)$ with one replacement, so the two parameter values induce the same observed law.

Facts & Assumptions

Given: Clean iid samples and a sample-replacement coupling as defined in Adversarial sample replacement.

[F1]

Adversarial sample replacement: the clean vector is iid and the mismatch count is at most $⌊ η N ⌋$ almost surely; the adversary may depend on the clean sample.

[F2]

Huber contamination model: under the Huber model the observed coordinates are iid from one common mixture law.

[F3]

Measurable spaces and measurable sets, Statistical experiments, The Dirac set function at a point, and A Dirac set function is a probability measure: the two-point experiment on full power sets has clean law $δ_{θ}$ at each $θ \in {0, 1}$ , so its size-two clean iid samples are $(0, 0)$ and $(1, 1)$ almost surely.

Verification

1.1givenalgebra

Let $I = {i : x_{i} \neq y_{i}}$ , with $∣ I ∣ \leq k$ . Since $x_{i}, y_{i} \in [0, 1]$ , each changed coordinate satisfies $∣ y_{i} - x_{i} ∣ \leq 1$ , and $∣ N^{- 1} \sum_{i} (y_{i} - x_{i}) ∣ = ∣ N^{- 1} \sum_{i \in I} (y_{i} - x_{i}) ∣ \leq ∣ I ∣ / N \leq k / N$ .

1.2F1F3givenconstruct

Use a one-point probability space for each coupling. By [F3], at parameter $0$ the clean iid sample is $(0, 0)$ ; set the observed vector to $(0, 1)$ . At parameter $1$ the clean sample is $(1, 1)$ ; set the observed vector to $(0, 1)$ . Each coupling changes exactly one of two coordinates, which is the allowed $⌊ (1 / 2) 2 ⌋ = 1$ replacement, so both observed laws are the same point mass.

2.1F1F2step 1.2algebra∎

A rule that sees only the observed vector receives the same value $(0, 1)$ under both parameter laws, so it cannot identify both parameters. The observed vector is not iid: its first coordinate is $0$ almost surely and its second is $1$ almost surely, whereas [F2] requires identical coordinate laws. Thus this replacement mechanism is distinct from iid Huber contamination.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

P. B. Stark, Statistics 240 Lecture Notes, Part 9: Robustness and Related Topics, §1.2, PDF pp. 10–12 (standard reference, not scraped)