Bridge Types: Connecting to Mathlib and Across Paradigms

Type infrastructure bridging our definitions to Mathlib types and connecting paradigm-specific types:

Bridge	Source	Target	Status
B₁	ConceptClass X Bool	Set (Set X)	Lossless for Bool (proved)
B₂	ConceptClass X Bool (Fintype)	Finset (Finset X)	NEW: connects to Mathlib
B₃	Shatters (ours)	Finset.Shatters (Mathlib)	NEW: key bridge
B₄	VCDim (ours)	Finset.vcDim (Mathlib K₁)	NEW: unlocks Sauer-Shelah
B₅	IIDSample	MeasureTheory.ProbabilityMeasure	Direct
B₆	WithTop ℕ	Ordinal	Embedding (ℕ∞ ↪ Ordinal)
B₇	BatchLearner ↔ GoldLearner	Cross-paradigm	No common parent (BP₁)

B₁: Function-Class ↔ Set-Family Bridge (Set-level)

For Y = Bool, the map c ↦ {x | c x = true} is a bijection between (X → Bool) and Set X. This is lossless because Bool-valued functions are determined by their level sets.

For Y with |Y| > 2, this bridge doesn't apply directly (BP₄ boundary).

def conceptClassToSetFamily (X : Type u) (C : ConceptClass X Bool) : Set (Set X)

Convert a concept class (set of functions) to a set family (set of subsets).

Equations

• conceptClassToSetFamily X C = {S : Set X | ∃ c ∈ C, S = {x : X | c x = true}}

noncomputable def setFamilyToConceptClass (X : Type u) (F : Set (Set X)) : ConceptClass X Bool

Convert a set family back to a concept class. Requires classical choice.

Equations

• setFamilyToConceptClass X F = {c : X → Bool | {x : X | c x = true} ∈ F}

theorem bridge_round_trip (X : Type u) (C : ConceptClass X Bool) : setFamilyToConceptClass X (conceptClassToSetFamily X C) = C

The round-trip is the identity for Bool-valued functions: distinct functions with the same level set get identified, but for Bool the level set determines the function. This is B₁'s losslessness proof.

B₂: Function-Class → Finset Family Bridge (Fintype-level)

This is the critical bridge to Mathlib's combinatorial shattering API. Requires [Fintype X] and [DecidableEq X] to produce Finsets.

The concept c : X → Bool maps to conceptToFinset c = {x ∈ univ | c x = true}. A finite concept class C : Finset (X → Bool) maps to conceptClassToFinsetFamily C = C.image conceptToFinset.

def conceptToFinset {X : Type u} [Fintype X] [DecidableEq X] (c : X → Bool) : Finset X

Convert a concept (X → Bool) to its level set as a Finset. This is the atomic bridge from function-representation to set-representation.

Equations

• conceptToFinset c = {x : X | c x = true}

def conceptClassToFinsetFamily {X : Type u} [Fintype X] [DecidableEq X] (C : Finset (X → Bool)) : Finset (Finset X)

Convert a finite concept class to a Finset family. Requires C to be a Finset (finite concept class). This is the source constraint: Mathlib's Finset.vcDim operates on finite families.

Equations

• conceptClassToFinsetFamily C = Finset.image conceptToFinset C

theorem conceptToFinset_injective {X : Type u} [Fintype X] [DecidableEq X] : Function.Injective conceptToFinset

The concept-to-finset map is injective: distinct Bool-valued functions produce distinct level sets. This ensures conceptClassToFinsetFamily preserves the cardinality of C.

B₃: Shatters Bridge (ours ↔ Mathlib's Finset.Shatters)

Our Shatters: ∀ f : S → Bool, ∃ c ∈ C, ∀ x : S, c x = f x "every labeling of S is realized by some c ∈ C"

Mathlib's Finset.Shatters: ∀ t ⊆ S, ∃ u ∈ 𝒜, S ∩ u = t "every subset of S appears as S ∩ u for some u ∈ 𝒜"

The correspondence: labeling f ↔ subset {x ∈ S | f x = true}. This equivalence holds because Bool has exactly two values.

theorem shatters_iff_finset_shatters {X : Type u} [Fintype X] [DecidableEq X] (C : Finset (X → Bool)) (S : Finset X) : Shatters X (↑C) S ↔ (conceptClassToFinsetFamily C).Shatters S

Our Shatters is equivalent to Mathlib's Finset.Shatters through the conceptToFinset bridge.

This is the KEY bridge theorem. It allows us to use Mathlib's Sauer-Shelah lemma (card_le_card_shatterer, card_shatterer_le_sum_vcDim) to prove bounds on our learning-theoretic growth function.

Proof strategy: →: Given t ⊆ S, define labeling f(x) = (x ∈ t). Our Shatters gives c ∈ C with c|_S = f. Then S ∩ conceptToFinset c = S ∩ {x | c x} = {x ∈ S | f x} = t. ←: Given f : S → Bool, let t = S.filter(f). Mathlib gives u ∈ 𝒜 with S ∩ u = t. Since u = conceptToFinset c for some c ∈ C, we get c|_S = f.

B₄: VCDim Bridge (ours ↔ Mathlib's Finset.vcDim)

Our VCDim: ⨆ (S : Finset X) (_ : Shatters X C S), S.card : WithTop ℕ Mathlib's Finset.vcDim: 𝒜.shatterer.sup card : ℕ

For [Fintype X], our VCDim is always finite (bounded by Fintype.card X), so the WithTop ℕ value is actually a natural number.

This bridge unlocks the full Mathlib shattering API:

• card_le_card_shatterer (Pajor's variant of Sauer-Shelah)
• card_shatterer_le_sum_vcDim (growth function bound)
• shatterer_compress_subset_shatterer (compression properties)
• vcDim_compress_le (down-compression preserves VC dim)

theorem vcdim_eq_finset_vcdim {X : Type u} [Fintype X] [DecidableEq X] (C : Finset (X → Bool)) : VCDim X ↑C = ↑(conceptClassToFinsetFamily C).vcDim

Our VCDim equals Mathlib's Finset.vcDim (cast to WithTop ℕ) for finite types.

This theorem connects our learning-theoretic VCDim (defined as a supremum over shattered sets in WithTop ℕ) to Mathlib's combinatorial vcDim (defined as shatterer.sup card in ℕ).

The proof requires shatters_iff_finset_shatters plus the equivalence between iSup over Shatters-witnesses and Finset.sup over shatterer members.

theorem vcdim_finite_of_fintype {X : Type u} [Fintype X] [DecidableEq X] (C : Finset (X → Bool)) : VCDim X ↑C < ⊤

VCDim is finite for finite concept classes over finite domains. This is a consequence of the bridge: Finset.vcDim is always finite (it's ℕ).

B₃': Restriction Bridge (concept class restricted to a subset)

For Sauer-Shelah quantitative: we need to restrict a concept class C to an m-element set S, producing a FINITE family of subsets of S. Then apply Mathlib's card_le_card_shatterer + card_shatterer_le_sum_vcDim.

The restriction of C to S: C|_S = { c ∩ S : c ∈ C } as a Finset (Finset S) = { conceptToFinset(c) ∩ S : c ∈ C.image (· ∘ Subtype.val) }

Since S is Finset X (finite), C|_S is a finite family over Finset S.

def restrictToFinset {X : Type u} (c : X → Bool) (S : Finset X) : ↥S → Bool

Restrict a concept (X → Bool) to a Finset S, producing a function S → Bool.

Equations

• restrictToFinset c S ⟨x_1, property⟩ = c x_1

def restrictConceptClass {X : Type u} [DecidableEq X] (C : Finset (X → Bool)) (S : Finset X) : Finset (↥S → Bool)

Restrict a finite concept class to a Finset S. Produces a Finset of functions S → Bool (the distinct restrictions).

Equations

• restrictConceptClass C S = Finset.image (fun (c : X → Bool) => restrictToFinset c S) C

theorem growthFunction_le_card_restrict {X : Type u} [Fintype X] [DecidableEq X] (C : Finset (X → Bool)) (S : Finset X) : (restrictConceptClass C S).card ≤ C.card

The number of distinct restrictions is our GrowthFunction. GrowthFunction X C m = max over m-element S of |C|_S|. This lemma connects GrowthFunction to the restriction operation.

def funcToSubsetFamily {X : Type u} [DecidableEq X] (S : Finset X) (fs : Finset (↥S → Bool)) : Finset (Finset ↥S)

Sauer-Shelah via Mathlib: |C|S| ≤ Σ{i ≤ d} C(|S|, i). The proof chain:

1. Convert C|_S to a Finset family over S (conceptToFinset on restrictions)
2. Apply card_le_card_shatterer: |𝒜| ≤ |𝒜.shatterer|
3. Apply card_shatterer_le_sum_vcDim: |𝒜.shatterer| ≤ Σ C(|S|, i) for i ≤ vcDim(𝒜)
4. Show vcDim(𝒜) ≤ d (restriction doesn't increase VCDim) This requires building the S-local Finset family from C|_S.

Equations

• funcToSubsetFamily S fs = Finset.image (fun (f : ↥S → Bool) => {x : ↥S | f x = true}) fs

theorem card_restrict_le_sauer_shelah_bound {X : Type u} [Fintype X] [DecidableEq X] (C : Finset (X → Bool)) (S : Finset X) (d : ℕ) (hd : (conceptClassToFinsetFamily C).vcDim = d) : (restrictConceptClass C S).card ≤ ∑ i ∈ Finset.range (d + 1), S.card.choose i

theorem growth_function_le_sauer_shelah {X : Type u} [Fintype X] [DecidableEq X] (C : Finset (X → Bool)) (d : ℕ) (hd : (conceptClassToFinsetFamily C).vcDim = d) (m : ℕ) (_hm : d ≤ m) : GrowthFunction X (↑C) m ≤ ∑ i ∈ Finset.range (d + 1), m.choose i

B₅: IIDSample ↔ ProbabilityMeasure Bridge (K₃: MeasureTheory)

def iidSampleToProbMeasure (X : Type u) (Y : Type v) [MeasurableSpace X] [MeasurableSpace Y] (S : IIDSample X Y) : MeasureTheory.Measure (X × Y)

Extract the probability measure from an IID sample. Direct bridge — no information loss.

Equations

• iidSampleToProbMeasure X Y S = S.distribution

instance iidSampleIsProbability (X : Type u) (Y : Type v) [MeasurableSpace X] [MeasurableSpace Y] (S : IIDSample X Y) : MeasureTheory.IsProbabilityMeasure S.distribution

The IIDSample distribution is a probability measure.

B₆: WithTop ℕ ↪ Ordinal Bridge (BP₂)

noncomputable def withTopNatToOrdinal : WithTop ℕ → Ordinal.{u_1}

Embedding of WithTop ℕ into Ordinal. n ↦ n, ⊤ ↦ ω. This is injective but NOT surjective: ordinals ≥ ω+1 have no preimage.

Equations

• withTopNatToOrdinal (some n) = ↑n
• withTopNatToOrdinal none = Ordinal.omega0

theorem withTopNatToOrdinal_mono (a b : WithTop ℕ) : a ≤ b → withTopNatToOrdinal a ≤ withTopNatToOrdinal b

The embedding preserves order.

theorem vcdim_to_ordinal_vcdim (X : Type u) (C : ConceptClass X Bool) : withTopNatToOrdinal (VCDim X C) ≤ OrdinalVCDim X C

VCDim embeds into OrdinalVCDim via this bridge. Γ₂₇ RESOLVED: uniform ω-bound BddAbove (from Ordinal.lean) makes le_ciSup_of_le work for all ordinal-valued nat-cast iSup. The bridge is paradigm-invariant.

B₇: Cross-Paradigm Learner Bridges (BP₁ boundary)

These bridges are LIMITED by BP₁: there is no lossless conversion between paradigm-specific learner types. But there are LOSSY conversions in one direction: Online → PAC is possible (every online learner induces a PAC learner). PAC → Online is NOT possible in general. Gold → PAC is NOT possible in general.

noncomputable def onlineToBatch (X : Type u) (Y : Type v) (OL : OnlineLearner X Y) : BatchLearner X Y

An online learner induces a batch learner: run the online algorithm on the sample in any order, return the final hypothesis.

Equations

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

def bayesianToBatch (X : Type u) (Y : Type v) [MeasurableSpace X] (BL : BayesianLearner X Y) : BatchLearner X Y

Bayesian learners can be viewed as batch learners by forgetting the prior.

Equations

• bayesianToBatch X Y BL = { hypotheses := BL.hypotheses, learn := fun {m : ℕ} => BL.learnMAP, output_in_H := ⋯ }

Complexity Measure Bridges

theorem compression_bounds_vcdim (X : Type u) (C : ConceptClass X Bool) (cs : CompressionScheme X Bool C) (hcs : 0 < cs.size) : VCDim X C ≤ ↑(2 * (cs.size + 1) * (cs.size + 1) - 1)