Version Space

The version space of a concept class C given a labeled sample S is the subset of C whose concepts agree with S on every observed point — the classical "concepts still consistent with the data" of Mitchell (1977) and Angluin (1980).

Main definitions

• VersionSpace C S: the subset of C whose concepts agree with S on every sample point.
• IsConsistent A C: a learner is consistent with C if its output always lies in the version space at the received sample.
• empiricalMiscount h S: number of sample points where h errs ([DecidableEq β]).
• empiricalMeasure S: the uniform Dirac mixture over the sample.
• empiricalError h S: the empirical distribution's mass on the disagreement set.
• Realizable C S: some concept in C labels every sample point correctly.

Main results

• versionSpace_subset, versionSpace_empty_sample, versionSpace_reindex, versionSpace_antitone, versionSpace_mono_C: structural properties.
• mem_versionSpace_iff_empiricalMiscount_zero: combinatorial bridge.
• mem_versionSpace_iff_empiricalError_zero: measure-theoretic bridge.
• IsConsistent.empiricalMiscount_eq_zero, IsConsistent.empiricalError_eq_zero: consistent learners achieve zero error / miscount on every sample.
• mem_versionSpace_of_realizable, Realizable.versionSpace_nonempty: realizable samples give non-empty version spaces.
• ae_mem_versionSpace_of_realizable: under iid sampling from a realizable joint distribution, the target concept lies in the version space almost surely.

References

• [Mit77]
• [Mit82]
• [Ang80]
• [Mit97]

Version Space

def Cslib.MachineLearning.PACLearning.VersionSpace {α : Type u_1} {β : Type u_2} {m : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) : ConceptClass α β

The version space of a concept class C given a labeled sample S: the set of concepts in C whose labels agree with S on every observed point.

Equations

• Cslib.MachineLearning.PACLearning.VersionSpace C S = {h : α → β | h ∈ C ∧ ∀ (i : Fin m), h (S i).1 = (S i).2}

theorem Cslib.MachineLearning.PACLearning.mem_versionSpace_iff {α : Type u_1} {β : Type u_2} {m : ℕ} {C : ConceptClass α β} {S : LabeledSample α β m} {h : α → β} : h ∈ VersionSpace C S ↔ h ∈ C ∧ ∀ (i : Fin m), h (S i).1 = (S i).2

Membership in the version space unfolds to concept membership plus per-sample consistency.

theorem Cslib.MachineLearning.PACLearning.versionSpace_subset {α : Type u_1} {β : Type u_2} {m : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) : VersionSpace C S ⊆ C

The version space is a subset of the original concept class.

theorem Cslib.MachineLearning.PACLearning.versionSpace_empty_sample {α : Type u_1} {β : Type u_2} (C : ConceptClass α β) (S : LabeledSample α β 0) : VersionSpace C S = C

Version space on the empty sample equals the whole concept class.

theorem Cslib.MachineLearning.PACLearning.versionSpace_reindex {α : Type u_1} {β : Type u_2} {m n : ℕ} (f : Fin m → Fin n) (C : ConceptClass α β) (S : LabeledSample α β n) : VersionSpace C S ⊆ VersionSpace C (S ∘ f)

Version space reindexing. For any reindexing f : Fin m → Fin n, the version space on S is contained in the version space on the reindexed sample S ∘ f.

theorem Cslib.MachineLearning.PACLearning.versionSpace_antitone {α : Type u_1} {β : Type u_2} {m n : ℕ} (hmn : m ≤ n) (C : ConceptClass α β) (S : LabeledSample α β n) : VersionSpace C S ⊆ VersionSpace C (S ∘ Fin.castLE hmn)

Version space antitonicity. Given a sample of size n and m ≤ n, the version space on all n observations is a subset of the version space on the first m observations. Special case of versionSpace_reindex with f := Fin.castLE hmn.

theorem Cslib.MachineLearning.PACLearning.versionSpace_mono_C {α : Type u_1} {β : Type u_2} {m : ℕ} {C C' : ConceptClass α β} (hCC' : C ⊆ C') (S : LabeledSample α β m) : VersionSpace C S ⊆ VersionSpace C' S

Version space is monotone in the concept class.

Empirical Error

def Cslib.MachineLearning.PACLearning.empiricalMiscount {α : Type u_1} {β : Type u_2} [DecidableEq β] {m : ℕ} (h : α → β) (S : LabeledSample α β m) : ℕ

The empirical miscount of a hypothesis h on a labeled sample S: the number of sample points where h predicts incorrectly.

Equations

• Cslib.MachineLearning.PACLearning.empiricalMiscount h S = {i : Fin m | h (S i).1 ≠ (S i).2}.card

noncomputable def Cslib.MachineLearning.PACLearning.empiricalMeasure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {m : ℕ} (S : LabeledSample α β m) : MeasureTheory.Measure (α × β)

The empirical distribution of a labeled sample: the uniform mixture of Dirac measures at each sample point. Equals the zero measure when m = 0.

Equations

• Cslib.MachineLearning.PACLearning.empiricalMeasure S = if _hm : m = 0 then 0 else (↑m)⁻¹ • ∑ i : Fin m, MeasureTheory.Measure.dirac (S i)

noncomputable def Cslib.MachineLearning.PACLearning.empiricalError {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {m : ℕ} (h : α → β) (S : LabeledSample α β m) : ENNReal

The empirical 0-1 error of h on S: the empirical distribution's mass on the disagreement set.

Equations

• Cslib.MachineLearning.PACLearning.empiricalError h S = Cslib.MachineLearning.PACLearning.error (Cslib.MachineLearning.PACLearning.empiricalMeasure S) h

theorem Cslib.MachineLearning.PACLearning.mem_versionSpace_iff_empiricalMiscount_zero {α : Type u_1} {β : Type u_2} [DecidableEq β] {m : ℕ} {C : ConceptClass α β} {S : LabeledSample α β m} {h : α → β} : h ∈ VersionSpace C S ↔ h ∈ C ∧ empiricalMiscount h S = 0

Version-space membership equals concept-class membership plus zero empirical miscount (combinatorial bridge).

theorem Cslib.MachineLearning.PACLearning.mem_versionSpace_iff_empiricalError_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] {m : ℕ} {C : ConceptClass α β} {S : LabeledSample α β m} {h : α → β} : h ∈ VersionSpace C S ↔ h ∈ C ∧ empiricalError h S = 0

Version-space membership equals concept-class membership plus zero empirical error (measure-theoretic bridge).

theorem Cslib.MachineLearning.PACLearning.empiricalError_eq_div {α : Type u_1} {β : Type u_2} [DecidableEq β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] {m : ℕ} (hm : 0 < m) (h : α → β) (S : LabeledSample α β m) : empiricalError h S = ↑(empiricalMiscount h S) / ↑m

The empirical 0-1 error equals the empirical miscount divided by the sample size.

Consistent Learners

def Cslib.MachineLearning.PACLearning.IsConsistent {α : Type u_1} {β : Type u_2} {m : ℕ} (A : Learner α β m) (C : ConceptClass α β) : Prop

A learner is consistent with the concept class C if, on every labeled sample it receives, its output hypothesis lies in the version space of C at that sample — i.e. the output is in C and agrees with every observed labeled pair.

Equations

• Cslib.MachineLearning.PACLearning.IsConsistent A C = ∀ (S : Cslib.MachineLearning.PACLearning.LabeledSample α β m), A S ∈ Cslib.MachineLearning.PACLearning.VersionSpace C S

theorem Cslib.MachineLearning.PACLearning.IsConsistent.output_mem_conceptClass {α : Type u_1} {β : Type u_2} {m : ℕ} {A : Learner α β m} {C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) : A S ∈ C

A consistent learner's output is always in the concept class.

theorem Cslib.MachineLearning.PACLearning.IsConsistent.output_agrees {α : Type u_1} {β : Type u_2} {m : ℕ} {A : Learner α β m} {C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) (i : Fin m) : A S (S i).1 = (S i).2

A consistent learner's output agrees with the sample on every observed point.

theorem Cslib.MachineLearning.PACLearning.IsConsistent.empiricalMiscount_eq_zero {α : Type u_1} {β : Type u_2} [DecidableEq β] {m : ℕ} {A : Learner α β m} {C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) : empiricalMiscount (A S) S = 0

A consistent learner has zero empirical miscount on every sample.

theorem Cslib.MachineLearning.PACLearning.IsConsistent.empiricalError_eq_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] {m : ℕ} {A : Learner α β m} {C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) : empiricalError (A S) S = 0

A consistent learner has zero empirical error on every sample.

Realizable case

def Cslib.MachineLearning.PACLearning.Realizable {α : Type u_1} {β : Type u_2} {m : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) : Prop

A labeled sample S is realizable by concept class C if some concept in C labels every sample point correctly.

Equations

• Cslib.MachineLearning.PACLearning.Realizable C S = ∃ c ∈ C, ∀ (i : Fin m), (S i).2 = c (S i).1

theorem Cslib.MachineLearning.PACLearning.mem_versionSpace_of_realizable {α : Type u_1} {β : Type u_2} {m : ℕ} {C : ConceptClass α β} {c : α → β} (hc : c ∈ C) (S : LabeledSample α β m) (hS : ∀ (i : Fin m), (S i).2 = c (S i).1) : c ∈ VersionSpace C S

Realizable version-space nonemptiness. If a target concept c lies in C and the sample S is labeled by c (i.e. every (S i).2 = c (S i).1), then c itself lies in the version space VersionSpace C S.

theorem Cslib.MachineLearning.PACLearning.Realizable.versionSpace_nonempty {α : Type u_1} {β : Type u_2} {m : ℕ} {C : ConceptClass α β} {S : LabeledSample α β m} (h : Realizable C S) : Set.Nonempty (VersionSpace C S)

A realizable sample has nonempty version space.

Probabilistic Realizable

theorem Cslib.MachineLearning.PACLearning.ae_mem_versionSpace_of_realizable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {C : ConceptClass α β} {c : α → β} (hc : c ∈ C) (hcm : Measurable c) (hG : MeasurableSet {p : α × β | p.2 = c p.1}) (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (m : ℕ) : ∀ᵐ (S : LabeledSample α β m) ∂MeasureTheory.Measure.pi fun (x : Fin m) => MeasureTheory.Measure.map (fun (x : α) => (x, c x)) P, c ∈ VersionSpace C S

Under iid sampling from the realizable joint distribution induced by c ∈ C and a probability measure P on α, the target concept c lies in the version space almost surely.