LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Binary zero-one excess risk with a zero-score error convention

Statement

For a binary supervised problem with the full power-set sigma-algebra on $Y \in {- 1, + 1}$ , conditional positive-label probability $η$ , and any measurable real-valued score $h$ , use $R_{01} (h) = P (Y h (X) \leq 0)$ and $R_{01}^{*} = E \min {η (X), 1 - η (X)}$ . Then $R_{01} (h) - R_{01}^{*} = 2 E ⁣ [∣ η (X) - \frac{1}{2} ∣ 1_{{h (X) (η (X) - \frac{1}{2}) \leq 0}}] + E ⁣ [\min {η (X), 1 - η (X)} 1_{{h (X) = 0}}] .$

Statement references

Binary surrogate classification risk: fixes $η$ , $R_{01}$ , and $R_{01}^{*}$ , including the zero-score-is-error convention.

Mohri et al., Lemma 4.5, printed pp. 74–75 (PDF pp. 91–92): the source predicts $+ 1$ at zero, and its displayed equality overcounts when $h (x) = 0$ and $η (x) > 1 / 2$ ; the corrected zero-score-is-error identity above is proved here.

Facts & Assumptions

Given: A binary supervised problem, its conditional probability function $η$ , and a measurable real-valued score $h$ .

[F1]

For every measurable feature event ${X \in A}$ , $P (Y = + 1, X \in A) = E [η (X) 1_{{X \in A}}]$ . A finite label has a conditional probability function

[F2]

$R_{01} (h)$ is the population risk of the indicator loss $1_{{y h \leq 0}}$ , and $R_{01}^{*} = E \min (η, 1 - η)$ . Population and empirical risk Binary surrogate classification risk

[F3]

A measurable real-valued function has measurable preimages of Borel intervals, including its sign sets and the threshold set ${η \geq 1 / 2}$ . A measurable function between measurable spaces

Proof

1.1F1F2F3givenalgebra

Put $A_{-} = {x : h (x) \leq 0}$ and $A_{+} = {x : h (x) \geq 0}$ , which are measurable by [F3]. The event ${Y h (X) \leq 0}$ is the disjoint union of ${Y = + 1, X \in A_{-}}$ and ${Y = - 1, X \in A_{+}}$ . Applying [F1] to $A_{-}$ and using $P (X \in A_{+}, Y = - 1) = P (X \in A_{+}) - P (X \in A_{+}, Y = + 1)$ gives $R_{01} (h) = E [η (X) 1_{A_{-}} (X) + (1 - η (X)) 1_{A_{+}} (X)] .$ Subtracting [F2]'s Bayes-risk integrand reduces the identity to a pointwise comparison for each $x$ .

2.1step 1.1F2algebra

Fix $x$ and abbreviate $a = η (x)$ . If $a > 1 / 2$ , then on $h (x) > 0$ the conditional risk is $1 - a$ and the excess is zero; on $h (x) < 0$ it is $a$ , so the excess is $2 a - 1 = 2 ∣ a - 1 / 2 ∣$ ; on $h (x) = 0$ it is $1$ , so the excess is $a = (2 a - 1) + (1 - a)$ . If $a < 1 / 2$ , the same three cases $h (x) < 0$ , $h (x) > 0$ , and $h (x) = 0$ give excesses $0$ , $1 - 2 a = 2 ∣ a - 1 / 2 ∣$ , and $1 - a = (1 - 2 a) + a$ , respectively. If $a = 1 / 2$ , every nonzero score has excess zero and a zero score has excess $1 / 2$ . In each case the excess equals $2 ∣ a - 1 / 2 ∣ 1_{{h (x) (a - 1 / 2) \leq 0}} + \min (a, 1 - a) 1_{{h (x) = 0}}$ .

3.1step 1.1step 2.1algebra

Integrating the pointwise equality in step 2.1 and using step 1.1 proves the displayed risk identity.

4.1F1F2F3step 3.1algebra∎

The right side of the identity is nonnegative, so every measurable score has risk at least $R_{01}^{*}$ . Define $h_{B} (x) = + 1$ when $η (x) \geq 1 / 2$ and $h_{B} (x) = - 1$ otherwise. Its two level sets are measurable by [F3]; at each $x$ , its conditional zero-one risk is $\min {η (x), 1 - η (x)}$ , including equality at $η = 1 / 2$ . Thus $R_{01} (h_{B}) = R_{01}^{*}$ , verifying that the stated Bayes risk is the attained infimum.

Depends on

Used by

Surrogate regret controls classification regret with explicit tie and scale terms Theorem

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, 2nd ed., Chapter 4, Section 4.7, Lemma 4.5, printed pp. 74–75 (PDF pp. 91–92) (standard reference, not scraped)
Rick Durrett, Probability: Theory and Examples, 5th ed., Section 4.1 (standard reference, not scraped)