The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

threshold concept

DefinitionThe value at which a score becomes a positive decision. Chapter 6.
ExampleScores 0.3, 0.6, and 0.9 at threshold 0.5 give one negative and two positives; at 0.7, two negatives and one positive.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id threshold, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 6.2.

Assumptions and scope
  • The value at which a score becomes a positive decision. Raising it can only shrink the predicted set, so true positives and false positives can only fall, which is why the ROC curve is traced by a single sweep, and below every score everything is positive while above every score nothing is.
  • A strictly increasing recalibration of the score with the matching recalibration of the threshold leaves every decision unchanged, which is the Monotone Invariance Theorem at the level of one decision.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Threshold.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
00.51-6-3036weighted sumscoredecision boundary at zero
The value that turns a score into a decision.

Equation

Book equation 6.2.

\[\begin{gathered} \max_{\tau,\ \mathrm{dir}}F_1\!\Big(\mathbf 1\big[\mathrm{dir}\big(g(f(X)),\tau\big)\big],\,y\Big)=\max_{\tau,\ \mathrm{dir}}F_1\!\Big(\mathbf 1\big[\mathrm{dir}\big(f(X),\tau\big)\big],\,y\Big) \\ \text{for every strictly monotone } g. \end{gathered}\]

Book equation 0.28.

\[P=\frac{TP}{TP+FP},\qquad R=\frac{TP}{TP+FN},\qquad F_1=\frac{2PR}{P+R}.\]

Conditions

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

Ledger

none

First stated

Chapter 6 section 6.1 of Data Mining as Observation, with the program’s threshold sweeps in theory-radar.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Threshold.lean, theorems predicted_anti, tp_anti, fp_anti, decision_comp, predicted_extremes, 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, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14.

Related

Monotone Invariance Theorem; Youden F1 bound; reliability weight; calibration.

See also

none

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.

← TF-IDFtoken →