Ordinal Extensions

Extends ℕ∞-valued complexity measures to ordinal-valued ones for universal learning theory. WithTop ℕ has a single infinity (⊤); Ordinal has ω, ω², ε₀, ... The embedding ℕ∞ ↪ Ordinal sends n ↦ n and ⊤ ↦ ω, but ordinal VC dimension can take values beyond ω.

BddAbove infrastructure for nat-to-ordinal iSup

Ordinal has ConditionallyCompleteLinearOrderBot, not CompleteLattice, so every ciSup/le_ciSup_of_le call needs an explicit BddAbove witness.

Key invariant: (n : ℕ) : Ordinal is always < ω, so ω bounds every nat-cast-to-ordinal range uniformly.

theorem ordinalVCDim_inner_bddAbove (X : Type u) (C : ConceptClass X Bool) (S : Finset X) : BddAbove (Set.range fun (x : Shatters X C S) => ↑S.card)

Inner BddAbove: for a fixed S, the range over shattering witnesses is trivially bounded.

theorem ordinalVCDim_outer_bddAbove (X : Type u) (C : ConceptClass X Bool) : BddAbove (Set.range fun (S : Finset X) => ⨆ (_ : Shatters X C S), ↑S.card)

Outer BddAbove: the range of the full OrdinalVCDim iSup is bounded by ω. Holds for all concept classes regardless of whether VCDim is finite or infinite.

structure VCLTree (X : Type u) : Type (max 1 u)

VCL tree: combines VC dimension and Littlestone dimension into a single ordinal-valued measure. Used in universal learning trichotomy.

• value : Ordinal.{0}

  The ordinal value of the combined VC-Littlestone measure

• conceptClass : ConceptClass X Bool

  The concept class this measures

noncomputable def OrdinalVCDim (X : Type u) (C : ConceptClass X Bool) : Ordinal.{u_1}

Ordinal VC dimension: extends VCdim to ordinal values.

Equations

• OrdinalVCDim X C = ⨆ (S : Finset X), ⨆ (_ : Shatters X C S), ↑S.card

noncomputable def OrdinalLittlestoneDim (X : Type u) (C : ConceptClass X Bool) : Ordinal.{u_1}

Ordinal Littlestone dimension.

Equations

• OrdinalLittlestoneDim X C = ⨆ (T : MistakeTree X), ⨆ (_ : MistakeTree.isShattered X C T), ↑T.depth

theorem VCDim_embed_ordinal (X : Type u) (C : ConceptClass X Bool) (n : ℕ) (h : VCDim X C = ↑n) : OrdinalVCDim X C = ↑n

Embedding: finite VCDim embeds into OrdinalVCDim.