Core Learner Types

The three paradigm-specific learner types with incompatible signatures. There is no common parent type; the type system cannot express "learner" without choosing a paradigm, because the three signatures are fundamentally different:

• PAC learner: {m : ℕ} → (Fin m → X × Y) → Concept X Y (batch)
• Online learner: State → X → Y (sequential with internal state)
• Gold learner: List (X × Y) → Concept X Y (sequential, extensible)

This is intentional: a common parent would erase the structural properties that make each paradigm's theorems non-trivial.

structure BatchLearner (X : Type u) (Y : Type v) : Type (max u v)

A batch learner (PAC paradigm): takes a finite sample, returns a hypothesis.

• hypotheses : HypothesisSpace X Y

  The learner's hypothesis space

• learn {m : ℕ} : (Fin m → X × Y) → Concept X Y

  The learning algorithm: given a sample, produce a hypothesis

• output_in_H {m : ℕ} (S : Fin m → X × Y) : self.learn S ∈ self.hypotheses

  Output is in the hypothesis space

structure OnlineLearner (X : Type u) (Y : Type v) : Type (max (max 1 u) v)

An online learner: receives instances one at a time, makes predictions sequentially.

• State : Type

  Internal state type

• init : self.State

  Initial state

• predict : self.State → X → Y

  Predict: given current state and new instance, output a prediction

• update : self.State → X → Y → self.State

  Update: given current state, instance, and revealed true label, update state

structure GoldLearner (X : Type u) (Y : Type v) : Type (max u v)

A Gold-style learner (identification in the limit): receives a stream of data and at each step conjectures a hypothesis.

• conjecture : List (X × Y) → Concept X Y

  The learner's conjecture given data seen so far

Measurability Typeclasses

Regularity conditions for measure-theoretic PAC arguments. These replace ad hoc predicates (LearnEvalMeasurable, AdviceEvalMeasurable) and explicit hypothesis threading (hmeas_C, hc_meas, hWB).

The conditions identified here are the minimal requirements for:

• PAC success events to be MeasurableSet
• Section measure arguments (measurable_measure_prod_mk_left)
• PAC-Bayes bounds to be well-defined
• Information-theoretic generalization bounds (mutual information) to be statable

Reference: Krapp & Wirth, "Measurability in the Fundamental Theorem of Statistical Learning", arXiv:2410.10243, 2024.

class MeasurableBatchLearner (X : Type u) [MeasurableSpace X] (L : BatchLearner X Bool) : Prop

A batch learner whose evaluation map is jointly measurable.

The condition: for each sample size m, the map (S, x) ↦ L.learn S x from (Fin m → X × Bool) × X to Bool is Measurable.

This is the minimal regularity that makes the PAC success event {S | D{x | L.learn(S)(x) ≠ c(x)} ≤ ε} a MeasurableSet (via measurable_measure_prod_mk_left).

Equivalent to LearnEvalMeasurable (Separation.lean) and AdviceEvalMeasurable (Extended.lean) for the non-advice case.

• eval_measurable (m : ℕ) : Measurable fun (p : (Fin m → X × Bool) × X) => L.learn p.1 p.2

  Joint measurability of the evaluation map