Ordered finite prefixes of information streams

This file supplies the paper-independent ordered-history interface used by Gold identification. KM and DenseGeneration usually consume sample, which forgets order and repetitions; textPrefix retains both. The bridge theorem textPrefix_toFinset shows that the two views contain the same observed values.

def GenLimit.textPrefix {α : Type u_1} (stream : ℕ → α) (t : ℕ) : List α

The ordered observations strictly before time t.

Equations

• GenLimit.textPrefix stream t = List.map stream (List.range t)

@[simp]

theorem GenLimit.textPrefix_length {α : Type u_1} (stream : ℕ → α) (t : ℕ) : (textPrefix stream t).length = t

@[simp]

theorem GenLimit.textPrefix_zero {α : Type u_1} (stream : ℕ → α) : textPrefix stream 0 = []

theorem GenLimit.textPrefix_succ {α : Type u_1} (stream : ℕ → α) (t : ℕ) : textPrefix stream (t + 1) = textPrefix stream t ++ [stream t]

theorem GenLimit.textPrefix_prefix {α : Type u_1} (stream : ℕ → α) {s t : ℕ} (hst : s ≤ t) : textPrefix stream s <+: textPrefix stream t

Earlier ordered histories are list prefixes of later histories.

theorem GenLimit.textPrefix_eq_ofFn {α : Type u_1} (stream : ℕ → α) (t : ℕ) : textPrefix stream t = List.ofFn fun (i : Fin t) => stream ↑i

The list prefix is the list representation of the corresponding finite tuple.

theorem GenLimit.mem_textPrefix_iff {α : Type u_1} {stream : ℕ → α} {t : ℕ} {x : α} : x ∈ textPrefix stream t ↔ ∃ s < t, stream s = x

theorem GenLimit.textPrefix_toFinset (stream : ℕ → ℕ) (t : ℕ) : (textPrefix stream t).toFinset = sample stream t

Forgetting order and repetitions from an ordered prefix gives the finite sample used by the KM and DenseGeneration developments.