The sofic value is approximable from below (Main Theorem I (1))

Paper I, Main Theorem I clause (1) (I:592) and its proof (I:1148–1168): enumerate the finite actions and take the running maximum of their values.

A finite action is coded by (N, P), P the list of the rows [σ_i(0), …, σ_i(N − 1)] of its permutations (ActCode). ValidC s c is the decidable condition that a code is one (each row a list of length N with entries below N and every point below N among them), decodeAct reads off the action, and codeOf writes one down. On codes the value is a ratio of naturals (value_eq_numC), the action of a word being computed letter by letter (applyWord, the inverse of a row by List.idxOf).

The approximation is dyadic: lowerSeq T t / 2^t is the largest value of the actions with code number at most t, rounded down to the grid of step 2^{-t}. It is primitive recursive (primrec_lowerSeq), non-decreasing, at most the sofic value, and tends to it (mainTheoremI_one).

Codes of finite actions

@[reducible, inline]

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

A code of a finite action: the number of points and the rows of the permutations.

Equations

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

def MIPRE.Tailored.Sofic.Measure.applyLetter (P : List (List ℕ)) (l : SubgroupTestValue.Letter) (y : ℕ) : ℕ

A letter acting on a point through the rows P; letters beyond the rows act as the identity, an inverted letter by the position of the point in its row.

Equations

• MIPRE.Tailored.Sofic.Measure.applyLetter P l y = if l.1 < P.length then if l.2 = true then List.idxOf y (P.getD l.1 []) else (P.getD l.1 []).getD y 0 else y

def MIPRE.Tailored.Sofic.Measure.applyWord (P : List (List ℕ)) (w : SubgroupTestValue.Word) (y : ℕ) : ℕ

A word acting on a point, its last letter first, as in FiniteAction.wordPerm.

Equations

• MIPRE.Tailored.Sofic.Measure.applyWord P w y = List.foldr (MIPRE.Tailored.Sofic.Measure.applyLetter P) y w

def MIPRE.Tailored.Sofic.Measure.litC (P : List (List ℕ)) (K : List SubgroupTestValue.Word) (y : ℕ) (lit : ℕ × Bool) : Bool

The literal (i, b) at the point y.

Equations

• MIPRE.Tailored.Sofic.Measure.litC P K y lit = (decide (lit.1 < K.length) && decide (MIPRE.Tailored.Sofic.Measure.applyWord P (K.getD lit.1 []) y = y) == lit.2)

def MIPRE.Tailored.Sofic.Measure.passC (P : List (List ℕ)) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) (y : ℕ) : Bool

The point y passes the challenge (K, cl).

Equations

• MIPRE.Tailored.Sofic.Measure.passC P K cl y = cl.any fun (c : List (ℕ × Bool)) => c.all fun (lit : ℕ × Bool) => MIPRE.Tailored.Sofic.Measure.litC P K y lit

def MIPRE.Tailored.Sofic.Measure.countC (c : ActCode) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : ℕ

The number of points passing a challenge.

Equations

• MIPRE.Tailored.Sofic.Measure.countC c K cl = (List.filter (MIPRE.Tailored.Sofic.Measure.passC c.2 K cl) (List.range c.1)).length

def MIPRE.Tailored.Sofic.Measure.numC (T : SubgroupTestValue.SubgroupTestData) (c : ActCode) : ℕ

The weighted number of passing points, the numerator of the value.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.Tailored.Sofic.Measure.ValidC (s : ℕ) (c : ActCode) : Prop

A code is the code of a finite action on s generators.

Equations

• MIPRE.Tailored.Sofic.Measure.ValidC s c = (0 < c.1 ∧ c.2.length = s ∧ ∀ p ∈ c.2, p.length = c.1 ∧ (∀ v ∈ p, v < c.1) ∧ ∀ y < c.1, y ∈ p)

@[instance_reducible]

instance MIPRE.Tailored.Sofic.Measure.instDecidablePredActCodeValidC (s : ℕ) : DecidablePred (ValidC s)

Equations

• MIPRE.Tailored.Sofic.Measure.instDecidablePredActCodeValidC s x✝ = id inferInstance

structure MIPRE.Tailored.Sofic.Measure.Represents {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) (c : ActCode) : Prop

The code c represents the action σ.

• N_eq : c.1 = σ.N
• len : c.2.length = s
• row_len (i : ℕ) : i < s → (c.2.getD i []).length = σ.N
• row (i : ℕ) (hi : i < s) (x : Fin σ.N) : (c.2.getD i []).getD (↑x) 0 = ↑((σ.σ ⟨i, hi⟩) x)

theorem MIPRE.Tailored.Sofic.Measure.Represents.mem_row {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) {i : ℕ} (hi : i < s) (y : Fin σ.N) : ↑y ∈ c.2.getD i []

theorem MIPRE.Tailored.Sofic.Measure.Represents.applyLetter_eq {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) (l : SubgroupTestValue.Letter) (y : Fin σ.N) : applyLetter c.2 l ↑y = ↑((σ.letterPerm l) y)

theorem MIPRE.Tailored.Sofic.Measure.Represents.applyWord_eq {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) (w : SubgroupTestValue.Word) (y : Fin σ.N) : applyWord c.2 w ↑y = ↑((σ.wordPerm w) y)

theorem MIPRE.Tailored.Sofic.Measure.Represents.litC_eq {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) (K : List SubgroupTestValue.Word) (y : Fin σ.N) (lit : ℕ × Bool) : litC c.2 K (↑y) lit = decide (σ.LitHolds K y lit)

theorem MIPRE.Tailored.Sofic.Measure.Represents.passC_eq {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) (y : Fin σ.N) : passC c.2 K cl ↑y = decide (σ.Passes K cl y)

theorem MIPRE.Tailored.Sofic.Measure.card_filter_fin (N : ℕ) (q : ℕ → Bool) : {x : Fin N | q ↑x = true}.card = (List.filter q (List.range N)).length

theorem MIPRE.Tailored.Sofic.Measure.Represents.countC_eq {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : countC c K cl = {x : Fin σ.N | σ.Passes K cl x}.card

theorem MIPRE.Tailored.Sofic.Measure.list_sum_map_div {ι : Type u_1} (l : List ι) (f : ι → ℝ) (a : ℝ) : (List.map (fun (i : ι) => f i / a) l).sum = (List.map f l).sum / a

theorem MIPRE.Tailored.Sofic.Measure.Represents.value_eq {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) (T : SubgroupTestValue.SubgroupTestData) (hs : s = T.nGen) : T.value (hs ▸ σ) = ↑(numC T c) / ↑(c.1 * T.totalWeight)

On a code the value is a ratio of naturals.

theorem MIPRE.Tailored.Sofic.Measure.ValidC.row {s : ℕ} {c : ActCode} (h : ValidC s c) {i : ℕ} (hi : i < s) : (c.2.getD i []).length = c.1 ∧ (∀ v ∈ c.2.getD i [], v < c.1) ∧ ∀ y < c.1, y ∈ c.2.getD i []

The row i of a valid code.

theorem MIPRE.Tailored.Sofic.Measure.ValidC.getD_lt {s : ℕ} {c : ActCode} (h : ValidC s c) {i : ℕ} (hi : i < s) {x : ℕ} (hx : x < c.1) : (c.2.getD i []).getD x 0 < c.1

def MIPRE.Tailored.Sofic.Measure.rowFun {s : ℕ} {c : ActCode} (h : ValidC s c) (i : Fin s) (x : Fin c.1) : Fin c.1

The map of the row i of a valid code.

Equations

• MIPRE.Tailored.Sofic.Measure.rowFun h i x = ⟨(c.2.getD ↑i []).getD (↑x) 0, ⋯⟩

theorem MIPRE.Tailored.Sofic.Measure.rowFun_bijective {s : ℕ} {c : ActCode} (h : ValidC s c) (i : Fin s) : Function.Bijective (rowFun h i)

noncomputable def MIPRE.Tailored.Sofic.Measure.decodeAct (s : ℕ) (c : ActCode) (h : ValidC s c) : SubgroupTestValue.FiniteAction s

The action of a valid code.

Equations

• MIPRE.Tailored.Sofic.Measure.decodeAct s c h = { N := c.1, N_pos := ⋯, σ := fun (i : Fin s) => Equiv.ofBijective (MIPRE.Tailored.Sofic.Measure.rowFun h i) ⋯ }

theorem MIPRE.Tailored.Sofic.Measure.represents_decodeAct (s : ℕ) (c : ActCode) (h : ValidC s c) : Represents (decodeAct s c h) c

def MIPRE.Tailored.Sofic.Measure.codeOf {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) : ActCode

The code of a finite action.

Equations

• MIPRE.Tailored.Sofic.Measure.codeOf σ = (σ.N, List.ofFn fun (i : Fin s) => List.ofFn fun (x : Fin σ.N) => ↑((σ.σ i) x))

theorem MIPRE.Tailored.Sofic.Measure.represents_codeOf {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) : Represents σ (codeOf σ)

theorem MIPRE.Tailored.Sofic.Measure.Represents.valid {s : ℕ} {σ : SubgroupTestValue.FiniteAction s} {c : ActCode} (h : Represents σ c) : ValidC s c

The lower approximation

def MIPRE.Tailored.Sofic.Measure.lowerC (T : SubgroupTestValue.SubgroupTestData) (c : ActCode) (t : ℕ) : ℕ

The value of a code rounded down to the grid of step 2^{-t}, as a numerator; 0 for an invalid code.

Equations

• MIPRE.Tailored.Sofic.Measure.lowerC T c t = if MIPRE.Tailored.Sofic.Measure.ValidC T.nGen c then 2 ^ t * MIPRE.Tailored.Sofic.Measure.numC T c / (c.1 * T.totalWeight) else 0

def MIPRE.Tailored.Sofic.Measure.lowerAt (T : SubgroupTestValue.SubgroupTestData) (n t : ℕ) : ℕ

lowerC of the code with number n.

Equations

• MIPRE.Tailored.Sofic.Measure.lowerAt T n t = match Encodable.decode n with | some c => MIPRE.Tailored.Sofic.Measure.lowerC T c t | none => 0

def MIPRE.Tailored.Sofic.Measure.lowerSeq (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) : ℕ

The lower approximation at stage t: the numerator over 2^t of the largest rounded value of the codes numbered at most t.

Equations

• MIPRE.Tailored.Sofic.Measure.lowerSeq T t = List.foldr max 0 (List.map (fun (n : ℕ) => MIPRE.Tailored.Sofic.Measure.lowerAt T n t) (List.range (t + 1)))

noncomputable def MIPRE.Tailored.Sofic.Measure.dyadic (n t : ℕ) : ℝ

The dyadic number n / 2^t.

Equations

• MIPRE.Tailored.Sofic.Measure.dyadic n t = ↑n / 2 ^ t

theorem MIPRE.Tailored.Sofic.Measure.dyadic_nonneg (n t : ℕ) : 0 ≤ dyadic n t

theorem MIPRE.Tailored.Sofic.Measure.floor_bounds (a b t : ℕ) : dyadic (2 ^ t * a / b) t ≤ ↑a / ↑b ∧ ↑a / ↑b - 1 / 2 ^ t ≤ dyadic (2 ^ t * a / b) t

Rounding down to the grid.

theorem MIPRE.Tailored.Sofic.Measure.lowerC_le {T : SubgroupTestValue.SubgroupTestData} {c : ActCode} {σ : SubgroupTestValue.FiniteAction T.nGen} (h : Represents σ c) (t : ℕ) : dyadic (lowerC T c t) t ≤ T.value σ

theorem MIPRE.Tailored.Sofic.Measure.le_lowerC {T : SubgroupTestValue.SubgroupTestData} {c : ActCode} {σ : SubgroupTestValue.FiniteAction T.nGen} (h : Represents σ c) (t : ℕ) : T.value σ - 1 / 2 ^ t ≤ dyadic (lowerC T c t) t

theorem MIPRE.Tailored.Sofic.Measure.lowerAt_le (T : SubgroupTestValue.SubgroupTestData) (n t : ℕ) : dyadic (lowerAt T n t) t ≤ T.valSof

theorem MIPRE.Tailored.Sofic.Measure.dyadic_mono_succ (n t : ℕ) : dyadic n t = dyadic (2 * n) (t + 1)

theorem MIPRE.Tailored.Sofic.Measure.lowerC_mono (T : SubgroupTestValue.SubgroupTestData) (c : ActCode) (t : ℕ) : dyadic (lowerC T c t) t ≤ dyadic (lowerC T c (t + 1)) (t + 1)

theorem MIPRE.Tailored.Sofic.Measure.lowerAt_mono (T : SubgroupTestValue.SubgroupTestData) (n t : ℕ) : dyadic (lowerAt T n t) t ≤ dyadic (lowerAt T n (t + 1)) (t + 1)

theorem MIPRE.Tailored.Sofic.Measure.le_foldr_max {l : List ℕ} {a : ℕ} (h : a ∈ l) : a ≤ List.foldr max 0 l

theorem MIPRE.Tailored.Sofic.Measure.foldr_max_mem_or (l : List ℕ) : List.foldr max 0 l = 0 ∨ List.foldr max 0 l ∈ l

theorem MIPRE.Tailored.Sofic.Measure.le_lowerSeq (T : SubgroupTestValue.SubgroupTestData) {n t : ℕ} (hn : n ≤ t) : lowerAt T n t ≤ lowerSeq T t

theorem MIPRE.Tailored.Sofic.Measure.lowerSeq_le (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) : dyadic (lowerSeq T t) t ≤ T.valSof

theorem MIPRE.Tailored.Sofic.Measure.lowerSeq_mono_succ (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) : dyadic (lowerSeq T t) t ≤ dyadic (lowerSeq T (t + 1)) (t + 1)

theorem MIPRE.Tailored.Sofic.Measure.lowerSeq_monotone (T : SubgroupTestValue.SubgroupTestData) : Monotone fun (t : ℕ) => dyadic (lowerSeq T t) t

theorem MIPRE.Tailored.Sofic.Measure.tendsto_lowerSeq (T : SubgroupTestValue.SubgroupTestData) : Filter.Tendsto (fun (t : ℕ) => dyadic (lowerSeq T t) t) Filter.atTop (nhds T.valSof)