A generic countable-universe interface

The original core fixes the universe to ℕ, as in the finite-query Kleinberg--Mullainathan construction. Many later papers state their results over an arbitrary countable example space. This file supplies that generic paper-facing layer without changing the existing API.

A finite history of length t is represented by Fin t → α. Thus a Generator α is literally a function on finite sequences, while output G stream t exposes only the prefix strictly before time t.

@[reducible, inline]

abbrev GenLimit.Generic.Language (α : Type u_1) : Type u_1

A language over an arbitrary example type.

Equations

• GenLimit.Generic.Language α = Set α

@[reducible, inline]

abbrev GenLimit.Generic.LanguageClass (α : Type u_1) : Type u_1

A possibly uncountable class of languages.

Equations

• GenLimit.Generic.LanguageClass α = Set (GenLimit.Generic.Language α)

@[reducible, inline]

abbrev GenLimit.Generic.LanguageFamily (α : Type u_1) : Type u_1

An enumerated countable family of languages. Unlike LanguageClass, this representation preserves the paper's index order and repetitions.

Equations

• GenLimit.Generic.LanguageFamily α = (ℕ → GenLimit.Generic.Language α)

@[reducible, inline]

abbrev GenLimit.Generic.Stream (α : Type u_1) : Type u_1

An infinite stream of examples.

Equations

• GenLimit.Generic.Stream α = (ℕ → α)

@[reducible, inline]

abbrev GenLimit.Generic.Generator (α : Type u_1) : Type u_1

A generator is a map from each finite sequence to one new example.

Equations

• GenLimit.Generic.Generator α = ((t : ℕ) → (Fin t → α) → α)

def GenLimit.Generic.Presents {α : Type u_1} (stream : Stream α) (L : Language α) : Prop

Exact presentation: repetitions are allowed, and every target element must eventually occur.

Equations

• GenLimit.Generic.Presents stream L = (Set.range stream = L)

def GenLimit.Generic.StreamIn {α : Type u_1} (stream : Stream α) (L : Language α) : Prop

Every element ever shown by the stream belongs to L.

Equations

• GenLimit.Generic.StreamIn stream L = (Set.range stream ⊆ L)

noncomputable def GenLimit.Generic.sequenceSample {α : Type u_1} {t : ℕ} (xs : Fin t → α) : Finset α

The distinct values in a finite sequence.

Equations

• GenLimit.Generic.sequenceSample xs = Finset.image xs Finset.univ

noncomputable def GenLimit.Generic.sample {α : Type u_1} (stream : Stream α) (t : ℕ) : Finset α

The distinct observations strictly before time t.

Equations

• GenLimit.Generic.sample stream t = Finset.image stream (Finset.range t)

def GenLimit.Generic.historyThenFallback {α : Type u_1} (history : List α) (fallback : α) : Stream α

The stream that follows a finite history and then repeats a fallback value forever.

Equations

• GenLimit.Generic.historyThenFallback history fallback n = if h : n < history.length then history.get ⟨n, h⟩ else fallback

theorem GenLimit.Generic.streamIn_historyThenFallback {α : Type u_1} {history : List α} {fallback : α} {L : Language α} (hhistory : ∀ x ∈ history, x ∈ L) (hfallback : fallback ∈ L) : StreamIn (historyThenFallback history fallback) L

A finite history followed by a fallback stays in a language when both the history and fallback do.

def GenLimit.Generic.output {α : Type u_1} (G : Generator α) (stream : Stream α) (t : ℕ) : α

Run G on the prefix of stream strictly before time t.

Equations

• GenLimit.Generic.output G stream t = G t fun (i : Fin t) => stream ↑i

theorem GenLimit.Generic.mem_sequenceSample_iff {α : Type u_1} {t : ℕ} {xs : Fin t → α} {x : α} : x ∈ sequenceSample xs ↔ ∃ (i : Fin t), xs i = x

theorem GenLimit.Generic.sequenceSample_list_get {α : Type u_1} [DecidableEq α] (xs : List α) : sequenceSample xs.get = xs.toFinset

Passing a list through its canonical Fin-indexed input recovers its underlying finite set of values.

theorem GenLimit.Generic.sequenceSample_card_of_injective {α : Type u_1} {t : ℕ} (xs : Fin t → α) (hxs : Function.Injective xs) : (sequenceSample xs).card = t

An injective finite history has as many distinct observations as positions.

theorem GenLimit.Generic.sequenceSample_subset_of_pointwise {α : Type u_1} {t : ℕ} {xs : Fin t → α} {S : Set α} (hxs : ∀ (k : Fin t), xs k ∈ S) : ↑(sequenceSample xs) ⊆ S

Pointwise membership of a finite history implies membership of every element in its underlying sample.

theorem GenLimit.Generic.sequenceSample_equivFin_symm {α : Type u_1} (S : Finset α) : (sequenceSample fun (i : Fin S.card) => ↑(S.equivFin.symm i)) = S

Enumerating a finset through its canonical equivalence with Fin recovers exactly that finset as the distinct sample.

theorem GenLimit.Generic.equivFin_symm_value_injective {α : Type u_1} (S : Finset α) : Function.Injective fun (i : Fin S.card) => ↑(S.equivFin.symm i)

The value map of a finset's canonical Fin enumeration is injective.

theorem GenLimit.Generic.mem_sample_iff {α : Type u_1} {stream : Stream α} {t : ℕ} {x : α} : x ∈ sample stream t ↔ ∃ s < t, stream s = x

theorem GenLimit.Generic.sample_card_of_injective {α : Type u_1} (stream : Stream α) (hstream : Function.Injective stream) (t : ℕ) : (sample stream t).card = t

An injective stream has exactly t distinct observations before round t.

theorem GenLimit.Generic.sample_eq_of_eq_on_prefix {α : Type u_1} {stream₁ stream₂ : Stream α} {t : ℕ} (h : ∀ n < t, stream₁ n = stream₂ n) : sample stream₁ t = sample stream₂ t

Samples depend only on the corresponding finite stream prefix.

theorem GenLimit.Generic.sample_historyThenFallback_length {α : Type u_1} [DecidableEq α] (history : List α) (fallback : α) : sample (historyThenFallback history fallback) history.length = history.toFinset

Sampling a finite-history stream at the end of the history recovers exactly the history's distinct values.

theorem GenLimit.Generic.sequenceSample_prefix {α : Type u_1} (stream : Stream α) (t : ℕ) : (sequenceSample fun (i : Fin t) => stream ↑i) = sample stream t

theorem GenLimit.Generic.sample_mono {α : Type u_1} {stream : Stream α} {s t : ℕ} (hst : s ≤ t) : sample stream s ⊆ sample stream t

theorem GenLimit.Generic.value_mem_sample {α : Type u_1} {stream : Stream α} {s t : ℕ} (hst : s < t) : stream s ∈ sample stream t

theorem GenLimit.Generic.sample_card_step {α : Type u_1} (stream : Stream α) (t : ℕ) : (sample stream (t + 1)).card ≤ (sample stream t).card + 1

theorem GenLimit.Generic.exists_sample_card_eq_of_le {α : Type u_1} {stream : Stream α} {t k : ℕ} (hk : k ≤ (sample stream t).card) : ∃ r ≤ t, (sample stream r).card = k

If a finite prefix contains at least k distinct observations, some earlier prefix contains exactly k.

theorem GenLimit.Generic.eventualAtExactSize_mono {size : ℕ → ℕ} {good : ℕ → Prop} {d n : ℕ} (hcross : ∀ {t k : ℕ}, k ≤ size t → ∃ r ≤ t, size r = k) (hdn : d ≤ n) (hgood : ∀ (t : ℕ), size t = d → ∀ (s : ℕ), t ≤ s → good s) (t : ℕ) : size t = n → ∀ (s : ℕ), t ≤ s → good s

If every reached size can be crossed exactly, a property that holds eventually after reaching exact size d also holds after reaching any larger exact size.

theorem GenLimit.Generic.sample_card_le {α : Type u_1} (stream : Stream α) (t : ℕ) : (sample stream t).card ≤ t

theorem GenLimit.Generic.mem_language_of_mem_sample_of_presents {α : Type u_1} {stream : Stream α} {L : Language α} (hP : Presents stream L) {t : ℕ} {x : α} (hx : x ∈ sample stream t) : x ∈ L

theorem GenLimit.Generic.streamIn_of_presents {α : Type u_1} {stream : Stream α} {L : Language α} (hP : Presents stream L) : StreamIn stream L

theorem GenLimit.Generic.eventually_mem_sample_of_presents {α : Type u_1} {stream : Stream α} {L : Language α} (hP : Presents stream L) {x : α} (hx : x ∈ L) : ∃ (T : ℕ), ∀ (t : ℕ), T ≤ t → x ∈ sample stream t

theorem GenLimit.Generic.finset_eventually_subset_sample {α : Type u_1} {stream : Stream α} {L : Language α} (hP : Presents stream L) (S : Finset α) (hS : ↑S ⊆ L) : ∃ (T : ℕ), S ⊆ sample stream T

theorem GenLimit.Generic.exists_sample_card_ge_of_presents_infinite {α : Type u_1} {stream : Stream α} {L : Language α} (hP : Presents stream L) (hL : Set.Infinite L) (d : ℕ) : ∃ (t : ℕ), d ≤ (sample stream t).card

theorem GenLimit.Generic.exists_sample_card_eq_of_presents_infinite {α : Type u_1} {stream : Stream α} {L : Language α} (hP : Presents stream L) (hL : Set.Infinite L) (d : ℕ) : ∃ (t : ℕ), (sample stream t).card = d

An exact presentation of an infinite language passes through every finite number of distinct observations.

def GenLimit.Generic.CorrectAt {α : Type u_1} (G : Generator α) (L : Language α) (stream : Stream α) (t : ℕ) : Prop

The generated value is a fresh member of L at time t.

Equations

• GenLimit.Generic.CorrectAt G L stream t = (GenLimit.Generic.output G stream t ∈ L ∧ GenLimit.Generic.output G stream t ∉ GenLimit.Generic.sample stream t)