The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

TF-IDF concept

DefinitionA weighting of term counts by how rare the term is across the collection, so that a term in every document carries no weight. Equation 0.36.
ExampleA term appearing 5 times in a 100-word document and in 1 of 100 documents weighs 0.05 times the log of 100.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id tf-idf, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 0.36.

Assumptions and scope
  • A term’s weight is its frequency in the document times the logarithm of the document count over the number containing it. A term in every document carries no weight, the weight is nonnegative and falls as the term spreads, and the frequency lies in the unit interval.
  • It is a reader that reads rarity. The legal-citation flip used a frozen TF-IDF to SVD baseline trained on the training split only, and the flip tied while its magnitude overshot, which the ledger carries as partial.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/TFIDF.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
weighttheofspectrumkernelreader
Term frequency scaled down by how many documents carry the term.

Equation

Book equation 0.36.

\[w_{t,d}=\mathrm{tf}_{t,d}\cdot\ln\frac{N}{\mathrm{df}_t},\qquad \mathrm{tf}_{t,d}=\frac{\text{count of }t\text{ in }d}{\text{length of }d},\qquad \mathrm{df}_t=\text{documents containing }t.\]

Book equation 12.3.

\[\text{validated}\iff \mathrm{AUROC}_{\text{cross}}-\max\big(\mathrm{AUROC}_{\text{untrained}},\ \mathrm{AUROC}_{\text{BoW}}\big)\ \ge\ 0.10.\]

Conditions

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

Ledger

none

First stated

Spärck Jones, a statistical interpretation of term specificity, 1972, as chapter 0 section 0.17 states it, with the program’s frozen LSA baseline in ledger row GO-B-legal.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/TFIDF.lean, theorems weight_everywhere, weight_nonneg, weight_antitone, tf_mem_unit, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 0, 12.

Related

bag of words; retrieval-augmented pipeline; cross-corpus gate; quotient.

See also

Ledger rows that cite the entry’s records without naming it: GO-B-legal (035→036).

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.

← test statisticthreshold →