Conjectura
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Prediction error

predictionErrordef

The prediction error (0–1 loss) of a hypothesis h under a joint distribution D on α × β: the probability that h disagrees with the label.

noncomputable def predictionError {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (D : Measure (α × β)) (h : α → β) : ENNReal :=
  D {p : α × β | h p.1 ≠ p.2}

import Conjectura.Defs.ComputerScience.Learning.PredictionError · maintainer — open · raw source

Adapted for Conjectura from cslib, split into one concept per module. Released by its authors under Apache 2.0.

Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger

Full credits