Conjectura
Sign inRegister
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 →

Optimal error

Conjectura.Defs.ComputerScience.Learning.OptimalError

/-
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/
import Conjectura.Defs.ComputerScience.Learning.PredictionError
import Conjectura.Defs.ComputerScience.Learning.ConceptClass

/-! # Optimal 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 **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

end Conjectura.Learning