Prediction error

Conjectura.Defs.ComputerScience.Learning.PredictionError

/-
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/
import Mathlib.MeasureTheory.Measure.MeasureSpace

/-! # Prediction error

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Learning

open MeasureTheory

/-- 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}

end Conjectura.Learning