PAC learner

Conjectura.Defs.ComputerScience.Learning.PACLearner

/-
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.OptimalError
import Conjectura.Defs.ComputerScience.Learning.Learner
import Mathlib.MeasureTheory.Constructions.Pi

/-! # PAC learner

## 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 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 + ε}

end Conjectura.Learning