PAC learner

IsPACLearnerdef

A learner is probably approximately correct at accuracy ε and confidence δ when, over the draw of an i.i.d. sample of size m, it outputs a hypothesis within ε of the best concept in the class with probability at least 1 - δ.

def IsPACLearner {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {m : ℕ}
    (L : Learner α β m) (D : Measure (α × β)) (C : ConceptClass α β) (ε δ : ENNReal) : Prop :=
  1 - δ ≤ (Measure.pi fun _ : Fin m => D)
    {S : Fin m → (α × β) | predictionError D (L S) ≤ optimalError D C + ε}

Builds on

Used by

PAC learnability

From Mathlib

MeasureTheory.Constructions.Pi

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