The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

cross-validation instrument

DefinitionSplitting the data into folds and evaluating on each fold a model trained on the others. Repeated cross-validation multiplies confidence it did not earn, chapter 8 section 8.5.
ExampleTen folds of 100 rows each test every row once, and the overall accuracy is the mean of the ten fold accuracies.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id cross-validation, kind instrument.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 8.2.

Assumptions and scope
  • Splitting the rows into folds and evaluating on each fold a model trained on the others, so every row is tested exactly once. The overall accuracy is the size-weighted mean of the fold accuracies, and with equal folds it is their plain mean.
  • The folds share training data, so repeated cross-validation multiplies confidence it did not earn, which the Nadeau and Bengio correction prices at one plus the fold count times the test-to-train ratio.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/CrossValidation.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
traintraintesttraintrainevery row is tested once across the 5 folds
Folds tested once each, sharing training data.

Equation

Book equation 8.2.

\[\begin{gathered} \widehat{\operatorname{Var}}_{\mathrm{NB}}=\Big(\frac1J+\frac{n_{\mathrm{test}}}{n_{\mathrm{train}}}\Big)\hat\sigma^{2}, \\ J=1000,\ \frac{n_{\mathrm{test}}}{n_{\mathrm{train}}}=\frac14\ \Rightarrow\ 1+250=251,\ \ \sqrt{251}=15.84. \end{gathered}\]

Book equation 0.18.

\[\widehat{\operatorname{Var}}_{\mathrm{NB}}=\Big(\frac1J+\frac{n_{\mathrm{test}}}{n_{\mathrm{train}}}\Big)\hat\sigma^{2},\qquad \frac{\widehat{\operatorname{Var}}_{\mathrm{NB}}}{\hat\sigma^{2}/J}=1+J\,\frac{n_{\mathrm{test}}}{n_{\mathrm{train}}}.\]

Conditions

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

Stone, cross-validatory choice, 1974, as chapter 8 section 8.5 of Data Mining as Observation reads it, with the program’s fold accounting in constraint-gap/review/FINDINGS.md:1-35.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/CrossValidation.lean, theorems sizes_sum, accuracy_weighted, accuracy_mean_of_equal, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation primer S, chapters 0, 1, 2, 4, 5, 6, 7, 8, 14.

Related

Nadeau and Bengio correction; harness; standard error; leakage.

See also

Sources-table rows that share a record with the entry without naming it: chapter 6 section 6.4, chapter 8 section 8.5.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← cross-support ratiocurvature →