def PACLearnable (X : Type u) [MeasurableSpace X]
    (C : ConceptClass X Bool) : Prop :=
  exists (L : BatchLearner X Bool) (mf : R -> R -> N),
    forall (e d : R), 0 < e -> 0 < d ->
      forall (D : Measure X), IsProbabilityMeasure D ->
        forall (c : Concept X Bool), c (*@$\in$@*) C ->
          let m := mf e d
          Measure.pi (fun _ : Fin m => D)
            { xs : Fin m -> X |
              D { x | L.learn (fun i => (xs i, c (xs i))) x (*@$\neq$@*) c x }
                (*@$\leq$@*) ENNReal.ofReal e }
            (*@$\geq$@*) ENNReal.ofReal (1 - d)

def OnlineLearnable (X : Type u) (Y : Type v) [DecidableEq Y]
    (C : ConceptClass X Y) : Prop :=
  exists (M : N), MistakeBounded X Y C M

def EXLearnable (X : Type u) (C : ConceptClass X Bool) : Prop :=
  exists (L : GoldLearner X Bool),
    forall (c : Concept X Bool), c (*@$\in$@*) C ->
      forall (T : TextPresentation X c),
        exists (t0 : N), forall (t : N), t (*@$\geq$@*) t0 ->
          L.conjecture (dataUpTo T.toDataStream t) = c