The lower approximation is primitive recursive

primrec_lowerSeq: the numerators lowerSeq T t of Main Theorem I (1) are a primitive recursive function of the test and the stage. mainTheoremI_one packages clause (1) of Main Theorem I (I:592): a primitive recursive dyadic sequence, non-decreasing and tending to the sofic value.

Rewritings

theorem MIPRE.Tailored.Sofic.Measure.any_eq_foldr {α : Type u_1} (l : List α) (f : α → Bool) : l.any f = List.foldr (fun (a : α) (b : Bool) => f a || b) false l

theorem MIPRE.Tailored.Sofic.Measure.all_eq_foldr {α : Type u_1} (l : List α) (f : α → Bool) : l.all f = List.foldr (fun (a : α) (b : Bool) => f a && b) true l

theorem MIPRE.Tailored.Sofic.Measure.length_filter_eq_foldr {α : Type u_1} (l : List α) (p : α → Bool) : (List.filter p l).length = List.foldr (fun (a : α) (n : ℕ) => if p a = true then n + 1 else n) 0 l

theorem MIPRE.Tailored.Sofic.Measure.sum_eq_foldr (l : List ℕ) : l.sum = List.foldr (fun (a n : ℕ) => a + n) 0 l

Primitive recursion

theorem MIPRE.Tailored.Sofic.Measure.primrec_two_pow : Primrec fun (t : ℕ) => 2 ^ t

theorem MIPRE.Tailored.Sofic.Measure.primrec_nGen : Primrec SubgroupTestValue.SubgroupTestData.nGen

theorem MIPRE.Tailored.Sofic.Measure.primrec_challenges : Primrec SubgroupTestValue.SubgroupTestData.challenges

theorem MIPRE.Tailored.Sofic.Measure.primrec_totalWeight : Primrec SubgroupTestValue.SubgroupTestData.totalWeight

theorem MIPRE.Tailored.Sofic.Measure.idxOf_nat (l : List ℕ) (a : ℕ) : List.idxOf a l = List.idxOf a l

theorem MIPRE.Tailored.Sofic.Measure.primrec_applyLetter : Primrec fun (q : List (List ℕ) × SubgroupTestValue.Letter × ℕ) => applyLetter q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_applyWord : Primrec fun (q : List (List ℕ) × SubgroupTestValue.Word × ℕ) => applyWord q.1 q.2.1 q.2.2

@[reducible, inline]

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

The arguments (P, K, y, lit) of litC.

Equations

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

theorem MIPRE.Tailored.Sofic.Measure.primrec_litC : Primrec fun (q : LitArgs) => litC q.1 q.2.1 q.2.2.1 q.2.2.2

@[reducible, inline]

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

The arguments (P, K, cl, y) of passC.

Equations

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

theorem MIPRE.Tailored.Sofic.Measure.primrec_passC : Primrec fun (q : PassArgs) => passC q.1 q.2.1 q.2.2.1 q.2.2.2

@[reducible, inline]

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

The arguments (c, K, cl) of countC.

Equations

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

theorem MIPRE.Tailored.Sofic.Measure.primrec_countC : Primrec fun (q : CountArgs) => countC q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_numC : Primrec₂ numC

theorem MIPRE.Tailored.Sofic.Measure.primrecRel_mem : PrimrecRel fun (a : ℕ) (l : List ℕ) => a ∈ l

theorem MIPRE.Tailored.Sofic.Measure.primrecPred_validC : PrimrecPred fun (q : ℕ × ActCode) => ValidC q.1 q.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_lowerC : Primrec fun (q : SubgroupTestValue.SubgroupTestData × ActCode × ℕ) => lowerC q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_lowerAt : Primrec fun (q : SubgroupTestValue.SubgroupTestData × ℕ × ℕ) => lowerAt q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.Measure.primrec_lowerSeq : Primrec₂ lowerSeq

The lower approximation is primitive recursive.

theorem MIPRE.Tailored.Sofic.Measure.mainTheoremI_one : ∃ (α : SubgroupTestValue.SubgroupTestData → ℕ → ℕ), Primrec₂ α ∧ ∀ (T : SubgroupTestValue.SubgroupTestData), (Monotone fun (t : ℕ) => dyadic (α T t) t) ∧ (∀ (t : ℕ), dyadic (α T t) t ≤ T.valSof) ∧ Filter.Tendsto (fun (t : ℕ) => dyadic (α T t) t) Filter.atTop (nhds T.valSof)

Main Theorem I (1) (I:592): a primitive recursive sequence of dyadic numbers α T t / 2^t, non-decreasing in t, at most the sofic value and tending to it.