Optimal error

optimalErrordef

The optimal error of a concept class is the least predictionError achievable by any concept in it. In the realisable setting this is zero; in the agnostic setting it is the benchmark a learner must approach.

noncomputable def optimalError {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (D : Measure (α × β)) (C : ConceptClass α β) : ENNReal :=
  ⨅ c ∈ C, predictionError D c

Builds on

Prediction error
Concept class

Used by

PAC learner

import Conjectura.Defs.ComputerScience.Learning.OptimalError · 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