The upper approximation is primitive recursive

primrec_upperSeq: the numerators upperSeq T t of the upper approximation of the ergodic value are a primitive recursive function of the test and the stage — the polytope optimum over the grid is a finite list computation (Lemma I:1105, with linear programming replaced by enumeration). Each construction of Stage.lean is a composition of list operations; List.all, List.any and List.sum are folds (primrec_all, primrec_any, primrec_sum_map), and List.zip is a map over the indices (zip_eq_range).

Folds

theorem MIPRE.Tailored.Sofic.Measure.primrec_all {α β : Type} [Primcodable α] [Primcodable β] {L : α → List β} {f : α → β → Bool} (hL : Primrec L) (hf : Primrec₂ f) : Primrec fun (a : α) => (L a).all (f a)

theorem MIPRE.Tailored.Sofic.Measure.primrec_any {α β : Type} [Primcodable α] [Primcodable β] {L : α → List β} {f : α → β → Bool} (hL : Primrec L) (hf : Primrec₂ f) : Primrec fun (a : α) => (L a).any (f a)

theorem MIPRE.Tailored.Sofic.Measure.primrec_sum_map {α β : Type} [Primcodable α] [Primcodable β] {L : α → List β} {f : α → β → ℕ} (hL : Primrec L) (hf : Primrec₂ f) : Primrec fun (a : α) => (List.map (f a) (L a)).sum

theorem MIPRE.Tailored.Sofic.Measure.primrec_sum : Primrec List.sum

theorem MIPRE.Tailored.Sofic.Measure.zip_eq_range {α β : Type} (l₁ : List α) (l₂ : List β) (d₁ : α) (d₂ : β) : l₁.zip l₂ = List.map (fun (i : ℕ) => (l₁.getD i d₁, l₂.getD i d₂)) (List.range (min l₁.length l₂.length))

theorem MIPRE.Tailored.Sofic.Measure.primrec_zip {α β : Type} [Primcodable α] [Primcodable β] [Inhabited α] [Inhabited β] : Primrec₂ List.zip

Words

theorem MIPRE.Tailored.Sofic.Measure.primrec_letters : Primrec letters

theorem MIPRE.Tailored.Sofic.Measure.primrec_wordsStep : Primrec₂ wordsStep

theorem MIPRE.Tailored.Sofic.Measure.primrec_wordsLen : Primrec₂ wordsLen

theorem MIPRE.Tailored.Sofic.Measure.primrec_wordsUpTo : Primrec₂ wordsUpTo

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Measure.TT : Type

The arguments (T, t).

Equations

• MIPRE.Tailored.Sofic.Measure.TT = (SubgroupTestValue.SubgroupTestData × ℕ)

theorem MIPRE.Tailored.Sofic.Measure.primrec_stageW : Primrec fun (x : TT) => stageW x.1 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_stageD : Primrec fun (x : TT) => stageD x.1 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_stagePt : Primrec fun (x : TT) => stagePt x.1 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_stageP : Primrec fun (x : TT) => stageP x.1 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_stageM : Primrec fun (x : TT) => stageM x.1 x.2

Patterns

theorem MIPRE.Tailored.Sofic.Measure.primrec_extW : Primrec fun (x : List SubgroupTestValue.Word × List Bool × SubgroupTestValue.Word) => extW x.1 x.2.1 x.2.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_extW' {γ : Type} [Primcodable γ] {W : γ → List SubgroupTestValue.Word} {p : γ → List Bool} {u : γ → SubgroupTestValue.Word} (hW : Primrec W) (hp : Primrec p) (hu : Primrec u) : Primrec fun (c : γ) => extW (W c) (p c) (u c)

extW with its arguments given by primitive recursive functions.

theorem MIPRE.Tailored.Sofic.Measure.primrec_litW_ext : Primrec fun (x : (List SubgroupTestValue.Word × List Bool) × List SubgroupTestValue.Word × ℕ × Bool) => litW x.2.1 (extW x.1.1 x.1.2) x.2.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_passW_ext : Primrec fun (x : (List SubgroupTestValue.Word × List Bool) × List SubgroupTestValue.Word × List (List (ℕ × Bool))) => passW x.2.1 x.2.2 (extW x.1.1 x.1.2)

theorem MIPRE.Tailored.Sofic.Measure.primrec_memW : Primrec₂ memW

theorem MIPRE.Tailored.Sofic.Measure.primrec_cancel2 : Primrec₂ cancel2

theorem MIPRE.Tailored.Sofic.Measure.primrec_drop1 : Primrec fun (x : ℕ × SubgroupTestValue.Word × ℕ) => drop1 x.1 x.2.1 x.2.2

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Measure.GArgs : Type

The arguments (s, W, p) of goodP.

Equations

• MIPRE.Tailored.Sofic.Measure.GArgs = (ℕ × List SubgroupTestValue.Word × List Bool)

theorem MIPRE.Tailored.Sofic.Measure.primrec_goodP : Primrec fun (x : GArgs) => goodP x.1 x.2.1 x.2.2

Grid points

theorem MIPRE.Tailored.Sofic.Measure.primrec_vecsStep : Primrec₂ vecsStep

theorem MIPRE.Tailored.Sofic.Measure.primrec_allVecs : Primrec₂ allVecs

theorem MIPRE.Tailored.Sofic.Measure.primrec_cntR {γ : Type} [Primcodable γ] {n : γ → List ℕ} {Pt : γ → List (List Bool)} {f : γ → List Bool → Bool} (hn : Primrec n) (hPt : Primrec Pt) (hf : Primrec₂ f) : Primrec fun (c : γ) => cntR (n c) (Pt c) (f c)

cntR with its arguments given by primitive recursive functions.

theorem MIPRE.Tailored.Sofic.Measure.primrec_ndist : Primrec₂ ndist

theorem MIPRE.Tailored.Sofic.Measure.listBool_beq (a b : List Bool) : (a == b) = decide (a = b)

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Measure.IArgs : Type

The arguments ((T, t), g, n) of invErr.

Equations

• MIPRE.Tailored.Sofic.Measure.IArgs = (MIPRE.Tailored.Sofic.Measure.TT × SubgroupTestValue.Letter × List ℕ)

theorem MIPRE.Tailored.Sofic.Measure.primrec_invErr : Primrec fun (x : IArgs) => invErr x.1.1 x.1.2 x.2.1 x.2.2

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Measure.NArgs : Type

The arguments ((T, t), n).

Equations

• MIPRE.Tailored.Sofic.Measure.NArgs = (MIPRE.Tailored.Sofic.Measure.TT × List ℕ)

theorem MIPRE.Tailored.Sofic.Measure.primrecRel_good : PrimrecRel fun (y : ℕ × List Bool) (x : NArgs) => ¬0 < y.1 ∨ goodP x.1.1.nGen (stageW x.1.1 x.1.2) y.2 = true

theorem MIPRE.Tailored.Sofic.Measure.primrecPred_feas2 : PrimrecPred fun (x : NArgs) => ∀ y ∈ x.2.zip (stagePt x.1.1 x.1.2), ¬0 < y.1 ∨ goodP x.1.1.nGen (stageW x.1.1 x.1.2) y.2 = true

theorem MIPRE.Tailored.Sofic.Measure.primrecRel_inv : PrimrecRel fun (g : SubgroupTestValue.Letter) (x : NArgs) => invErr x.1.1 x.1.2 g x.2 ≤ 4 * stageP x.1.1 x.1.2

theorem MIPRE.Tailored.Sofic.Measure.primrecPred_feas3 : PrimrecPred fun (x : NArgs) => ∀ g ∈ letters x.1.1.nGen, invErr x.1.1 x.1.2 g x.2 ≤ 4 * stageP x.1.1 x.1.2

theorem MIPRE.Tailored.Sofic.Measure.primrecPred_feas1 : PrimrecPred fun (x : NArgs) => x.2.sum = stageM x.1.1 x.1.2

theorem MIPRE.Tailored.Sofic.Measure.primrecPred_feasible : PrimrecPred fun (x : NArgs) => Feasible x.1.1 x.1.2 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_numG : Primrec fun (x : NArgs) => numG x.1.1 x.1.2 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_maxNum : Primrec fun (x : TT) => maxNum x.1 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrecPred_covers : PrimrecPred fun (x : TT) => Covers x.1 x.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_ceilDiv : Primrec₂ ceilDiv

theorem MIPRE.Tailored.Sofic.Measure.primrec_upperSeq : Primrec₂ upperSeq

The upper approximation is primitive recursive.