Mann–Whitney statistic and ROC area

DefinitionEmpirical ROC rate at or above a threshold#✓fully proved

Empirical rate #{i | t ≤ z i} / k of scores at or above the threshold t (the true- or false-positive rate when z are the positive or negative scores).

noncomputable def rocRate {k : ℕ} (z : Fin k → ℝ) (t : ℝ) : ℝ :=
  (#{i | t ≤ z i} : ℝ) / k

Used by 3

Used byEmpirical area under the ROC curve · Empirical AUC = Mann–Whitney with ties · Strict ROC rate equals the rate at the next score

DefinitionEmpirical ROC rate strictly above a threshold#✓fully proved

Empirical rate #{i | t < z i} / k of scores strictly above t: the ROC coordinate at the next larger distinct score.

noncomputable def rocRateAbove {k : ℕ} (z : Fin k → ℝ) (t : ℝ) : ℝ :=
  (#{i | t < z i} : ℝ) / k

Used by 4

Used byEmpirical area under the ROC curve · Empirical AUC = Mann–Whitney with ties · Strict ROC rate equals the rate at the next score · Strict ROC rate vanishes above the largest score

DefinitionEmpirical area under the ROC curve#✓fully proved

Trapezoidal area under the empirical ROC curve of positive scores x and negative scores y: the sum over the distinct observed scores t of the trapezoid from the point (rocRateAbove y t, rocRateAbove x t) to (rocRate y t, rocRate x t).

noncomputable def empiricalAUC {m n : ℕ} (x : Fin m → ℝ) (y : Fin n → ℝ) : ℝ :=
  ∑ t ∈ univ.image x ∪ univ.image y,
    (rocRate y t - rocRateAbove y t) * (rocRate x t + rocRateAbove x t) / 2

Uses 2 · Used by 1

Statement usesEmpirical ROC rate at or above a threshold · Empirical ROC rate strictly above a threshold

Used byEmpirical AUC = Mann–Whitney with ties

DefinitionMann–Whitney U statistic#✓fully proved

Mann–Whitney count U = ∑ᵢ ∑ⱼ (1[y j < x i] + ½ 1[y j = x i]) of (positive, negative) pairs ranked correctly, with ties counted one half.

noncomputable def mannWhitneyU {m n : ℕ} (x : Fin m → ℝ) (y : Fin n → ℝ) : ℝ :=
  ∑ i, ∑ j, if y j < x i then 1 else if y j = x i then 1 / 2 else 0

Used by 1

Used byEmpirical AUC = Mann–Whitney with ties

TheoremStrict ROC rate equals the rate at the next score#✓fully proved

If no score lies strictly between t < t', the strict rate at t is the rate at t': the left end of the trapezoid at t is the ROC point of the next larger distinct score.

theorem rocRateAbove_eq_rocRate_of_forall_not_mem_Ioo {k : ℕ} {z : Fin k → ℝ} {t t' : ℝ}
    (htt' : t < t') (h : ∀ i, z i ∉ Set.Ioo t t') : rocRateAbove z t = rocRate z t'

Uses 2

Statement usesEmpirical ROC rate at or above a threshold · Empirical ROC rate strictly above a threshold

TheoremStrict ROC rate vanishes above the largest score#✓fully proved

Above the largest score the strict rate is zero: the first trapezoid starts at (0, 0).

theorem rocRateAbove_eq_zero_of_forall_le {k : ℕ} {z : Fin k → ℝ} {t : ℝ}
    (h : ∀ i, z i ≤ t) : rocRateAbove z t = 0

Uses 1

Statement usesEmpirical ROC rate strictly above a threshold

TheoremEmpirical AUC = Mann–Whitney with ties#✓fully proved

Empirical AUC = Mann–Whitney with ties (Bamber 1975): the trapezoidal area under the empirical ROC curve equals U / (m n), for nonempty samples.

theorem empiricalAUC_eq_mannWhitneyU {m n : ℕ} (hm : 0 < m) (hn : 0 < n)
    (x : Fin m → ℝ) (y : Fin n → ℝ) : empiricalAUC x y = mannWhitneyU x y / (m * n)

Uses 4

Statement usesEmpirical area under the ROC curve · Mann–Whitney U statistic

Proof usesEmpirical ROC rate at or above a threshold · Empirical ROC rate strictly above a threshold

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.