The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

F1 concept

DefinitionTwice the product of precision and recall over their sum. The optimal thresholded F1 of a score is the best F1 over every threshold and depends only on the score's ranking. Equation 0.28.
ExamplePrecision 0.6 and recall 0.75 give F1 of 2 times 0.45 over 1.35, or 0.667.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id f1, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 0.28.

Assumptions and scope
  • Twice the product of precision and recall over their sum. The optimal thresholded F1 of a score is the best F1 over every threshold in both directions, and it depends only on the score’s ranking, so a strictly monotone transform of the score leaves it unchanged.
  • Its ceiling from the Youden index holds for every score, and the AUROC form of that ceiling only for concave ROC curves, which is the theory-radar erratum.
Prior artnone recorded
Evidencetheory-radar/paper/astar_paper.tex:94-170, theory-radar/paper/theory_radar_paper.tex:290-304, lean/DataMiningAsObservation/MonotoneInvariance.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
00.5100.51false positive ratetrue positive rateoperating pointarea under the curve, AUROCchance is the diagonal
The harmonic mean of precision and recall at a threshold.

Equation

Book equation 0.28.

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

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 5.4.

\[\begin{gathered} F_1^{\max}\ \le\ \sup_{t\in[J,\,1]}\ \frac{2t\pi}{t\pi+\pi+(t-J)(1-\pi)},\qquad J=\max_{\tau}\big(\mathrm{TPR}-\mathrm{FPR}\big),\qquad \pi=\text{prevalence}, \\ J\le 2A-1\ \text{when the ROC curve is concave, and not in general.} \end{gathered}\]

Conditions

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

Ledger

none

First stated

Chapter 0 section 0.14 and chapter 6 section 6.3 of Data Mining as Observation, with the program’s optimal thresholded F1 in theory-radar, DOI 10.5281/zenodo.20660206.

Measurements

Where the book states it Numbers, as the book’s sources table records them Source
chapter 5 section 5.4 Monotone Invariance and AUROC invariance theorems, the AUROC to F1 bound via the Youden index, stated in the source for every ROC curve and corrected in the book to concave curves, with the counterexample at AUROC 0.75 and F1 0.857 theory-radar/paper/astar_paper.tex:94-170; theory-radar/paper/theory_radar_paper.tex:290-304

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/MonotoneInvariance.lean, theorems aurocNum_comp, auroc_comp, predicted_comp, predictedBelow_comp, sweptF1_comp, sweptF1Below_comp, optF1_comp, 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, 5, 6, 7.

Related

precision, recall; Monotone Invariance Theorem; Youden F1 bound; formula search; threshold.

See also

Sources-table rows that share a record with the entry without naming it: chapter 6 section 6.3.

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.

← explained variancefalse-clear rate →