Version Space Learner: Measurable Selection via Countable Enumeration

A version space learner outputs the first hypothesis (in a fixed enumeration) consistent with the training data. For concept classes with a measurable enumeration enum : ℕ → Concept X Bool, Nat.find provides a constructive measurable selector.

Main Result

versionSpaceLearner_measurableBatchLearner: the version space learner satisfies MeasurableBatchLearner - it is a valid RL policy class.

Proof Architecture

For Y = Bool, the preimage of each singleton under the evaluation map decomposes as a countable union of measurable rectangles:

{(S, x) | learn S x = true} = ⋃ n, ({S | firstConsistent = n} ×ˢ {x | enum n x = true})

Measurability follows from measurable_to_countable' (Mathlib).

References

• Mitchell (1982): version spaces in computational learning theory
• Kuratowski-Ryll-Nardzewski: measurable selection (NOT in Mathlib - motivates the countable restriction)

Definitions

def IsConsistent {X : Type u} (h : Concept X Bool) {m : ℕ} (S : Fin m → X × Bool) : Prop

Consistency: hypothesis h predicts correctly on every example in sample S.

Equations

• IsConsistent h S = ∀ (i : Fin m), h (S i).1 = (S i).2

@[implicit_reducible]

instance isConsistent_decidable {X : Type u} (h : Concept X Bool) {m : ℕ} (S : Fin m → X × Bool) : Decidable (IsConsistent h S)

Decidability of consistency (finite conjunction of Bool equality).

Equations

• isConsistent_decidable h S = Fintype.decidableForallFintype

def IsFirstConsistent {X : Type u} (enum : ℕ → Concept X Bool) {m : ℕ} (S : Fin m → X × Bool) (n : ℕ) : Prop

The "first consistent index is n" predicate, stated without Nat.find. This is the measurability-friendly version: no proof-term dependence.

Equations

• IsFirstConsistent enum S n = (IsConsistent (enum n) S ∧ ∀ k < n, ¬IsConsistent (enum k) S)

noncomputable def versionSpaceLearner {X : Type u} [MeasurableSpace X] (enum : ℕ → Concept X Bool) : BatchLearner X Bool

Version space learner: select the first consistent hypothesis in the enumeration. Falls back to the zero concept (always false) if no hypothesis is consistent.

Equations

• One or more equations did not get rendered due to their size.

Measurability Infrastructure

theorem measurableSet_isConsistent {X : Type u} [MeasurableSpace X] (enum : ℕ → Concept X Bool) (h_meas : ∀ (n : ℕ), Measurable (enum n)) (m n : ℕ) : MeasurableSet {S : Fin m → X × Bool | IsConsistent (enum n) S}

Each "enum n is consistent with S" event is measurable in S.

theorem measurableSet_isFirstConsistent {X : Type u} [MeasurableSpace X] (enum : ℕ → Concept X Bool) (h_meas : ∀ (n : ℕ), Measurable (enum n)) (m n : ℕ) : MeasurableSet {S : Fin m → X × Bool | IsFirstConsistent enum S n}

The "first consistent index is n" event is measurable.

theorem nat_find_eq_iff_isFirstConsistent {X : Type u} (enum : ℕ → Concept X Bool) {m : ℕ} (S : Fin m → X × Bool) (h : ∃ (n : ℕ), IsConsistent (enum n) S) (n : ℕ) : Nat.find h = n ↔ IsFirstConsistent enum S n

Bridge: Nat.find h = n ↔ IsFirstConsistent.

theorem measurableSet_versionSpace_true {X : Type u} [MeasurableSpace X] [MeasurableSingletonClass X] (enum : ℕ → Concept X Bool) (h_meas : ∀ (n : ℕ), Measurable (enum n)) (m : ℕ) : MeasurableSet ((fun (p : (Fin m → X × Bool) × X) => (versionSpaceLearner enum).learn p.1 p.2) ⁻¹' {true})

The preimage of {true} under the evaluation map is measurable. Core lemma: decompose as countable union of measurable rectangles.

Main Theorem

theorem versionSpaceLearner_measurableBatchLearner {X : Type u} [MeasurableSpace X] [MeasurableSingletonClass X] (enum : ℕ → Concept X Bool) (h_meas : ∀ (n : ℕ), Measurable (enum n)) : MeasurableBatchLearner X (versionSpaceLearner enum)

Version space learners are MeasurableBatchLearners.

For any measurable enumeration of concepts, the learner that selects the first consistent hypothesis satisfies joint measurability. This makes version space learners valid RL policy classes.

Proof: measurable_to_countable' reduces to showing each singleton preimage is MeasurableSet. For {true}, decompose as ⋃ₙ (Aₙ ×ˢ Bₙ). For {false}, take the complement.