Closure of Measurable Learners under Combiners and Selection

The algebra of MeasurableBatchLearners is closed under:

• arbitrary Boolean combiners (combineLearner)
• majority-vote boosting (boostLearner)
• measurable-set interpolation (interpLearner)
• countable selection (concatLearner)

Part 1: combineLearner

noncomputable def combineLearner {X : Type u} [MeasurableSpace X] (k : ℕ) (F : X → (Fin k → Bool) → Bool) (L : Fin k → BatchLearner X Bool) : BatchLearner X Bool

Combines k learners by a measurable Boolean function. Given learners L₁, …, Lₖ and a jointly measurable combiner F : X × (Fin k → Bool) → Bool, returns a learner whose prediction at x is F applied to x and the vector of base predictions. The foundational closure operation: every other operation in this file is a special case.

Equations

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

Part 2: Measurability of combineLearner

theorem measurableBatchLearner_combine {X : Type u} [MeasurableSpace X] (k : ℕ) (F : X → (Fin k → Bool) → Bool) (hF : Measurable fun (p : X × (Fin k → Bool)) => F p.1 p.2) (L : Fin k → BatchLearner X Bool) (hL : ∀ (i : Fin k), MeasurableBatchLearner X (L i)) : MeasurableBatchLearner X (combineLearner k F L)

combineLearner preserves MeasurableBatchLearner whenever the combiner F is jointly measurable. Factored through measurability of coordinate projections in the product σ-algebra.

Part 3: Boost learner via majority vote

noncomputable def boostLearner {X : Type u} [MeasurableSpace X] (k : ℕ) (L : Fin k → BatchLearner X Bool) : BatchLearner X Bool

Boosting via majority vote. Runs k base learners on the same training sample and outputs the majority of their predictions at each query point. Used in the boost_two_thirds_to_pac reduction that promotes a weak learner with success probability at least 2/3 to a full PAC learner; the quantitative 7/12-Chebyshev step lives in the proof of that reduction, not in the construction itself.

Equations

• boostLearner k L = combineLearner k (fun (x : X) (v : Fin k → Bool) => majority_vote k v) L

theorem measurableBatchLearner_boost {X : Type u} [MeasurableSpace X] (k : ℕ) (L : Fin k → BatchLearner X Bool) (hL : ∀ (i : Fin k), MeasurableBatchLearner X (L i)) : MeasurableBatchLearner X (boostLearner k L)

Boosting preserves measurability. Majority vote is a measurable Boolean function of finitely many inputs, so boostLearner inherits measurability via measurableBatchLearner_combine.

Part 4: Interpolation learner

noncomputable def interpLearner {X : Type u} [MeasurableSpace X] (A : Set X) (L₁ L₂ : BatchLearner X Bool) : BatchLearner X Bool

Spatial interpolation: uses learner L₁ on a region A ⊆ X and learner L₂ on its complement. The piecewise selector uses x ∈ A directly; measurability of A is not required by the definition and appears only in the accompanying measurableBatchLearner_interp theorem. The constructive content of the Complexity/Interpolation.lean module.

Equations

• interpLearner A L₁ L₂ = combineLearner 2 (fun (x : X) (v : Fin 2 → Bool) => if x ∈ A then v 0 else v 1) fun (i : Fin 2) => if i = 0 then L₁ else L₂

theorem measurableBatchLearner_interp {X : Type u} [MeasurableSpace X] (A : Set X) (hA : MeasurableSet A) (L₁ L₂ : BatchLearner X Bool) (h₁ : MeasurableBatchLearner X L₁) (h₂ : MeasurableBatchLearner X L₂) : MeasurableBatchLearner X (interpLearner A L₁ L₂)

interpLearner preserves measurability when the region A is measurable. The indicator of A composed with Measurable.ite and the two component learners gives a measurable conditional selector.

Part 5: Uniform measurability for indexed families

class UniformMeasurableBatchFamily {X : Type u} [MeasurableSpace X] (L : ℕ → BatchLearner X Bool) : Prop

A family of batch learners indexed by ℕ with a uniform joint measurability guarantee: for each m, the map (n, S, x) ↦ (L n).learn S x on ℕ × (Fin m → X × Bool) × X is measurable. Required wherever a learner construction selects among infinitely many components, in particular by concatLearner and the monad's bind. Pointwise measurability of each individual L n is the easier consequence (UniformMeasurableBatchFamily.pointwise); uniformity is the substantive requirement.

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

theorem UniformMeasurableBatchFamily.pointwise {X : Type u} [MeasurableSpace X] (L : ℕ → BatchLearner X Bool) [hL : UniformMeasurableBatchFamily L] (n : ℕ) : MeasurableBatchLearner X (L n)

A uniform measurable batch family is pointwise measurable: each individual L n belongs to MeasurableBatchLearner. The uniform property factors through the constant index embedding n ↦ (n, ·).

Part 6: Concat learner with measurable selection

noncomputable def concatLearner {X : Type u} [MeasurableSpace X] (L : ℕ → BatchLearner X Bool) (sel : {m : ℕ} → (Fin m → X × Bool) → ℕ) : BatchLearner X Bool

Sequential composition via a selector. Given a family of learners and a selector sel : {m : ℕ} → (Fin m → X × Bool) → ℕ, runs L (sel S) on sample S. The composite hypothesis space is the union of the component spaces. No measurability requirement on sel is imposed at the definition level; the accompanying measurableBatchLearner_concat theorem adds that hypothesis to derive closure under the uniform-measurable family. The construction underlying the monadic bind.

Equations

• concatLearner L sel = { hypotheses := ⋃ (n : ℕ), (L n).hypotheses, learn := fun {m : ℕ} (S : Fin m → X × Bool) (x : X) => (L (sel S)).learn S x, output_in_H := ⋯ }

theorem measurableBatchLearner_concat {X : Type u} [MeasurableSpace X] (L : ℕ → BatchLearner X Bool) [hL : UniformMeasurableBatchFamily L] (sel : {m : ℕ} → (Fin m → X × Bool) → ℕ) (hsel : ∀ (m : ℕ), Measurable fun (S : Fin m → X × Bool) => sel S) : MeasurableBatchLearner X (concatLearner L fun {m : ℕ} => sel)

concatLearner preserves measurability when the selector is measurable and the family is uniformly measurable. Composes the selector's measurability with the family's uniform measurability to obtain joint measurability of the evaluation map in (S, x).