PAC learnability

IsPACLearnabledef

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 ε δ

Builds on

PAC learner

Used by

Problem CX-001 — the fundamental theorem of statistical learning

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