PAC learnability

Conjectura.Defs.ComputerScience.Learning.PACLearnable

/-
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.PACLearner

/-! # PAC learnability

## 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

/-- A concept class is **PAC learnable** over a family of distributions when for every accuracy
and confidence there is a sample size and an `IsPACLearner` achieving them, uniformly over the
family. This is the central definition of statistical learning theory. -/
def IsPACLearnable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (C : ConceptClass α β) (𝒟 : Set (Measure (α × β))) : Prop :=
  ∀ ε δ : ENNReal, 0 < ε → 0 < δ →
    ∃ m : ℕ, ∃ L : Learner α β m, ∀ D ∈ 𝒟, IsPACLearner L D C ε δ

end Conjectura.Learning