Finite history domains and query bounds for normalization

def GenLimit.FiniteWitness.boundedWords {α : Type u_1} [DecidableEq α] (S : Finset α) : ℕ → Finset (List α)

A constructive enumeration, including repetitions, of every word of bounded length.

Equations

• GenLimit.FiniteWitness.boundedWords S 0 = {[]}
• GenLimit.FiniteWitness.boundedWords S n.succ = insert [] (Finset.image (fun (p : α × List α) => p.1 :: p.2) (S ×ˢ GenLimit.FiniteWitness.boundedWords S n))

theorem GenLimit.FiniteWitness.mem_boundedWords {α : Type u_1} [DecidableEq α] {S : Finset α} {n : ℕ} {q : List α} : q ∈ boundedWords S n ↔ q.toFinset ⊆ S ∧ q.length ≤ n

theorem GenLimit.FiniteWitness.Candidate.congr_oracle {α : Type u_1} [DecidableEq α] [Encodable α] {F G : List α → α} {S : Finset α} {n k : ℕ} (h : ∀ q ∈ boundedWords S (2 * n), F q = G q) (p q : List α) : Candidate F S n p k q ↔ Candidate G S n p k q

theorem GenLimit.FiniteWitness.sampleRun_congr_oracle {α : Type u_1} [DecidableEq α] [Encodable α] {F G : List α → α} {S : Finset α} {n : ℕ} (h : ∀ q ∈ boundedWords S (2 * n), F q = G q) (k : ℕ) : sampleRun F S n k = sampleRun G S n k

theorem GenLimit.FiniteWitness.normalized_finite_query_bound {α : Type u_1} [DecidableEq α] [Encodable α] {F G : List α → α} (S : Finset α) (h : ∀ q ∈ boundedWords S (2 * S.card), F q = G q) : normalized F S = normalized G S

One finite set of oracle inputs, fixed by S alone, determines the normalized output.